:: The Well Ordering Relations :: by Grzegorz Bancerek :: :: Received April 4, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for R being Relation holds ( R is reflexive iff for x being set st x in field R holds [x,x] in R ) proofend; Lm2: for R being Relation holds ( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds [x,z] in R ) proofend; Lm3: for R being Relation holds ( R is antisymmetric iff for x, y being set st [x,y] in R & [y,x] in R holds x = y ) proofend; Lm4: for R being Relation holds ( R is connected iff for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds [y,x] in R ) proofend; definition let R be Relation; let a be set ; funcR -Seg a -> set equals :: WELLORD1:def 1 (Coim (R,a)) \ {a}; coherence (Coim (R,a)) \ {a} is set ; end; :: deftheorem defines -Seg WELLORD1:def_1_:_ for R being Relation for a being set holds R -Seg a = (Coim (R,a)) \ {a}; theorem Th1: :: WELLORD1:1 for x, a being set for R being Relation holds ( x in R -Seg a iff ( x <> a & [x,a] in R ) ) proofend; theorem Th2: :: WELLORD1:2 for x being set for R being Relation holds ( x in field R or R -Seg x = {} ) proofend; definition let R be Relation; attrR is well_founded means :Def2: :: WELLORD1:def 2 for Y being set st Y c= field R & Y <> {} holds ex a being set st ( a in Y & R -Seg a misses Y ); let X be set ; predR is_well_founded_in X means :Def3: :: WELLORD1:def 3 for Y being set st Y c= X & Y <> {} holds ex a being set st ( a in Y & R -Seg a misses Y ); end; :: deftheorem Def2 defines well_founded WELLORD1:def_2_:_ for R being Relation holds ( R is well_founded iff for Y being set st Y c= field R & Y <> {} holds ex a being set st ( a in Y & R -Seg a misses Y ) ); :: deftheorem Def3 defines is_well_founded_in WELLORD1:def_3_:_ for R being Relation for X being set holds ( R is_well_founded_in X iff for Y being set st Y c= X & Y <> {} holds ex a being set st ( a in Y & R -Seg a misses Y ) ); theorem Th3: :: WELLORD1:3 for R being Relation holds ( R is well_founded iff R is_well_founded_in field R ) proofend; definition let R be Relation; attrR is well-ordering means :Def4: :: WELLORD1:def 4 ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ); let X be set ; predR well_orders X means :Def5: :: WELLORD1:def 5 ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ); end; :: deftheorem Def4 defines well-ordering WELLORD1:def_4_:_ for R being Relation holds ( R is well-ordering iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) ); :: deftheorem Def5 defines well_orders WELLORD1:def_5_:_ for R being Relation for X being set holds ( R well_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) ); registration cluster Relation-like well-ordering -> reflexive antisymmetric connected transitive well_founded for set ; coherence for b1 being Relation st b1 is well-ordering holds ( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) by Def4; cluster Relation-like reflexive antisymmetric connected transitive well_founded -> well-ordering for set ; coherence for b1 being Relation st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded holds b1 is well-ordering by Def4; end; theorem :: WELLORD1:4 for R being Relation holds ( R well_orders field R iff R is well-ordering ) proofend; theorem :: WELLORD1:5 for X being set for R being Relation st R well_orders X holds for Y being set st Y c= X & Y <> {} holds ex a being set st ( a in Y & ( for b being set st b in Y holds [a,b] in R ) ) proofend; theorem Th6: :: WELLORD1:6 for R being Relation st R is well-ordering holds for Y being set st Y c= field R & Y <> {} holds ex a being set st ( a in Y & ( for b being set st b in Y holds [a,b] in R ) ) proofend; theorem :: WELLORD1:7 for R being Relation st R is well-ordering & field R <> {} holds ex a being set st ( a in field R & ( for b being set st b in field R holds [a,b] in R ) ) by Th6; theorem :: WELLORD1:8 for R being Relation st R is well-ordering holds for a being set holds ( not a in field R or for b being set st b in field R holds [b,a] in R or ex b being set st ( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds [b,c] in R ) ) ) proofend; theorem Th9: :: WELLORD1:9 for a being set for R being Relation holds R -Seg a c= field R proofend; definition let R be Relation; let Y be set ; funcR |_2 Y -> Relation equals :: WELLORD1:def 6 R /\ [:Y,Y:]; coherence R /\ [:Y,Y:] is Relation ; end; :: deftheorem defines |_2 WELLORD1:def_6_:_ for R being Relation for Y being set holds R |_2 Y = R /\ [:Y,Y:]; theorem Th10: :: WELLORD1:10 for X being set for R being Relation holds R |_2 X = (X |` R) | X proofend; theorem Th11: :: WELLORD1:11 for X being set for R being Relation holds R |_2 X = X |` (R | X) proofend; Lm5: for X being set for R being Relation holds dom (X |` R) c= dom R proofend; theorem Th12: :: WELLORD1:12 for x, X being set for R being Relation st x in field (R |_2 X) holds ( x in field R & x in X ) proofend; theorem Th13: :: WELLORD1:13 for X being set for R being Relation holds ( field (R |_2 X) c= field R & field (R |_2 X) c= X ) proofend; theorem Th14: :: WELLORD1:14 for X, a being set for R being Relation holds (R |_2 X) -Seg a c= R -Seg a proofend; theorem Th15: :: WELLORD1:15 for X being set for R being Relation st R is reflexive holds R |_2 X is reflexive proofend; theorem Th16: :: WELLORD1:16 for Y being set for R being Relation st R is connected holds R |_2 Y is connected proofend; theorem Th17: :: WELLORD1:17 for Y being set for R being Relation st R is transitive holds R |_2 Y is transitive proofend; theorem Th18: :: WELLORD1:18 for Y being set for R being Relation st R is antisymmetric holds R |_2 Y is antisymmetric proofend; theorem Th19: :: WELLORD1:19 for X, Y being set for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y) proofend; theorem :: WELLORD1:20 for X, Y being set for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X proofend; theorem :: WELLORD1:21 for Y being set for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y proofend; theorem Th22: :: WELLORD1:22 for Z, Y being set for R being Relation st Z c= Y holds (R |_2 Y) |_2 Z = R |_2 Z proofend; theorem Th23: :: WELLORD1:23 for R being Relation holds R |_2 (field R) = R proofend; theorem Th24: :: WELLORD1:24 for X being set for R being Relation st R is well_founded holds R |_2 X is well_founded proofend; theorem Th25: :: WELLORD1:25 for Y being set for R being Relation st R is well-ordering holds R |_2 Y is well-ordering proofend; theorem Th26: :: WELLORD1:26 for a, b being set for R being Relation st R is well-ordering holds R -Seg a,R -Seg b are_c=-comparable proofend; theorem Th27: :: WELLORD1:27 for b, a being set for R being Relation st R is well-ordering & b in R -Seg a holds (R |_2 (R -Seg a)) -Seg b = R -Seg b proofend; theorem Th28: :: WELLORD1:28 for Y being set for R being Relation st R is well-ordering & Y c= field R holds ( ( Y = field R or ex a being set st ( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds for b being set st [b,a] in R holds b in Y ) proofend; theorem Th29: :: WELLORD1:29 for a, b being set for R being Relation st R is well-ordering & a in field R & b in field R holds ( [a,b] in R iff R -Seg a c= R -Seg b ) proofend; theorem Th30: :: WELLORD1:30 for a, b being set for R being Relation st R is well-ordering & a in field R & b in field R holds ( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) ) proofend; theorem Th31: :: WELLORD1:31 for X being set for R being Relation st R is well-ordering & X c= field R holds field (R |_2 X) = X proofend; theorem Th32: :: WELLORD1:32 for a being set for R being Relation st R is well-ordering holds field (R |_2 (R -Seg a)) = R -Seg a proofend; theorem Th33: :: WELLORD1:33 for R being Relation st R is well-ordering holds for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds a in Z ) holds field R c= Z proofend; theorem Th34: :: WELLORD1:34 for a, b being set for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds ( [c,b] in R & c <> b ) ) holds [a,b] in R proofend; theorem Th35: :: WELLORD1:35 for R being Relation for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being set st [a,b] in R & a <> b holds ( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds for a being set st a in field R holds [a,(F . a)] in R proofend; definition let R, S be Relation; let F be Function; predF is_isomorphism_of R,S means :Def7: :: WELLORD1:def 7 ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds ( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ); end; :: deftheorem Def7 defines is_isomorphism_of WELLORD1:def_7_:_ for R, S being Relation for F being Function holds ( F is_isomorphism_of R,S iff ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds ( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) ); theorem Th36: :: WELLORD1:36 for R, S being Relation for F being Function st F is_isomorphism_of R,S holds for a, b being set st [a,b] in R & a <> b holds ( [(F . a),(F . b)] in S & F . a <> F . b ) proofend; definition let R, S be Relation; predR,S are_isomorphic means :Def8: :: WELLORD1:def 8 ex F being Function st F is_isomorphism_of R,S; end; :: deftheorem Def8 defines are_isomorphic WELLORD1:def_8_:_ for R, S being Relation holds ( R,S are_isomorphic iff ex F being Function st F is_isomorphism_of R,S ); theorem Th37: :: WELLORD1:37 for R being Relation holds id (field R) is_isomorphism_of R,R proofend; theorem :: WELLORD1:38 for R being Relation holds R,R are_isomorphic proofend; theorem Th39: :: WELLORD1:39 for R, S being Relation for F being Function st F is_isomorphism_of R,S holds F " is_isomorphism_of S,R proofend; theorem Th40: :: WELLORD1:40 for R, S being Relation st R,S are_isomorphic holds S,R are_isomorphic proofend; theorem Th41: :: WELLORD1:41 for R, S, T being Relation for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of S,T holds G * F is_isomorphism_of R,T proofend; theorem Th42: :: WELLORD1:42 for R, S, T being Relation st R,S are_isomorphic & S,T are_isomorphic holds R,T are_isomorphic proofend; theorem Th43: :: WELLORD1:43 for R, S being Relation for F being Function st F is_isomorphism_of R,S holds ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) ) proofend; theorem Th44: :: WELLORD1:44 for R, S being Relation for F being Function st R is well-ordering & F is_isomorphism_of R,S holds S is well-ordering proofend; theorem Th45: :: WELLORD1:45 for R, S being Relation st R is well-ordering holds for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds F = G proofend; definition let R, S be Relation; assume that A1: R is well-ordering and A2: R,S are_isomorphic ; func canonical_isomorphism_of (R,S) -> Function means :Def9: :: WELLORD1:def 9 it is_isomorphism_of R,S; existence ex b1 being Function st b1 is_isomorphism_of R,S by A2, Def8; uniqueness for b1, b2 being Function st b1 is_isomorphism_of R,S & b2 is_isomorphism_of R,S holds b1 = b2 by A1, Th45; end; :: deftheorem Def9 defines canonical_isomorphism_of WELLORD1:def_9_:_ for R, S being Relation st R is well-ordering & R,S are_isomorphic holds for b3 being Function holds ( b3 = canonical_isomorphism_of (R,S) iff b3 is_isomorphism_of R,S ); theorem Th46: :: WELLORD1:46 for R being Relation st R is well-ordering holds for a being set st a in field R holds not R,R |_2 (R -Seg a) are_isomorphic proofend; theorem Th47: :: WELLORD1:47 for a, b being set for R being Relation st R is well-ordering & a in field R & b in field R & a <> b holds not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic proofend; theorem Th48: :: WELLORD1:48 for Z being set for R, S being Relation for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic ) proofend; theorem Th49: :: WELLORD1:49 for R, S being Relation for F being Function st F is_isomorphism_of R,S holds for a being set st a in field R holds ex b being set st ( b in field S & F .: (R -Seg a) = S -Seg b ) proofend; theorem Th50: :: WELLORD1:50 for R, S being Relation for F being Function st R is well-ordering & F is_isomorphism_of R,S holds for a being set st a in field R holds ex b being set st ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) proofend; theorem Th51: :: WELLORD1:51 for a, b, c being set for R, S being Relation st R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic holds ( S -Seg c c= S -Seg b & [c,b] in S ) proofend; theorem Th52: :: WELLORD1:52 for R, S being Relation st R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being set holds ( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) holds ex a being set st ( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) proofend; theorem :: WELLORD1:53 for Y being set for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds ex a being set st ( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic ) proofend; :: from AMISTD_3, 2010.01.10, A.T. theorem :: WELLORD1:54 for R, S being Relation st R,S are_isomorphic & R is well-ordering holds S is well-ordering proofend;