:: SYSREL semantic presentation

registration

let c₁, c₂ be set ;
cluster [:a₁,a₂:] -> Relation-like ;
correctness by RELAT_1:6;

end;

theorem Th1: :: SYSREL:1

canceled;

theorem Th2: :: SYSREL:2

canceled;

theorem Th3: :: SYSREL:3

canceled;

theorem Th4: :: SYSREL:4

canceled;

theorem Th5: :: SYSREL:5

canceled;

theorem Th6: :: SYSREL:6

canceled;

theorem Th7: :: SYSREL:7

canceled;

theorem Th8: :: SYSREL:8

canceled;

theorem Th9: :: SYSREL:9

canceled;

theorem Th10: :: SYSREL:10

canceled;

theorem Th11: :: SYSREL:11

canceled;

theorem Th12: :: SYSREL:12

for b₁, b₂ being set st b₁ <> {} & b₂ <> {} holds
( dom [:b₁,b₂:] = b₁ & rng [:b₁,b₂:] = b₂ )

proof end;

theorem Th13: :: SYSREL:13

for b₁, b₂ being set
for b₃ being Relation holds
( dom (b₃ /\ [:b₁,b₂:]) c= b₁ & rng (b₃ /\ [:b₁,b₂:]) c= b₂ )

proof end;

theorem Th14: :: SYSREL:14

for b₁, b₂ being set
for b₃ being Relation st b₁ misses b₂ holds
( dom (b₃ /\ [:b₁,b₂:]) misses rng (b₃ /\ [:b₁,b₂:]) & dom ((b₃ ~ ) /\ [:b₁,b₂:]) misses rng ((b₃ ~ ) /\ [:b₁,b₂:]) )

proof end;

theorem Th15: :: SYSREL:15

for b₁, b₂ being set
for b₃ being Relation st b₃ c= [:b₁,b₂:] holds
( dom b₃ c= b₁ & rng b₃ c= b₂ )

proof end;

theorem Th16: :: SYSREL:16

for b₁, b₂ being set
for b₃ being Relation st b₃ c= [:b₁,b₂:] holds
b₃ ~ c= [:b₂,b₁:]

proof end;

theorem Th17: :: SYSREL:17

canceled;

theorem Th18: :: SYSREL:18

for b₁, b₂ being set holds [:b₁,b₂:] ~ = [:b₂,b₁:]

proof end;

theorem Th19: :: SYSREL:19

canceled;

theorem Th20: :: SYSREL:20

for b₁, b₂, b₃ being Relation holds
( (b₁ \/ b₂) * b₃ = (b₁ * b₃) \/ (b₂ * b₃) & b₁ * (b₂ \/ b₃) = (b₁ * b₂) \/ (b₁ * b₃) )

proof end;

theorem Th21: :: SYSREL:21

canceled;

theorem Th22: :: SYSREL:22

for b₁, b₂, b₃, b₄ being set
for b₅ being Relation holds
( ( b₁ misses b₂ & b₅ c= [:b₁,b₂:] \/ [:b₂,b₁:] & [b₃,b₄] in b₅ & b₃ in b₁ implies ( not b₃ in b₂ & not b₄ in b₁ & b₄ in b₂ ) ) & ( b₁ misses b₂ & b₅ c= [:b₁,b₂:] \/ [:b₂,b₁:] & [b₃,b₄] in b₅ & b₄ in b₂ implies ( not b₄ in b₁ & not b₃ in b₂ & b₃ in b₁ ) ) & ( b₁ misses b₂ & b₅ c= [:b₁,b₂:] \/ [:b₂,b₁:] & [b₃,b₄] in b₅ & b₃ in b₂ implies ( not b₃ in b₁ & not b₄ in b₂ & b₄ in b₁ ) ) & ( b₁ misses b₂ & b₅ c= [:b₁,b₂:] \/ [:b₂,b₁:] & [b₃,b₄] in b₅ & b₄ in b₁ implies ( not b₃ in b₁ & not b₄ in b₂ & b₃ in b₂ ) ) )

proof end;

theorem Th23: :: SYSREL:23

canceled;

theorem Th24: :: SYSREL:24

