Copyright (c) 1989 Association of Mizar Users
environ vocabulary RELAT_1, SETFAM_1, ARYTM_1, BOOLE, RELAT_2, LATTICES, FINSEQ_1, FUNCT_1, TARSKI, EQREL_1, PARTFUN1, TOLER_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, FINSEQ_1, FUNCT_1, NAT_1, PARTFUN1; constructors RELAT_2, SETFAM_1, FINSEQ_1, REAL_1, NAT_1, XREAL_0, MEMBERED, PARTFUN1, ORDERS_1, XBOOLE_0; clusters RELSET_1, FINSEQ_1, SUBSET_1, XREAL_0, ARYTM_3, ZFMISC_1, PARTFUN1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, RELAT_2, XBOOLE_0, PARTFUN1; theorems RELAT_1, RELAT_2, AXIOMS, RELSET_1, SETFAM_1, ZFMISC_1, TARSKI, FINSEQ_1, NAT_1, REAL_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, ORDERS_1, PARTFUN1; schemes SETFAM_1, RELSET_1, FINSEQ_1, NAT_1; begin reserve X,Y,Z,x,y,y1,y2,z for set; reserve i,j,k for Nat; reserve A,B,C for Subset of X; reserve R,R1,R2 for Relation of X; reserve AX for Subset of [:X,X:]; reserve SFXX for Subset-Family of [:X,X:]; :: Auxiliary theorems theorem Th1: i < j implies j - i is Nat proof defpred P[Nat] means i < $1 implies $1 - i is Nat; A1: P[0] by NAT_1:18; A2: now let j; assume A3: P[j]; thus P[j+1] proof assume i < j + 1; then A4: i <= j by NAT_1:38; A5: j + 1 - i = (j - i) + 1 by XCMPLX_1:29; now per cases by A4,REAL_1:def 5; suppose i = j; then j + 1 - i = 0 + 1 by A5,XCMPLX_1:14; hence j + 1 - i is Nat; suppose i < j; then reconsider k = j - i as Nat by A3; j - i + 1 = k + 1; hence j + 1 - i is Nat by XCMPLX_1:29; end; hence j + 1 - i is Nat; end; end; for j holds P[j] from Ind(A1,A2); hence thesis; end; :: Equivalence Relation and its properties definition let X; func nabla X -> Relation of X equals :Def1: [:X,X:]; coherence by RELSET_1:def 1; end; definition let X; cluster nabla X -> total reflexive; coherence proof thus dom nabla X c= X; thus X c= dom nabla X proof let x be set; assume x in X; then [x,x] in [:X,X:] by ZFMISC_1:106; then [x,x] in nabla X by Def1; hence x in dom nabla X by RELAT_1:def 4; end; let x; assume x in field nabla X; then x in dom nabla X \/ rng nabla X by RELAT_1:def 6; then [x,x] in [:X,X:] by ZFMISC_1:106; hence [x,x] in nabla X by Def1; end; end; definition let X; let R1,R2; redefine func R1 /\ R2 -> Relation of X; coherence proof R1 /\ R2 c= [:X,X:]; hence thesis; end; func R1 \/ R2 -> Relation of X; coherence proof R1 \/ R2 c= [:X,X:]; hence thesis; end; end; canceled 2; theorem id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X proof thus for x st x in X holds [x,x] in id X by RELAT_1:def 10; thus for x,y st x in X & y in X & [x,y] in id X holds [y,x] in id X proof let x,y; assume x in X & y in X & [x,y] in id X; then y in X & x in X & y = x by RELAT_1:def 10; hence thesis by RELAT_1:def 10; end; thus for x,y,z st x in X & y in X & z in X & [x,y] in id X & [y,z] in id X holds [x,z] in id X by RELAT_1:def 10; end; definition let X; mode Tolerance of X is total reflexive symmetric Relation of X; mode Equivalence_Relation of X is total symmetric transitive Relation of X; end; canceled; theorem id X is Equivalence_Relation of X; theorem Th7: nabla X is Equivalence_Relation of X proof A1: nabla X = [:X,X:] by Def1; A2: nabla X is_symmetric_in X proof for x,y holds x in X & y in X & [x,y] in nabla X implies [y,x] in nabla X by A1,ZFMISC_1:107; hence thesis by RELAT_2:def 3; end; A3: nabla X is_transitive_in X proof for x,y,z st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in nabla X holds [x,z] in nabla X by A1,ZFMISC_1:106; hence thesis by RELAT_2:def 8; end; field nabla X = X by ORDERS_1:97; hence thesis by A2,A3,RELAT_2:def 11,def 16; end; definition let X; cluster nabla X -> total symmetric transitive; coherence by Th7; end; reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X; Lm1: [x,y] in R implies x in X & y in X proof assume [x,y] in R; then x in dom R & y in rng R by RELAT_1:20; hence thesis; end; canceled 3; LemA: for X being set, R being total Relation of X holds field R = X proof let X be set, R be total Relation of X; dom R = X by PARTFUN1:def 4; hence field R = X \/ rng R by RELAT_1:def 6 .= X by XBOOLE_1:12; end; theorem Th11: for R being total reflexive Relation of X holds x in X implies [x,x] in R proof let R be total reflexive Relation of X; field R = X by ORDERS_1:97; then R is_reflexive_in X by RELAT_2:def 9; hence thesis by RELAT_2:def 1; end; theorem Th12: for R being total symmetric Relation of X holds [x,y] in R implies [y,x] in R proof let R be total symmetric Relation of X; A1: field R = X by LemA; assume [x,y] in R; then A2: x in X & y in X & [x,y] in R by Lm1; R is_symmetric_in X by A1,RELAT_2:def 11; hence thesis by A2,RELAT_2:def 3; end; theorem Th13: for R being total transitive Relation of X holds [x,y] in R & [y,z] in R implies [x,z] in R proof let R be total transitive Relation of X; A1: field R = X by LemA; assume [x,y] in R & [y,z] in R; then A2: x in X & y in X & z in X & [x,y] in R & [y,z] in R by Lm1; R is_transitive_in X by A1,RELAT_2:def 16; hence thesis by A2,RELAT_2:def 8; end; theorem for R being total reflexive Relation of X holds (ex x being set st x in X) implies R <> {} by Th11; theorem for R being total Relation of X holds field R = X by LemA; theorem Th16: R is Equivalence_Relation of X iff R is reflexive symmetric transitive & field R = X proof thus R is Equivalence_Relation of X implies R is reflexive symmetric transitive & field R = X by LemA; assume A1: R is reflexive & R is symmetric & R is transitive & field R = X; then R is_reflexive_in X by RELAT_2:def 9; then dom R = X by ORDERS_1:98; hence thesis by A1,PARTFUN1:def 4; end; definition let X; let EqR1,EqR2; redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X; coherence proof A1: field (EqR1 /\ EqR2) = X proof A2: for x st x in X holds [x,x] in EqR1 by Th11; for x st x in X holds [x,x] in EqR2 by Th11; then id X c= EqR1 & id X c= EqR2 by A2,RELAT_1:73; then id X c= EqR1 /\ EqR2 by XBOOLE_1:19; then dom(EqR1 /\ EqR2) = X & rng(EqR1 /\ EqR2) = X by RELSET_1:31,32; then field (EqR1 /\ EqR2) = X \/ X by RELAT_1:def 6; hence thesis; end; A3: EqR1 /\ EqR2 is reflexive by RELAT_2:31; A4: EqR1 /\ EqR2 is symmetric by RELAT_2:35; EqR1 /\ EqR2 is transitive by RELAT_2:43; hence thesis by A1,A3,A4,Th16; end; end; theorem id X /\ EqR = id X proof now let x,y; assume [x,y] in id X; then x in X & x = y by RELAT_1:def 10; hence [x,y] in EqR by Th11; end; then id X c= EqR by RELAT_1:def 3; hence thesis by XBOOLE_1:28; end; theorem Th18: nabla X /\ R = R proof [:X,X:] = nabla X by Def1; hence thesis by XBOOLE_1:28; end; theorem Th19: for SFXX st (SFXX <> {} & for Y st Y in SFXX holds Y is Equivalence_Relation of X) holds meet SFXX is Equivalence_Relation of X proof let SFXX such that A1: SFXX <> {} and A2: for Y st Y in SFXX holds Y is Equivalence_Relation of X; reconsider XX = meet SFXX as Relation of X by RELSET_1:def 1; A3: XX is_reflexive_in X proof let x such that A4: x in X; for Y st Y in SFXX holds [x,x] in Y proof let Y; assume Y in SFXX; then Y is Equivalence_Relation of X by A2; hence thesis by A4,Th11; end; hence thesis by A1,SETFAM_1:def 1; end; A5: XX is_symmetric_in X proof let x,y; assume A6: x in X & y in X & [x,y] in XX; now let Y; assume A7: Y in SFXX; then A8: Y is Equivalence_Relation of X by A2; [x,y] in Y by A6,A7,SETFAM_1:def 1; hence [y,x] in Y by A8,Th12; end; hence thesis by A1,SETFAM_1:def 1; end; A9: XX is_transitive_in X proof let x,y,z; assume A10: x in X & y in X & z in X & [x,y] in XX & [y,z] in XX; now let Y; assume A11: Y in SFXX; then A12: Y is Equivalence_Relation of X by A2; [x,y] in Y & [y,z] in Y by A10,A11,SETFAM_1:def 1; hence [x,z] in Y by A12,Th13; end; hence thesis by A1,SETFAM_1:def 1; end; A13: field XX = X by A3,ORDERS_1:98; dom XX = X by A3,ORDERS_1:98; hence thesis by A5,A9,A13,RELAT_2:def 11,def 16,PARTFUN1:def 4; end; theorem Th20: for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2 proof let R; defpred P[set] means $1 is Equivalence_Relation of X & R c= $1; consider F being Subset-Family of [:X,X:] such that A1: for AX holds AX in F iff P[AX] from SubFamEx; nabla X /\ R = R by Th18; then R c= nabla X by XBOOLE_1:17; then A2: F <> {} by A1; for Y st Y in F holds Y is Equivalence_Relation of X by A1; then reconsider EqR = meet F as Equivalence_Relation of X by A2,Th19; take EqR; A3: for Y st Y in F holds R c= Y by A1; now let EqR2; assume R c= EqR2; then EqR2 in F by A1; hence EqR c= EqR2 by SETFAM_1:4; end; hence thesis by A2,A3,SETFAM_1:6; end; definition let X; let EqR1,EqR2; canceled; func EqR1 "\/" EqR2 -> Equivalence_Relation of X means :Def3: EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR; existence by Th20; uniqueness proof let R1,R2 be Equivalence_Relation of X such that A1: EqR1 \/ EqR2 c= R1 & for EqR st EqR1 \/ EqR2 c= EqR holds R1 c= EqR and A2: EqR1 \/ EqR2 c= R2 & for EqR st EqR1 \/ EqR2 c= EqR holds R2 c= EqR; A3: R1 c= R2 by A1,A2; R2 c= R1 by A1,A2; hence thesis by A3,XBOOLE_0:def 10; end; end; canceled; theorem EqR "\/" EqR = EqR proof for EqR3 st EqR \/ EqR c= EqR3 holds EqR c= EqR3; hence thesis by Def3; end; theorem Th23:EqR1 "\/" EqR2 = EqR2 "\/" EqR1 proof for EqR3 holds EqR3 = EqR1 "\/" EqR2 implies EqR3 = EqR2 "\/" EqR1 proof let EqR3; assume A1: EqR3 = EqR1 "\/" EqR2; then A2: EqR2 \/ EqR1 c= EqR3 by Def3; for EqR st EqR2 \/ EqR1 c= EqR holds EqR3 c= EqR by A1,Def3; hence thesis by A2,Def3; end; hence thesis; end; definition let X; let EqR1,EqR2; redefine func EqR1 "\/" EqR2; commutativity by Th23; end; theorem EqR1 /\ (EqR1 "\/" EqR2) = EqR1 proof thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17; A1: EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7; EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def3; then EqR1 c= EqR1 "\/" EqR2 by A1,XBOOLE_1:1; hence thesis by XBOOLE_1:19; end; theorem EqR1 "\/" (EqR1 /\ EqR2) = EqR1 proof A1: EqR1 = EqR1 \/ (EqR1 /\ EqR2) by XBOOLE_1:22; for EqR st EqR1 \/ (EqR1 /\ EqR2) c= EqR holds EqR1 c= EqR by XBOOLE_1:22; hence thesis by A1,Def3; end; scheme Ex_Eq_Rel {X() -> set,P[set,set]}: ex EqR being Equivalence_Relation of X() st for x,y holds [x,y] in EqR iff x in X() & y in X() & P[x,y] provided A1: for x st x in X() holds P[x,x] and A2: for x,y st P[x,y] holds P[y,x] and A3: for x,y,z st P[x,y] & P[y,z] holds P[x,z] proof defpred R[set,set] means P[$1,$2]; consider Y being Relation of X(),X() such that A4: for x,y holds [x,y] in Y iff x in X() & y in X() & R[x,y] from Rel_On_Set_Ex; A5: Y is_reflexive_in X() proof let x; assume A6: x in X(); then P[x,x] by A1; hence thesis by A4,A6; end; A7: Y is_symmetric_in X() proof let x,y; assume A8: x in X() & y in X() & [x,y] in Y; then P[x,y] by A4; then y in X() & x in X() & P[y,x] by A2,A8; hence thesis by A4; end; A9: Y is_transitive_in X() proof let x,y,z; assume A10: x in X() & y in X() & z in X() & [x,y] in Y & [y,z] in Y; then A11: P[x,y] by A4; P[y,z] by A4,A10; then P[x,z] by A3,A11; hence thesis by A4,A10; end; A12: field Y = X() by A5,ORDERS_1:98; dom Y = X() by A5,ORDERS_1:98; then reconsider R1 = Y as Equivalence_Relation of X() by A7,A9,A12,RELAT_2:def 11,def 16,PARTFUN1:def 4; take R1; thus thesis by A4; end; :: Classes of abstraction definition let X be set, R be Tolerance of X, x be set; func Class(R,x) -> Subset of X equals :Def4: R.:{x}; correctness; end; canceled; theorem Th27: for R being Tolerance of X holds y in Class (R,x) iff [y,x] in R proof let R be Tolerance of X; thus y in Class(R,x) implies [y,x] in R proof assume y in Class(R,x); then y in R.:{x} by Def4; then ex z being set st [z,y] in R & z in {x} by RELAT_1:def 13; then [x,y] in R by TARSKI:def 1; hence [y,x] in R by Th12; end; assume [y,x] in R; then A1: [x,y] in R by Th12; x in {x} by TARSKI:def 1; then y in R.:{x} by A1,RELAT_1:def 13; hence thesis by Def4; end; theorem Th28: for R being Tolerance of X holds for x st x in X holds x in Class (R,x) proof let R be Tolerance of X; let x; assume x in X; then [x,x] in R by Th11; hence thesis by Th27; end; theorem for R being Tolerance of X holds for x st x in X holds ex y st x in Class(R,y) proof let R be Tolerance of X; let x; assume x in X; then x in Class(R,x) by Th28; hence thesis; end; theorem for R being transitive Tolerance of X holds y in Class(R,x) & z in Class(R,x) implies [y,z] in R proof let R be transitive Tolerance of X; assume y in Class(R,x) & z in Class(R,x); then [y,x] in R & [z,x] in R by Th27; then [y,x] in R & [x,z] in R by Th12; hence thesis by Th13; end; Lm2: for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y) proof let x such that A1: x in X; thus [x,y] in EqR implies Class(EqR,x) = Class(EqR,y) proof assume A2: [x,y] in EqR; now let z; assume z in Class(EqR,x); then [z,x] in EqR by Th27; then [z,y] in EqR by A2,Th13; hence z in Class(EqR,y) by Th27; end; then A3: Class(EqR,x) c= Class(EqR,y) by TARSKI:def 3; now let z; assume z in Class(EqR,y); then A4: [z,y] in EqR by Th27; [y,x] in EqR by A2,Th12; then [z,x] in EqR by A4,Th13; hence z in Class(EqR,x) by Th27; end; then Class(EqR,y) c= Class(EqR,x) by TARSKI:def 3; hence thesis by A3,XBOOLE_0:def 10; end; assume Class(EqR,x) = Class(EqR,y); then x in Class(EqR,y) by A1,Th28; hence thesis by Th27; end; theorem Th31: for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class(EqR,y) proof let x such that A1: x in X; thus y in Class(EqR,x) implies Class(EqR,x) = Class(EqR,y) proof assume y in Class(EqR,x); then [y,x] in EqR by Th27; then [x,y] in EqR by Th12; hence thesis by A1,Lm2; end; assume Class(EqR,x) = Class(EqR,y); then [x,y] in EqR by A1,Lm2; then [y,x] in EqR by Th12; hence thesis by Th27; end; theorem Th32: for x,y st x in X & y in X holds Class(EqR,x) = Class(EqR,y) or Class(EqR,x) misses Class(EqR,y) proof let x,y; assume A1: x in X & y in X; A2: [x,y] in EqR implies Class(EqR,x) = Class(EqR,y) proof assume [x,y] in EqR; then x in Class(EqR,y) by Th27; hence thesis by A1,Th31; end; not [x,y] in EqR implies Class(EqR,x) misses Class(EqR,y) proof assume A3: not [x,y] in EqR; assume Class(EqR,x) meets Class(EqR,y); then consider z such that A4: z in Class(EqR,x) & z in Class(EqR,y) by XBOOLE_0:3; [z,x] in EqR & [z,y] in EqR by A4,Th27; then [x,z] in EqR & [z,y] in EqR by Th12; hence contradiction by A3,Th13; end; hence thesis by A2; end; theorem for x st x in X holds Class(id X,x) = {x} proof let x; assume A1: x in X; now let y; assume y in Class(id X,x); then [y,x] in id X by Th27; hence y = x by RELAT_1:def 10; end; then for y holds y in Class(id X,x) iff y = x by A1,Th28; hence thesis by TARSKI:def 1; end; theorem Th34: for x st x in X holds Class(nabla X,x) = X proof let x such that A1: x in X; now let y; assume y in X; then [y,x] in [:X,X:] by A1,ZFMISC_1:106; then [y,x] in nabla X by Def1; hence y in Class(nabla X,x) by Th27; end; then for y holds y in X iff y in Class(nabla X,x); hence thesis by TARSKI:2; end; theorem Th35: (ex x st Class(EqR,x) = X) implies EqR = nabla X proof given x such that A1: Class(EqR,x) = X; now let y,z; assume [y,z] in [:X,X:]; then y in Class(EqR,x) & z in Class(EqR,x) by A1,ZFMISC_1:106; then [y,x] in EqR & [z,x] in EqR by Th27; then [y,x] in EqR & [x,z] in EqR by Th12; hence [y,z] in EqR by Th13; end; then [:X,X:] c= EqR by ZFMISC_1:109; then [:X,X:] = EqR by XBOOLE_0:def 10; hence thesis by Def1; end; theorem x in X implies ([x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st 1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2) proof assume A1: x in X; thus [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st 1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 proof assume A2: [x,y] in EqR1 "\/" EqR2; defpred P[set,set] means ex f being FinSequence st (1 <= len f & $1 = f.1 & $2 = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2); consider Y being Relation of X,X such that A3: for x,y holds [x,y] in Y iff x in X & y in X & P[x,y] from Rel_On_Set_Ex; A4: Y is_reflexive_in X proof let x such that A5: x in X; set g = <*x*>; A6: len g = 1 & g.1 = x by FINSEQ_1:57; for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 by FINSEQ_1:57; hence thesis by A3,A5,A6; end; A7: Y is_symmetric_in X proof let x,y; assume A8: x in X & y in X & [x,y] in Y; then consider f being FinSequence such that A9: (1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2) by A3; defpred P[Nat,set] means $2 = f.(1 + (len f) - $1); A10: for k,y1,y2 st k in Seg(len f) & P[k,y1] & P[k,y2] holds y1 =y2; A11: for k st k in Seg(len f) ex z st P[k,z]; consider g being FinSequence such that A12: dom g = Seg(len f) & for k st k in Seg(len f) holds P[k,g.k] from SeqEx(A10,A11); A13: len f = len g by A12,FINSEQ_1:def 3; A14: 1 <= len g by A9,A12,FINSEQ_1:def 3; A15: now 1 in Seg(len f) by A9,FINSEQ_1:3; then g.1 = f.((len f) + 1 - 1) by A12 .= f.((len f) + (1 - 1)) by XCMPLX_1:29 .= f.(len f); hence y = g.1 by A9; end; A16: now len f in Seg(len f) by A9,FINSEQ_1:3; then g.(len f) = f.(1 + (len f) - len f) by A12 .= f.(1 + (len f - (len f))) by XCMPLX_1:29 .= f.(1 + 0) by XCMPLX_1:14; hence x = g.(len g) by A9,A12,FINSEQ_1:def 3; end; for j st 1 <= j & j < len g holds [g.j,g.(j+1)] in EqR1 \/ EqR2 proof let j; assume A17: 1 <= j & j < len g; then j in Seg(len f) by A13,FINSEQ_1:3; then A18: g.j = f.(1 + (len f) - j) by A12 .= f.(((len f) - j) + 1) by XCMPLX_1:29; A19: 1 <= (j + 1) by NAT_1:37; (j + 1) <= len f by A13,A17,NAT_1:38; then (j + 1) in Seg(len f) by A19,FINSEQ_1:3; then A20: g.(j + 1) = f.((len f) + 1 - (1 + j)) by A12 .= f.((len f) + 1 - 1 - j) by XCMPLX_1:36 .= f.((len f) + (1 - 1) - j) by XCMPLX_1:29 .= f.((len f) - j); reconsider k = (len f) - j as Nat by A13,A17,Th1; j - (len f) < (len f) - (len f) by A13,A17,REAL_1:54; then - ((len f) - j) < (len f) - (len f) by XCMPLX_1:143; then - ((len f) - j) < - 0 by XCMPLX_1:14; then 0 < k by REAL_1:50; then A21: 0 + 1 <= k by NAT_1:38; 0 + 1 <= j by A17; then 0 < j by NAT_1:38; then - j < 0 by REAL_1:26,50; then (len f) + (- j) < 0 + (len f) by REAL_1:53; then (len f) - j < len f by XCMPLX_0:def 8; then A22: [f.k,f.(k + 1)] in EqR1 \/ EqR2 by A9,A21; now per cases by A22,XBOOLE_0:def 2; suppose [f.k,f.(k + 1)] in EqR1; then [f.(k + 1),f.k] in EqR1 by Th12; hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 2; suppose [f.k,f.(k + 1)] in EqR2; then [f.(k + 1),f.k] in EqR2 by Th12; hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 2; end; hence thesis by A18,A20; end; hence thesis by A3,A8,A14,A15,A16; end; A23: Y is_transitive_in X proof let x,y,z; assume A24: x in X & y in X & z in X & [x,y] in Y & [y,z] in Y; then consider f being FinSequence such that A25: (1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2) by A3; consider g being FinSequence such that A26: (1 <= len g & y = g.1 & z = g.(len g) & for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2) by A3,A24; set h = f^g; A27:len h = len f + len g by FINSEQ_1:35; then A28: 1 <= len h by A25,NAT_1:37; 1 in Seg(len f) by A25,FINSEQ_1:3; then 1 in dom f by FINSEQ_1:def 3; then A29: x = h.1 by A25,FINSEQ_1:def 7; A30: len f + 1 <= len f + len g by A26,REAL_1:55; then A31: h.(len h) = g.(len g + len f - len f) by A27,FINSEQ_1:36 .= g.(len g + (len f - len f)) by XCMPLX_1:29 .= g.(len g + 0) by XCMPLX_1:14 .= g.(len g); for i st 1 <= i & i < len h holds [h.i,h.(i+1)] in EqR1 \/ EqR2 proof let i; assume A32: 1 <= i & i < len h; then A33: (1 <= i & i < len f) or i = len f or len f < i by REAL_1:def 5; now per cases by A32,A33,NAT_1:38; suppose A34: (1 <= i & i < len f); then i in Seg(len f) by FINSEQ_1:3; then i in dom f by FINSEQ_1:def 3; then A35: h.i = f.i by FINSEQ_1:def 7; (1 <= i + 1 & i + 1 <= len f) by A34,NAT_1:38; then i + 1 in Seg(len f) by FINSEQ_1:3; then i + 1 in dom f by FINSEQ_1:def 3; then h.(i + 1) = f.(i + 1) by FINSEQ_1:def 7; hence [h.i,h.(i+1)] in EqR1 \/ EqR2 by A25,A34,A35; suppose A36: i = len f; len f in Seg(len f) by A25,FINSEQ_1:3; then len f in dom f by FINSEQ_1:def 3; then A37: h.i = y by A25,A36,FINSEQ_1:def 7; A38: h.(i + 1) = g.(1 + len f - len f) by A30,A36,FINSEQ_1:36 .= g.(1 + (len f - len f)) by XCMPLX_1:29 .= g.(1 + 0) by XCMPLX_1:14 .= y by A26; [y,y] in EqR1 by A24,Th11; hence [h.i,h.(i+1)] in EqR1 \/ EqR2 by A37,A38,XBOOLE_0:def 2; suppose A39: (len f + 1 <= i & i < len h); then (len f + 1 <= i + 1 & i + 1 <= len f + len g) by A27,NAT_1:38; then A40: h.(i + 1) = g.(1 + i - len f) by FINSEQ_1:36 .= g.((i - len f) + 1) by XCMPLX_1:29; 1 <= len f & len f < i by A25,A39,NAT_1:38; then reconsider k = i - len f as Nat by Th1; (1 + len f - len f <= i - len f & i < len f + len g) by A39,FINSEQ_1:35, REAL_1:49; then (1 + (len f - len f) <= i - len f & i < len f + len g) by XCMPLX_1:29 ; then (1 + 0 <= i - len f & i < len f + len g) by XCMPLX_1:14; then (1 <= i - len f & i - len f < len g) by REAL_1:84; then [g.k,g.(k + 1)] in EqR1 \/ EqR2 by A26; hence [h.i,h.(i+1)] in EqR1 \/ EqR2 by A27,A39,A40,FINSEQ_1:36; end; hence thesis; end; hence thesis by A3,A24,A26,A28,A29,A31; end; field Y = X & dom Y = X by A4,ORDERS_1:98; then reconsider R1 = Y as Equivalence_Relation of X by A7,A23,RELAT_2:def 11,def 16,PARTFUN1:def 4; for x,y holds [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 proof let x,y; assume A42: [x,y] in EqR1 \/ EqR2; then A43: x in X & y in X by Lm1; set g = <*x,y*>; A44: len g = 2 by FINSEQ_1:61; A45:len g = 1 + 1 by FINSEQ_1:61; A46: g.1 = x & g.2 = y by FINSEQ_1:61; A47: g.1 = x & g.(len g) = y by A44,FINSEQ_1:61; for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 proof let i; assume 1 <= i & i < len g; then 1 <= i & i <= 1 by A45,NAT_1:38; then 1 = i by AXIOMS:21; hence thesis by A42,A46; end; hence thesis by A3,A43,A45,A47; end; then EqR1 \/ EqR2 c= R1 by RELAT_1:def 3; then EqR1 "\/" EqR2 c= R1 by Def3; then consider f being FinSequence such that A48: 1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 by A2,A3; take f; thus thesis by A48; end; given f being FinSequence such that A49: 1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2; defpred P[Nat] means 1 <= $1 & $1 <= len f implies [f.1,f.$1] in EqR1 "\/" EqR2; for i holds P[i] proof A50:P[0]; A51:now let i; assume A52: P[i]; thus P[i+1] proof assume A53: 1 <= i + 1 & i + 1 <= len f; then A54: i < len f by NAT_1:38; 1 <= i or 1 = i + 1 by A53,NAT_1:26; then A55: 1 <= i or 1 - 1 = i by XCMPLX_1:26; A56: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def3; now per cases by A55; suppose A57: 1 <= i; then [f.i,f.(i+1)] in EqR1 \/ EqR2 by A49,A54; hence [f.1,f.(i+1)] in EqR1 "\/" EqR2 by A52,A53,A56,A57,Th13,NAT_1:38; suppose A58: 0 = i; [f.1,f.1] in EqR1 by A1,A49,Th11; then [f.1,f.1] in EqR1 \/ EqR2 by XBOOLE_0:def 2; hence [f.1,f.(i+1)] in EqR1 "\/" EqR2 by A56,A58; end; hence [f.1,f.(i + 1)] in EqR1 "\/" EqR2; end; end; thus thesis from Ind(A50,A51); end; hence thesis by A49; end; theorem Th37: for E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x) proof let E be Equivalence_Relation of X such that A1: E = EqR1 \/ EqR2; for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x) proof let x such that x in X; assume that A2: not Class(E,x) = Class(EqR1,x) and A3: not Class(E,x) = Class(EqR2,x); consider y such that A4: y in Class(E,x) & not y in Class(EqR1,x) or y in Class(EqR1,x) & not y in Class(E,x) by A2,TARSKI:2; A5: now assume that A6: y in Class(EqR1,x) and A7: not y in Class(E,x); [y,x] in EqR1 by A6,Th27; then [y,x] in E by A1,XBOOLE_0:def 2; hence contradiction by A7,Th27; end; consider z such that A8: z in Class(E,x) & not z in Class(EqR2,x) or z in Class(EqR2,x) & not z in Class(E,x) by A3,TARSKI:2; A9: now assume that A10: z in Class(EqR2,x) and A11: not z in Class(E,x); [z,x] in EqR2 by A10,Th27; then [z,x] in E by A1,XBOOLE_0:def 2; hence contradiction by A11,Th27; end; A12:[y,x] in E by A4,A5,Th27; not [y,x] in EqR1 by A4,A5,Th27; then A13:[y,x] in EqR2 by A1,A12,XBOOLE_0:def 2; A14:[z,x] in E by A8,A9,Th27; then [x,z] in E by Th12; then A15: [y,z] in E by A12,Th13; not [z,x] in EqR2 by A8,A9,Th27; then A16: [z,x] in EqR1 by A1,A14,XBOOLE_0:def 2; A17:now assume A18:[y,z] in EqR2; [x,y] in EqR2 by A13,Th12; then [x,z] in EqR2 by A18,Th13; then [z,x] in EqR2 by Th12; hence contradiction by A8,A9,Th27; end; now assume [y,z] in EqR1; then A19:[z,y] in EqR1 by Th12; [x,z] in EqR1 by A16,Th12; then [x,y] in EqR1 by A19,Th13; then [y,x] in EqR1 by Th12; hence contradiction by A4,A5,Th27; end; hence contradiction by A1,A15,A17,XBOOLE_0:def 2; end; hence thesis; end; theorem EqR1 \/ EqR2 = nabla X implies EqR1 = nabla X or EqR2 = nabla X proof assume A1: EqR1 \/ EqR2 = nabla X; A2: now assume X = {}; then [:X,X:] = {} by ZFMISC_1:113; then nabla X = {} by Def1; hence EqR1 = nabla X or EqR2 = nabla X by A1,XBOOLE_1:15; end; (not X = {}) implies EqR1 = nabla X or EqR2 = nabla X proof assume A3: X <> {}; consider y being Element of X; now let x; assume A4: x in X; then Class(nabla X,x) = Class(EqR1,x) or Class(nabla X,x) = Class(EqR2,x) by A1,Th37; hence Class(EqR1,x) = X or Class(EqR2,x) = X by A4,Th34; end; then Class(EqR1,y) = X or Class(EqR2,y) = X by A3; hence thesis by Th35; end; hence thesis by A2; end; definition let X; let EqR; func Class EqR -> Subset-Family of X means :Def5: A in it iff ex x st x in X & A = Class(EqR,x); existence proof defpred P[set] means ex x st x in X & $1 = Class(EqR,x); consider F being Subset-Family of X such that A1:for A holds A in F iff P[A] from SubFamEx; take F; thus thesis by A1; end; uniqueness proof let F1,F2 be Subset-Family of X; assume that A2: for A holds A in F1 iff ex x st x in X & A = Class(EqR,x) and A3: for A holds A in F2 iff ex x st x in X & A = Class(EqR,x); now let A; A in F1 iff ex x st x in X & A = Class(EqR,x) by A2; hence A in F1 iff A in F2 by A3; end; hence F1 = F2 by SETFAM_1:44; end; end; canceled; theorem Th40: X = {} implies Class EqR = {} proof assume that A1: X = {} and A2: Class EqR <> {}; consider z being Element of Class EqR; z is Subset of X by A2,TARSKI:def 3; then ex x st x in X & z = Class(EqR,x) by A2,Def5; hence contradiction by A1; end; definition let X; mode a_partition of X -> Subset-Family of X means :Def6: union it = X & for A st A in it holds A<>{} & for B st B in it holds A = B or A misses B if X <> {} otherwise it = {}; existence proof thus X <> {} implies ex F being Subset-Family of X st union F = X & for A st A in F holds A<>{} & for B st B in F holds A = B or A misses B proof assume X <> {}; defpred P[set] means ex x st x in X & $1 = {x}; consider F being Subset-Family of X such that A1: for A being Subset of X holds A in F iff P[A] from SubFamEx; A2: now let y; now assume A3: y in X; set Z = {y}; A4: y in Z by TARSKI:def 1; Z is Subset of X by A3,ZFMISC_1:37; then Z in F by A1,A3; hence ex Z st y in Z & Z in F by A4; end; hence y in X iff ex Z st y in Z & Z in F; end; A5: for A st A in F holds A<>{} & for B st B in F holds A = B or A misses B proof let A; assume A in F; then consider x such that A6: x in X & A = {x} by A1; thus A <> {} by A6; let B; assume B in F; then consider y such that A7: y in X & B = {y} by A1; now assume A8: (not x = y); for z st z in A holds not z in B proof let z; assume z in A; then not z = y by A6,A8,TARSKI:def 1; hence thesis by A7,TARSKI:def 1; end; hence A misses B by XBOOLE_0:3; end; hence thesis by A6,A7; end; take F; thus thesis by A2,A5,TARSKI:def 4; end; assume X = {}; {} c= bool X by XBOOLE_1:2; then {} is Subset-Family of X by SETFAM_1:def 7; hence thesis; end; consistency; end; canceled; theorem Class EqR is a_partition of X proof A1: X <> {} implies Class EqR is a_partition of X proof assume A2: X <> {}; now let x; now assume A3: x in X; consider Z such that A4: Z = Class(EqR,x); A5: x in Z by A3,A4,Th28; Z in Class EqR by A3,A4,Def5; hence ex Z st x in Z & Z in Class EqR by A5; end; hence x in X iff ex Z st x in Z & Z in Class EqR; end; then A6: union(Class EqR) = X by TARSKI:def 4; for A st A in Class EqR holds A<>{} & for B st B in Class EqR holds A = B or A misses B proof let A; assume A in Class EqR; then consider x such that A7: x in X & A = Class(EqR,x) by Def5; thus A <> {} by A7,Th28; let B; assume B in Class EqR; then ex y st y in X & B = Class(EqR,y) by Def5; hence thesis by A7,Th32; end; hence thesis by A2,A6,Def6; end; X = {} implies Class EqR is a_partition of X proof assume A8: X = {}; then Class EqR = {} by Th40; hence thesis by A8,Def6; end; hence thesis by A1; end; theorem for P being a_partition of X holds ex EqR st P = Class EqR proof let P be a_partition of X; A1: X <> {} implies ex EqR st P = Class EqR proof assume A2: X <> {}; then A3: union P = X by Def6; defpred P[set,set] means ex A st A in P & $1 in A & $2 in A; A4: for x st x in X holds P[x,x] proof let x; assume x in X; then consider Z such that A5: x in Z & Z in P by A3,TARSKI:def 4; reconsider A = Z as Subset of X by A5; take A; thus thesis by A5; end; A6: for x,y st P[x,y] holds P[y,x]; A7: for x,y,z st P[x,y] & P[y,z] holds P[x,z] proof let x,y,z; given A such that A8: A in P & x in A & y in A; given B such that A9: B in P & y in B & z in B; A = B or A misses B by A8,A9,Def6; hence thesis by A8,A9,XBOOLE_0:3; end; consider R being Equivalence_Relation of X such that A10: for x,y holds [x,y] in R iff x in X & y in X & P[x,y] from Ex_Eq_Rel(A4,A6,A7); take R; P = Class R proof now let A; A11: now assume A12: A in P; then A13: A <> {} by A2,Def6; consider x being Element of A; A14: x in X by A13,TARSKI:def 3; now let y; A15: now assume y in A; then [y,x] in R by A10,A12,A14; hence y in Class(R,x) by Th27; end; now assume y in Class(R,x); then [y,x] in R by Th27; then consider B such that A16: B in P & y in B & x in B by A10; A meets B by A13,A16,XBOOLE_0:3; hence y in A by A12,A16,Def6; end; hence y in A iff y in Class(R,x) by A15; end; then A = Class(R,x) by TARSKI:2; hence A in Class R by A14,Def5; end; now assume A in Class R; then consider x such that A17: x in X & A = Class(R,x) by Def5; x in Class(R,x) by A17,Th28; then [x,x] in R by Th27; then consider B such that A18: B in P & x in B & x in B by A10; A = B proof now let y; A19: now assume y in A; then [y,x] in R by A17,Th27; then consider C such that A20: C in P & y in C & x in C by A10; B meets C by A18,A20,XBOOLE_0:3; hence y in B by A18,A20,Def6; end; now assume y in B; then [y,x] in R by A10,A18; hence y in A by A17,Th27; end; hence y in A iff y in B by A19; end; hence thesis by TARSKI:2; end; hence A in P by A18; end; hence A in P iff A in Class R by A11; end; hence thesis by SETFAM_1:44; end; hence thesis; end; X = {} implies ex EqR st P = Class EqR proof assume A21: X = {}; then A22: P = {} by Def6; consider EqR1; take EqR1; thus P = Class EqR1 by A21,A22,Th40; end; hence thesis by A1; end; theorem for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y) by Lm2; theorem x in Class EqR implies ex y being Element of X st x = Class(EqR,y) proof assume A1: x in Class EqR; then reconsider x as Subset of X; consider y such that A2: y in X & x = Class(EqR,y) by A1,Def5; reconsider y as Element of X by A2; take y; thus thesis by A2; end;