for b₁, b₂, b₃ being set
for b₄ being Relation holds
( ( b₄ c= [:b₁,b₂:] & b₃ c= b₁ implies b₄ | b₃ = b₄ /\ [:b₃,b₂:] ) & ( b₄ c= [:b₁,b₂:] & b₃ c= b₂ implies b₃ | b₄ = b₄ /\ [:b₁,b₃:] ) )

proof end;

theorem Th25: :: SYSREL:25

for b₁, b₂, b₃, b₄ being set
for b₅ being Relation st b₅ c= [:b₁,b₂:] & b₁ = b₃ \/ b₄ holds
b₅ = (b₅ | b₃) \/ (b₅ | b₄)

proof end;

theorem Th26: :: SYSREL:26

for b₁, b₂ being set
for b₃ being Relation st b₁ misses b₂ & b₃ c= [:b₁,b₂:] \/ [:b₂,b₁:] holds
b₃ | b₁ c= [:b₁,b₂:]

proof end;

theorem Th27: :: SYSREL:27

for b₁, b₂ being Relation st b₁ c= b₂ holds
b₁ ~ c= b₂ ~

proof end;

Lemma6: for b₁ being set holds id b₁ c= [:b₁,b₁:]

proof end;

theorem Th28: :: SYSREL:28

canceled;

theorem Th29: :: SYSREL:29

for b₁ being set holds (id b₁) * (id b₁) = id b₁

proof end;

theorem Th30: :: SYSREL:30

for b₁ being set holds id {b₁} = {[b₁,b₁]}

proof end;

theorem Th31: :: SYSREL:31

for b₁, b₂, b₃ being set holds
( [b₁,b₂] in id b₃ iff [b₂,b₁] in id b₃ ) by RELAT_1:def 10;

theorem Th32: :: SYSREL:32

for b₁, b₂ being set holds
( id (b₁ \/ b₂) = (id b₁) \/ (id b₂) & id (b₁ /\ b₂) = (id b₁) /\ (id b₂) & id (b₁ \ b₂) = (id b₁) \ (id b₂) )

proof end;

theorem Th33: :: SYSREL:33

for b₁, b₂ being set st b₁ c= b₂ holds
id b₁ c= id b₂

proof end;

theorem Th34: :: SYSREL:34

for b₁, b₂ being set holds (id (b₁ \ b₂)) \ (id b₁) = {}

proof end;

theorem Th35: :: SYSREL:35

for b₁ being Relation st b₁ c= id (dom b₁) holds
b₁ = id (dom b₁)

proof end;

theorem Th36: :: SYSREL:36

for b₁ being set
for b₂ being Relation st id b₁ c= b₂ \/ (b₂ ~ ) holds
( id b₁ c= b₂ & id b₁ c= b₂ ~ )

proof end;

theorem Th37: :: SYSREL:37

for b₁ being set
for b₂ being Relation st id b₁ c= b₂ holds
id b₁ c= b₂ ~

proof end;

theorem Th38: :: SYSREL:38

for b₁ being set
for b₂ being Relation st b₂ c= [:b₁,b₁:] holds
( b₂ \ (id (dom b₂)) = b₂ \ (id b₁) & b₂ \ (id (rng b₂)) = b₂ \ (id b₁) )

proof end;

theorem Th39: :: SYSREL:39

for b₁ being set
for b₂ being Relation holds
( ( (id b₁) * (b₂ \ (id b₁)) = {} implies dom (b₂ \ (id b₁)) = (dom b₂) \ (dom (id b₁)) ) & ( (b₂ \ (id b₁)) * (id b₁) = {} implies rng (b₂ \ (id b₁)) = (rng b₂) \ (rng (id b₁)) ) )

proof end;

theorem Th40: :: SYSREL:40

for b₁ being Relation holds
( ( b₁ c= b₁ * b₁ & b₁ * (b₁ \ (id (rng b₁))) = {} implies id (rng b₁) c= b₁ ) & ( b₁ c= b₁ * b₁ & (b₁ \ (id (dom b₁))) * b₁ = {} implies id (dom b₁) c= b₁ ) )

proof end;

theorem Th41: :: SYSREL:41

for b₁ being Relation holds
( ( b₁ c= b₁ * b₁ & b₁ * (b₁ \ (id (rng b₁))) = {} implies b₁ /\ (id (rng b₁)) = id (rng b₁) ) & ( b₁ c= b₁ * b₁ & (b₁ \ (id (dom b₁))) * b₁ = {} implies b₁ /\ (id (dom b₁)) = id (dom b₁) ) )

proof end;

theorem Th42: :: SYSREL:42

for b₁ being set
for b₂ being Relation holds
( ( b₂ * (b₂ \ (id b₁)) = {} & rng b₂ c= b₁ implies b₂ * (b₂ \ (id (rng b₂))) = {} ) & ( (b₂ \ (id b₁)) * b₂ = {} & dom b₂ c= b₁ implies (b₂ \ (id (dom b₂))) * b₂ = {} ) )

proof end;

definition

let c₁ be Relation;
func CL c₁ -> Relation equals :: SYSREL:def 1
a₁ /\ (id (dom a₁));
correctness ;

end;

:: deftheorem Def1 defines CL SYSREL:def 1 :

theorem Th43: :: SYSREL:43

for b₁ being Relation holds
( CL b₁ c= b₁ & CL b₁ c= id (dom b₁) ) by XBOOLE_1:17;

theorem Th44: :: SYSREL:44

for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in CL b₃ holds
( b₁ in dom (CL b₃) & b₁ = b₂ )

proof end;

theorem Th45: :: SYSREL:45

for b₁ being Relation holds dom (CL b₁) = rng (CL b₁)

proof end;

theorem Th46: :: SYSREL:46

for b₁ being set
for b₂ being Relation holds
( ( b₁ in dom (CL b₂) implies ( b₁ in dom b₂ & [b₁,b₁] in b₂ ) ) & ( b₁ in dom b₂ & [b₁,b₁] in b₂ implies b₁ in dom (CL b₂) ) & ( b₁ in rng (CL b₂) implies ( b₁ in dom b₂ & [b₁,b₁] in b₂ ) ) & ( b₁ in dom b₂ & [b₁,b₁] in b₂ implies b₁ in rng (CL b₂) ) & ( b₁ in rng (CL b₂) implies ( b₁ in rng b₂ & [b₁,b₁] in b₂ ) ) & ( b₁ in rng b₂ & [b₁,b₁] in b₂ implies b₁ in rng (CL b₂) ) & ( b₁ in dom (CL b₂) implies ( b₁ in rng b₂ & [b₁,b₁] in b₂ ) ) & ( b₁ in rng b₂ & [b₁,b₁] in b₂ implies b₁ in dom (CL b₂) ) )

proof end;

theorem Th47: :: SYSREL:47

for b₁ being Relation holds CL b₁ = id (dom (CL b₁))

proof end;

theorem Th48: :: SYSREL:48

for b₁, b₂ being set
for b₃ being Relation holds
( ( b₃ * b₃ = b₃ & b₃ * (b₃ \ (CL b₃)) = {} & [b₁,b₂] in b₃ & b₁ <> b₂ implies ( b₁ in (dom b₃) \ (dom (CL b₃)) & b₂ in dom (CL b₃) ) ) & ( b₃ * b₃ = b₃ & (b₃ \ (CL b₃)) * b₃ = {} & [b₁,b₂] in b₃ & b₁ <> b₂ implies ( b₂ in (rng b₃) \ (dom (CL b₃)) & b₁ in dom (CL b₃) ) ) )

proof end;

theorem Th49: :: SYSREL:49

for b₁, b₂ being set
for b₃ being Relation holds
( ( b₃ * b₃ = b₃ & b₃ * (b₃ \ (id (dom b₃))) = {} & [b₁,b₂] in b₃ & b₁ <> b₂ implies ( b₁ in (dom b₃) \ (dom (CL b₃)) & b₂ in dom (CL b₃) ) ) & ( b₃ * b₃ = b₃ & (b₃ \ (id (dom b₃))) * b₃ = {} & [b₁,b₂] in b₃ & b₁ <> b₂ implies ( b₂ in (rng b₃) \ (dom (CL b₃)) & b₁ in dom (CL b₃) ) ) )

proof end;

theorem Th50: :: SYSREL:50

for b₁ being Relation holds
( ( b₁ * b₁ = b₁ & b₁ * (b₁ \ (id (dom b₁))) = {} implies ( dom (CL b₁) = rng b₁ & rng (CL b₁) = rng b₁ ) ) & ( b₁ * b₁ = b₁ & (b₁ \ (id (dom b₁))) * b₁ = {} implies ( dom (CL b₁) = dom b₁ & rng (CL b₁) = dom b₁ ) ) )

proof end;

theorem Th51: :: SYSREL:51

for b₁ being Relation holds
( dom (CL b₁) c= dom b₁ & rng (CL b₁) c= rng b₁ & rng (CL b₁) c= dom b₁ & dom (CL b₁) c= rng b₁ )

proof end;

theorem Th52: :: SYSREL:52

for b₁ being Relation holds
( id (dom (CL b₁)) c= id (dom b₁) & id (rng (CL b₁)) c= id (dom b₁) )

proof end;

theorem Th53: :: SYSREL:53

for b₁ being Relation holds
( id (dom (CL b₁)) c= b₁ & id (rng (CL b₁)) c= b₁ )

proof end;

theorem Th54: :: SYSREL:54

for b₁ being set
for b₂ being Relation holds
( ( id b₁ c= b₂ & (id b₁) * (b₂ \ (id b₁)) = {} implies b₂ | b₁ = id b₁ ) & ( id b₁ c= b₂ & (b₂ \ (id b₁)) * (id b₁) = {} implies b₁ | b₂ = id b₁ ) )

proof end;

theorem Th55: :: SYSREL:55

for b₁ being Relation holds
( ( (id (dom (CL b₁))) * (b₁ \ (id (dom (CL b₁)))) = {} implies ( b₁ | (dom (CL b₁)) = id (dom (CL b₁)) & b₁ | (rng (CL b₁)) = id (dom (CL b₁)) ) ) & ( (b₁ \ (id (rng (CL b₁)))) * (id (rng (CL b₁))) = {} implies ( (dom (CL b₁)) | b₁ = id (dom (CL b₁)) & (rng (CL b₁)) | b₁ = id (rng (CL b₁)) ) ) )

proof end;

theorem Th56: :: SYSREL:56

for b₁ being Relation holds
( ( b₁ * (b₁ \ (id (dom b₁))) = {} implies (id (dom (CL b₁))) * (b₁ \ (id (dom (CL b₁)))) = {} ) & ( (b₁ \ (id (dom b₁))) * b₁ = {} implies (b₁ \ (id (dom (CL b₁)))) * (id (dom (CL b₁))) = {} ) )

proof end;

theorem Th57: :: SYSREL:57

for b₁, b₂ being Relation holds
( ( b₁ * b₂ = b₁ & b₂ * (b₂ \ (id (dom b₂))) = {} implies b₁ * (b₂ \ (id (dom b₂))) = {} ) & ( b₂ * b₁ = b₁ & (b₂ \ (id (dom b₂))) * b₂ = {} implies (b₂ \ (id (dom b₂))) * b₁ = {} ) )

proof end;

theorem Th58: :: SYSREL:58

for b₁, b₂ being Relation holds
( ( b₁ * b₂ = b₁ & b₂ * (b₂ \ (id (dom b₂))) = {} implies CL b₁ c= CL b₂ ) & ( b₂ * b₁ = b₁ & (b₂ \ (id (dom b₂))) * b₂ = {} implies CL b₁ c= CL b₂ ) )

proof end;

theorem Th59: :: SYSREL:59

for b₁, b₂ being Relation holds
( ( b₁ * b₂ = b₁ & b₂ * (b₂ \ (id (dom b₂))) = {} & b₂ * b₁ = b₂ & b₁ * (b₁ \ (id (dom b₁))) = {} implies CL b₁ = CL b₂ ) & ( b₂ * b₁ = b₁ & (b₂ \ (id (dom b₂))) * b₂ = {} & b₁ * b₂ = b₂ & (b₁ \ (id (dom b₁))) * b₁ = {} implies CL b₁ = CL b₂ ) )

proof end;