### The Mizar article:

### Zermelo Theorem and Axiom of Choice

**by****Grzegorz Bancerek**

- Received June 26, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: WELLORD2
- [ MML identifier index ]

environ vocabulary RELAT_1, ORDINAL1, BOOLE, RELAT_2, WELLORD1, FUNCT_1, TARSKI, WELLORD2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1, ORDINAL1; constructors RELAT_2, WELLORD1, SUBSET_1, ORDINAL1, XBOOLE_0; clusters FUNCT_1, ORDINAL1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, RELAT_2, WELLORD1; theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ORDINAL1, XBOOLE_0, XBOOLE_1; schemes FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0; begin reserve X,Y,Z for set, a,b,c,d,x,y,z,u for set, R for Relation, A,B,C for Ordinal; definition let X; func RelIncl X -> Relation means :Def1: field it = X & for Y,Z st Y in X & Z in X holds [Y,Z] in it iff Y c= Z; existence proof defpred P[set,set] means ex Y,Z st $1 = Y & $2 = Z & Y c= Z; consider R such that A1: [x,y] in R iff x in X & y in X & P[x,y] from Rel_Existence; take R; thus field R = X proof thus x in field R implies x in X proof assume x in field R; then A2: x in dom R \/ rng R by RELAT_1:def 6; A3: now assume x in dom R; then ex y st [x,y] in R by RELAT_1:def 4; hence x in X by A1; end; now assume x in rng R; then ex y st [y,x] in R by RELAT_1:def 5; hence x in X by A1; end; hence thesis by A2,A3,XBOOLE_0:def 2; end; let x; assume x in X; then [x,x] in R by A1; hence x in field R by RELAT_1:30; end; let Y,Z such that A4: Y in X & Z in X; thus [Y,Z] in R implies Y c= Z proof assume [Y,Z] in R; then ex V1,V2 being set st V1 = Y & V2 = Z & V1 c= V2 by A1; hence thesis; end; assume Y c= Z; hence thesis by A1,A4; end; uniqueness proof let R1,R2 be Relation such that A5: field R1 = X & for Y,Z st Y in X & Z in X holds [Y,Z] in R1 iff Y c= Z and A6: field R2 = X & for Y,Z st Y in X & Z in X holds [Y,Z] in R2 iff Y c= Z; let x,y; thus [x,y] in R1 implies [x,y] in R2 proof assume A7: [x,y] in R1; then A8: x in field R1 & y in field R1 by RELAT_1:30; then x c= y by A5,A7; hence thesis by A5,A6,A8; end; assume A9: [x,y] in R2; then A10: x in field R2 & y in field R2 by RELAT_1:30; then x c= y by A6,A9; hence thesis by A5,A6,A10; end; end; canceled; theorem Th2: RelIncl X is reflexive proof let a such that A1: a in field RelIncl X; field RelIncl X = X & for Y,Z st Y in X & Z in X holds [Y,Z] in RelIncl X iff Y c= Z by Def1; hence [a,a] in RelIncl X by A1; end; theorem Th3: RelIncl X is transitive proof let a,b,c such that A1: a in field RelIncl X & b in field RelIncl X & c in field RelIncl X & [a,b] in RelIncl X & [b,c] in RelIncl X; field RelIncl X = X & for Y,Z st Y in X & Z in X holds [Y,Z] in RelIncl X iff Y c= Z by Def1; then a c= b & b c= c by A1; then a in X & c in X & a c= c by A1,Def1,XBOOLE_1:1; hence thesis by Def1; end; theorem Th4: RelIncl A is connected proof let a,b such that A1: a in field RelIncl A & b in field RelIncl A & a <> b; A2: field RelIncl A = A & for Y,Z st Y in A & Z in A holds [Y,Z] in RelIncl A iff Y c= Z by Def1; then reconsider Y = a , Z = b as Ordinal by A1,ORDINAL1:23; Y c= Z or Z c= Y; hence [a,b] in RelIncl A or [b,a] in RelIncl A by A1,A2; end; theorem Th5: RelIncl X is antisymmetric proof let a,b such that A1: a in field RelIncl X & b in field RelIncl X & [a,b] in RelIncl X & [b,a] in RelIncl X; field RelIncl X = X & for Y,Z st Y in X & Z in X holds [Y,Z] in RelIncl X iff Y c= Z by Def1; then a c= b & b c= a by A1; hence a = b by XBOOLE_0:def 10; end; theorem Th6: RelIncl A is well_founded proof let Y; assume A1: Y c= field RelIncl A & Y <> {}; consider x being Element of Y; A2: field RelIncl A = A by Def1; then x in A by A1,TARSKI:def 3; then reconsider x as Ordinal by ORDINAL1:23; defpred P[Ordinal] means $1 in Y; x in Y by A1; then A3: ex B st P[B]; consider B such that A4: P[B] & for C st P[C] holds B c= C from Ordinal_Min(A3); reconsider x = B as set; take x; thus x in Y by A4; assume A5: (RelIncl A)-Seg(x) /\ Y <> {}; consider y being Element of (RelIncl A)-Seg(x) /\ Y; A6: y in (RelIncl A)-Seg(x) & y in Y by A5,XBOOLE_0:def 3; then A7: y <> x & [y,x] in RelIncl A & y in A by A1,A2,WELLORD1:def 1; reconsider C = y as Ordinal by A1,A2,A6,ORDINAL1:23; C c= B & B c= C by A1,A2,A4,A6,A7,Def1; hence contradiction by A7,XBOOLE_0:def 10; end; theorem Th7: RelIncl A is well-ordering proof thus RelIncl A is reflexive & RelIncl A is transitive & RelIncl A is antisymmetric & RelIncl A is connected & RelIncl A is well_founded by Th2,Th3,Th4,Th5,Th6; end; theorem Th8: Y c= X implies (RelIncl X) |_2 Y = RelIncl Y proof assume A1: Y c= X; let a,b; thus [a,b] in (RelIncl X) |_2 Y implies [a,b] in RelIncl Y proof assume [a,b] in (RelIncl X) |_2 Y; then A2: [a,b] in [:Y,Y:] & [a,b] in RelIncl X by WELLORD1:16; then A3: a in Y & b in Y by ZFMISC_1:106; then a c= b by A1,A2,Def1; hence [a,b] in RelIncl Y by A3,Def1; end; assume A4: [a,b] in RelIncl Y; then A5: a in field RelIncl Y & b in field RelIncl Y & field RelIncl Y = Y by Def1,RELAT_1:30; then a c= b by A4,Def1; then [a,b] in RelIncl X & [a,b] in [:Y,Y:] by A1,A5,Def1,ZFMISC_1:106; hence thesis by WELLORD1:16; end; theorem Th9: for A,X st X c= A holds RelIncl X is well-ordering proof let A,X such that A1: X c= A; RelIncl A is well-ordering by Th7; then (RelIncl A) |_2 X is well-ordering by WELLORD1:32; hence thesis by A1,Th8; end; reserve H for Function; theorem Th10: A in B implies A = (RelIncl B)-Seg(A) proof assume A1: A in B; thus a in A implies a in (RelIncl B)-Seg(A) proof assume A2: a in A; then reconsider C = a as Ordinal by ORDINAL1:23; A3: C c= A by A2,ORDINAL1:def 2; A c= B by A1,ORDINAL1:def 2; then A4: [C,A] in RelIncl B by A1,A2,A3,Def1; a <> A by A2; hence a in (RelIncl B)-Seg(A) by A4,WELLORD1:def 1; end; let a; assume a in (RelIncl B)-Seg(A); then A5: [a,A] in RelIncl B & a <> A by WELLORD1:def 1; then A6: a in field RelIncl B & field RelIncl B = B by Def1,RELAT_1:30; then reconsider C = a as Ordinal by ORDINAL1:23; C c= A by A1,A5,A6,Def1; then C c< A by A5,XBOOLE_0:def 8; hence a in A by ORDINAL1:21; end; theorem Th11: RelIncl A,RelIncl B are_isomorphic implies A = B proof assume A1: RelIncl A,RelIncl B are_isomorphic; assume A <> B; then A2: A in B or B in A by ORDINAL1:24; A3: now assume A4: A in B; then A5: A = (RelIncl B)-Seg(A) by Th10; A6: field RelIncl B = B by Def1; then (RelIncl B)-Seg(A) c= B by WELLORD1:13; then A7: RelIncl A = (RelIncl B) |_2 ((RelIncl B)-Seg(A)) by A5,Th8; RelIncl B is well-ordering by Th7; then not RelIncl B,RelIncl A are_isomorphic by A4,A6,A7,WELLORD1:57; hence contradiction by A1,WELLORD1:50; end; then A8: B = (RelIncl A)-Seg(B) by A2,Th10; A9: field RelIncl A = A by Def1; then (RelIncl A)-Seg(B) c= A by WELLORD1:13; then A10: RelIncl B = (RelIncl A) |_2 ((RelIncl A)-Seg(B)) by A8,Th8; RelIncl A is well-ordering by Th7; hence contradiction by A1,A2,A3,A9,A10,WELLORD1:57; end; theorem Th12: for X,R,A,B st R,RelIncl A are_isomorphic & R,RelIncl B are_isomorphic holds A = B proof let X,R,A,B such that A1: R,RelIncl A are_isomorphic and A2: R,RelIncl B are_isomorphic; RelIncl A,R are_isomorphic by A1,WELLORD1:50; then RelIncl A,RelIncl B are_isomorphic by A2,WELLORD1:52; hence A = B by Th11; end; theorem Th13: for R st R is well-ordering & for a st a in field R ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic ex A st R,RelIncl A are_isomorphic proof let R such that A1: R is well-ordering; assume A2: for a st a in field R ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic; defpred P[set,set] means for A holds A = $2 iff R |_2 (R-Seg $1),RelIncl A are_isomorphic; A3: for b,c,d st b in field R & P[b,c] & P[b,d] holds c = d proof let b,c,d such that A4: b in field R and A5: A = c iff R |_2 (R-Seg(b)),RelIncl A are_isomorphic and A6: B = d iff R |_2 (R-Seg(b)),RelIncl B are_isomorphic; consider A such that A7: R |_2 (R-Seg(b)),RelIncl A are_isomorphic by A2,A4; A = c & A = d by A5,A6,A7; hence c = d; end; A8: for a st a in field R ex b st P[a,b] proof let a; assume a in field R; then consider A such that A9: R |_2 (R-Seg(a)),RelIncl A are_isomorphic by A2; reconsider b = A as set; take b; let B; thus B = b implies R |_2 (R-Seg(a)),RelIncl B are_isomorphic by A9; assume R |_2 (R-Seg(a)),RelIncl B are_isomorphic; hence B = b by A9,Th12; end; consider H such that A10: dom H = field R & for b st b in field R holds P[b, H.b] from FuncEx(A3,A8); for a st a in rng H holds a is Ordinal proof let b; assume b in rng H; then consider c such that A11: c in dom H & b = H.c by FUNCT_1:def 5; consider A such that A12: R |_2 (R-Seg(c)),RelIncl A are_isomorphic by A2,A10,A11; thus thesis by A10,A11,A12; end; then consider C such that A13: rng H c= C by ORDINAL1:36; A14:C = field RelIncl C by Def1; A15: RelIncl C is well-ordering by Th7; A16: now let b; assume A17: b in rng H; then consider b' being set such that A18: b' in dom H & b = H.b' by FUNCT_1:def 5; set V = R-Seg(b'); set P = R |_2 V; consider A such that A19: P,RelIncl A are_isomorphic by A2,A10,A18; A20: A = b by A10,A18,A19; let c such that A21: [c,b] in RelIncl C; now assume A22: c <> b; C = field RelIncl C by Def1; then A23: c in C & b in C by A21,RELAT_1:30; then reconsider B = c as Ordinal by ORDINAL1:23; A24: B c= A by A20,A21,A23,Def1; then B c< A by A20,A22,XBOOLE_0:def 8; then A25: B in A & A = field RelIncl A by Def1,ORDINAL1:21; A26: RelIncl A is well-ordering by Th7; RelIncl A,P are_isomorphic by A19,WELLORD1:50; then canonical_isomorphism_of(RelIncl A,P) is_isomorphism_of RelIncl A,P by A26,WELLORD1:def 9; then consider d such that A27: d in field P & (RelIncl A) |_2 ((RelIncl A)-Seg(B)),P |_2 (P-Seg(d)) are_isomorphic by A25,A26,WELLORD1:61; A28: d in V & d in field R by A27,WELLORD1:19; then A29: [d,b'] in R by WELLORD1:def 1; A30: B = (RelIncl A)-Seg(B) by A25,Th10; A31: (RelIncl A) |_2 B = RelIncl B by A24,Th8; A32: P-Seg(d) = R-Seg(d) by A1,A10,A18,A28,WELLORD1:35; R-Seg(d) c= R-Seg(b') by A1,A10,A18,A28,A29,WELLORD1:37; then RelIncl B,R |_2 (R-Seg(d)) are_isomorphic by A27,A30,A31,A32,WELLORD1:29 ; then R |_2 (R-Seg(d)),RelIncl B are_isomorphic by WELLORD1:50; then B = H.d by A10,A28; hence c in rng H by A10,A28,FUNCT_1:def 5; end; hence c in rng H by A17; end; rng H is Ordinal proof now given a such that A33: a in C & rng H = (RelIncl C)-Seg(a); reconsider A = a as Ordinal by A33,ORDINAL1:23; (RelIncl C)-Seg(A) = A by A33,Th10; hence thesis by A33; end; hence thesis by A13,A14,A15,A16,WELLORD1:36; end; then reconsider A = rng H as Ordinal; A34: a in dom H implies H.a is Ordinal proof assume a in dom H; then H.a in A by FUNCT_1:def 5; hence thesis by ORDINAL1:23; end; take A; take H; thus dom H = field R by A10; thus rng H = field RelIncl A by Def1; thus A35: H is one-to-one proof let a,b; assume A36: a in dom H & b in dom H & H.a = H.b; then reconsider B = H.a as Ordinal by A34; A37: R |_2 (R-Seg(a)),RelIncl B are_isomorphic & R |_2 (R-Seg(b)),RelIncl B are_isomorphic by A10,A36; then RelIncl B,R |_2 (R-Seg(b)) are_isomorphic by WELLORD1:50; then R |_2 (R-Seg(a)),R |_2 (R-Seg(b)) are_isomorphic by A37,WELLORD1:52 ; hence a = b by A1,A10,A36,WELLORD1:58; end; let a,b; thus [a,b] in R implies a in field R & b in field R & [H.a,H.b] in RelIncl A proof assume A38: [a,b] in R; hence A39: a in field R & b in field R by RELAT_1:30; then reconsider A' = H.a , B' = H.b as Ordinal by A10,A34; A40: R |_2 (R-Seg(a)),RelIncl A' are_isomorphic & R |_2 (R-Seg(b)),RelIncl B' are_isomorphic by A10,A39; A41: A' in A & B' in A & A = field RelIncl A by A10,A39,Def1,FUNCT_1:def 5; set Z = R-Seg(b); set P = R |_2 Z; A42: P is well-ordering by A1,WELLORD1:32; now assume a <> b; then A43: a in Z & Z c= field R by A38,WELLORD1:13,def 1; then A44: a in field P by A1,WELLORD1:39; A45: RelIncl A is well-ordering by Th7; A46: A' = (RelIncl A)-Seg(A') & B' = (RelIncl A)-Seg(B') by A41,Th10; A47: A' c= A & B' c= A by A41,ORDINAL1:def 2; then A48: (RelIncl A) |_2 A' = RelIncl A' & (RelIncl A) |_2 B' = RelIncl B' by Th8; A49: P,(RelIncl A) |_2 ((RelIncl A)-Seg(B')) are_isomorphic by A40,A46,A47,Th8 ; A50: P-Seg(a) = R-Seg(a) by A1,A39,A43,WELLORD1:35; R-Seg(a) c= R-Seg(b) by A1,A38,A39,WELLORD1:37; then P |_2 (P-Seg(a)),(RelIncl A) |_2 ((RelIncl A)-Seg(A')) are_isomorphic by A40,A46,A48,A50,WELLORD1:29; hence [A',B'] in RelIncl A by A41,A42,A44,A45,A49,WELLORD1:62; end; hence thesis by A41,Def1; end; assume A51: a in field R & b in field R & [H.a,H.b] in RelIncl A; R is connected by A1,WELLORD1:def 4; then A52: R is_connected_in field R by RELAT_2:def 14; R is reflexive by A1,WELLORD1:def 4; then A53: R is_reflexive_in field R by RELAT_2:def 9; RelIncl A is antisymmetric by Th5; then A54: RelIncl A is_antisymmetric_in field RelIncl A by RELAT_2:def 12; assume A55: not [a,b] in R; then A56: a <> b by A51,A53,RELAT_2:def 1; then A57: [b,a] in R by A51,A52,A55,RELAT_2:def 6; reconsider A' = H.a , B' = H.b as Ordinal by A10,A34,A51; A58: R |_2 (R-Seg(a)),RelIncl A' are_isomorphic & R |_2 (R-Seg(b)),RelIncl B' are_isomorphic by A10,A51; set Z = R-Seg(a); set P = R |_2 Z; A59: P is well-ordering by A1,WELLORD1:32; A60:b in Z & Z c= field R by A56,A57,WELLORD1:13,def 1; then A61: b in field P by A1,WELLORD1:39; A62: RelIncl A is well-ordering by Th7; A63: A' in A & B' in A & A = field RelIncl A by A10,A51,Def1,FUNCT_1:def 5 ; then A64: A' = (RelIncl A)-Seg(A') & B' = (RelIncl A)-Seg(B') by Th10; A65: A' c= A & B' c= A by A63,ORDINAL1:def 2; then A66: (RelIncl A) |_2 A' = RelIncl A' & (RelIncl A) |_2 B' = RelIncl B' by Th8; A67: P,(RelIncl A) |_2 ((RelIncl A)-Seg(A')) are_isomorphic by A58,A64,A65,Th8; A68: P-Seg(b) = R-Seg(b) by A1,A51,A60,WELLORD1:35; R-Seg(b) c= R-Seg(a) by A1,A51,A57,WELLORD1:37; then P |_2 (P-Seg(b)),(RelIncl A) |_2 ((RelIncl A)-Seg(B')) are_isomorphic by A58,A64,A66,A68,WELLORD1:29; then [B',A'] in RelIncl A by A59,A61,A62,A63,A67,WELLORD1:62; then H.a = H.b by A51,A54,A63,RELAT_2:def 4; hence contradiction by A10,A35,A51,A56,FUNCT_1:def 8; end; theorem Th14: for R st R is well-ordering ex A st R,RelIncl A are_isomorphic proof let R such that A1: R is well-ordering; defpred P[set] means ex A st R |_2 (R-Seg($1)),RelIncl A are_isomorphic; consider Z such that A2: a in Z iff a in field R & P[a] from Separation; now let a such that A3: a in field R & R-Seg(a) c= Z; set P = R |_2 (R-Seg(a)); A4: P is well-ordering by A1,WELLORD1:32; now let b; assume b in field P; then A5: b in R-Seg(a) & b in field R by WELLORD1:19; then consider A such that A6: R |_2 (R-Seg(b)),RelIncl A are_isomorphic by A2,A3; take A; A7: P-Seg(b) = R-Seg(b) by A1,A3,A5,WELLORD1:35; [b,a] in R by A5,WELLORD1:def 1; then R-Seg(b) c= R-Seg(a) by A1,A3,A5,WELLORD1:37; hence P |_2 (P-Seg(b)),RelIncl A are_isomorphic by A6,A7,WELLORD1:29; end; then ex A st P,RelIncl A are_isomorphic by A4,Th13; hence a in Z by A2,A3; end; then field R c= Z by A1,WELLORD1:41; then for a st a in field R ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic by A2; hence thesis by A1,Th13; end; definition let R; assume A1: R is well-ordering; func order_type_of R -> Ordinal means :Def2: R,RelIncl it are_isomorphic; existence by A1,Th14; uniqueness by Th12; end; definition let A,R; pred A is_order_type_of R means A = order_type_of R; end; canceled 2; theorem X c= A implies order_type_of RelIncl X c= A proof assume A1: X c= A; then A2: RelIncl X is well-ordering by Th9; A3: RelIncl A is well-ordering by Th7; A4: field RelIncl A = A by Def1; A5: (RelIncl A) |_2 X = RelIncl X by A1,Th8; A6: now assume RelIncl A,(RelIncl A) |_2 X are_isomorphic; then RelIncl X,RelIncl A are_isomorphic by A5,WELLORD1:50; hence order_type_of RelIncl X c= A by A2,Def2; end; now given a such that A7: a in A & (RelIncl A) |_2 ((RelIncl A)-Seg(a)),(RelIncl A) |_2 X are_isomorphic; reconsider a as Ordinal by A7,ORDINAL1:23; A8: (RelIncl A)-Seg(a) = a by A7,Th10; A9: a c= A by A7,ORDINAL1:def 2; then (RelIncl A) |_2 a = RelIncl a by Th8; then RelIncl X,RelIncl a are_isomorphic by A5,A7,A8,WELLORD1:50; hence order_type_of RelIncl X c= A by A2,A9,Def2; end; hence thesis by A1,A3,A4,A6,WELLORD1:64; end; reserve f,g for Function; definition let X,Y; redefine pred X,Y are_equipotent means ex f st f is one-to-one & dom f = X & rng f = Y; compatibility proof thus X,Y are_equipotent implies ex f st f is one-to-one & dom f = X & rng f = Y proof assume X,Y are_equipotent; then consider Z such that A1: for x st x in X ex y st y in Y & [x,y] in Z and A2: for y st y in Y ex x st x in X & [x,y] in Z and A3: for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u by TARSKI :def 6; set F = Z /\ [:X,Y:]; F is Relation-like Function-like proof thus for z st z in F ex x,y st [x,y] = z proof let z; assume z in F; then z in [:X,Y:] by XBOOLE_0:def 3; hence thesis by ZFMISC_1:102; end; thus for x,y,z st [x,y] in F & [x,z] in F holds y = z proof let x,y,z; assume [x,y] in F & [x,z] in F; then [x,y] in Z & [x,z] in Z by XBOOLE_0:def 3; hence thesis by A3; end; end; then reconsider F as Function; take f = F; thus f is one-to-one proof let x,y; assume A4: x in dom f & y in dom f & f.x = f.y; then [x,f.x] in f & [y,f.y] in f by FUNCT_1:8; then [x,f.x] in Z & [y,f.y] in Z by XBOOLE_0:def 3; hence x = y by A3,A4; end; thus dom f c= X proof let x; assume x in dom f; then [x,f.x] in f by FUNCT_1:8; then [x,f.x] in [:X,Y:] by XBOOLE_0:def 3; hence x in X by ZFMISC_1:106; end; thus X c= dom f proof let x; assume A5: x in X; then consider y such that A6: y in Y & [x,y] in Z by A1; [x,y] in [:X,Y:] by A5,A6,ZFMISC_1:106; then [x,y] in f by A6,XBOOLE_0:def 3; hence x in dom f by FUNCT_1:8; end; thus rng f c= Y proof let y; assume y in rng f; then consider x such that A7: x in dom f & y = f.x by FUNCT_1:def 5; [x,y] in f by A7,FUNCT_1:8; then [x,y] in [:X,Y:] by XBOOLE_0:def 3; hence y in Y by ZFMISC_1:106; end; thus Y c= rng f proof let y; assume A8: y in Y; then consider x such that A9: x in X & [x,y] in Z by A2; [x,y] in [:X,Y:] by A8,A9,ZFMISC_1:106; then [x,y] in f by A9,XBOOLE_0:def 3; then x in dom f & y = f.x by FUNCT_1:8; hence y in rng f by FUNCT_1:def 5; end; end; (ex f st f is one-to-one & dom f = X & rng f = Y) implies ex Z st (for x st x in X ex y st y in Y & [x,y] in Z) & (for y st y in Y ex x st x in X & [x,y] in Z) & for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u proof given f such that A10: f is one-to-one & dom f = X & rng f = Y; take Z = f; thus x in X implies ex y st y in Y & [x,y] in Z proof assume A11: x in X; take f.x; thus f.x in Y by A10,A11,FUNCT_1:def 5; thus [x,f.x] in Z by A10,A11,FUNCT_1:8; end; thus for y st y in Y ex x st x in X & [x,y] in Z proof let y such that A12: y in Y; take f".y; A13: dom(f") = rng f & rng(f") = dom f by A10,FUNCT_1:55; hence f".y in X by A10,A12,FUNCT_1:def 5; A14: y = f.(f".y) by A10,A12,FUNCT_1:57; f".y in rng(f") by A10,A12,A13,FUNCT_1:def 5; hence [f".y,y] in Z by A13,A14,FUNCT_1:8; end; let x,y,z,u; assume [x,y] in Z & [z,u] in Z; then y = f.x & u = f.z & x in dom f & z in dom f by FUNCT_1:8; hence x = z iff y = u by A10,FUNCT_1:def 8; end; hence thesis by TARSKI:def 6; end; reflexivity proof let X; take id X; thus thesis by FUNCT_1:52,RELAT_1:71; end; symmetry proof let X,Y; given f such that A15: f is one-to-one & dom f = X & rng f = Y; take f"; thus thesis by A15,FUNCT_1:55,62; end; end; canceled 4; theorem X,Y are_equipotent & Y,Z are_equipotent implies X,Z are_equipotent proof given f such that A1: f is one-to-one & dom f = X & rng f = Y; given g such that A2: g is one-to-one & dom g = Y & rng g = Z; take g*f; thus thesis by A1,A2,FUNCT_1:46,RELAT_1:46,47; end; canceled 2; theorem Th25: R well_orders X implies field(R|_2 X) = X & R|_2 X is well-ordering proof assume A1: 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; thus A2: field(R|_2 X) = X proof thus field(R|_2 X) c= X by WELLORD1:20; let x; assume x in X; then [x,x] in R & [x,x] in [:X,X:] by A1,RELAT_2:def 1,ZFMISC_1:106; then [x,x] in R|_2 X by WELLORD1:16; hence x in field(R|_2 X) by RELAT_1:30; end; R|_2 X well_orders X proof thus R|_2 X is_reflexive_in X proof let x; assume x in X; then [x,x] in R & [x,x] in [:X,X:] by A1,RELAT_2:def 1,ZFMISC_1:106; hence [x,x] in R|_2 X by WELLORD1:16; end; thus R|_2 X is_transitive_in X proof let x,y,z; assume A3: x in X & y in X & z in X & [x,y] in R|_2 X & [y,z] in R|_2 X; then [x,y] in R & [y,z] in R by WELLORD1:16; then [x,z] in R & [x,z] in [:X,X:] by A1,A3,RELAT_2:def 8,ZFMISC_1: 106; hence [x,z] in R|_2 X by WELLORD1:16; end; thus R|_2 X is_antisymmetric_in X proof let x,y; assume A4: x in X & y in X & [x,y] in R|_2 X & [y,x] in R|_2 X; then [x,y] in R & [y,x] in R by WELLORD1:16; hence x = y by A1,A4,RELAT_2:def 4; end; thus R|_2 X is_connected_in X proof let x,y; assume x in X & y in X & x <> y; then ([x,y] in R or [y,x] in R) & [x,y] in [:X,X:] & [y,x] in [:X,X :] by A1,RELAT_2:def 6,ZFMISC_1:106; hence [x,y] in R|_2 X or [y,x] in R|_2 X by WELLORD1:16; end; thus R|_2 X is_well_founded_in X proof let Y; assume Y c= X & Y <> {}; then consider a such that A5: a in Y & R-Seg(a) misses Y by A1,WELLORD1:def 3; take a; thus a in Y by A5; assume not thesis; then consider x being set such that A6: x in (R|_2 X)-Seg(a) & x in Y by XBOOLE_0:3; A7: x <> a & [x,a] in R|_2 X by A6,WELLORD1:def 1; then [x,a] in R by WELLORD1:16; then x in R-Seg(a) by A7,WELLORD1:def 1; hence contradiction by A5,A6,XBOOLE_0:3; end; end; hence thesis by A2,WELLORD1:8; end; :: :: Zermelo theorem :: Lm1: R is well-ordering & X,field R are_equipotent implies ex R st R well_orders X proof assume A1: R is well-ordering; then R is reflexive by WELLORD1:def 4; then A2: R is_reflexive_in field R by RELAT_2:def 9; given f such that A3: f is one-to-one & dom f = X & rng f = field R; defpred P[set,set] means [f.$1,f.$2] in R; consider Q being Relation such that A4: [x,y] in Q iff x in X & y in X & P[x,y] from Rel_Existence; A5: field Q = X proof thus field Q c= X proof let x; assume A6: x in field Q & not x in X; then (for y holds not [x,y] in Q) & (for y holds not [y,x] in Q) by A4; then not x in dom Q & not x in rng Q by RELAT_1:def 4,def 5; then not x in dom Q \/ rng Q by XBOOLE_0:def 2; hence contradiction by A6,RELAT_1:def 6; end; let x; assume A7: x in X; then f.x in rng f by A3,FUNCT_1:def 5; then [f.x,f.x] in R by A2,A3,RELAT_2:def 1; then [x,x] in Q by A4,A7; hence x in field Q by RELAT_1:30; end; f is_isomorphism_of Q,R proof thus dom f = field Q & rng f = field R & f is one-to-one by A3,A5; let x,y; thus [x,y] in Q implies x in field Q & y in field Q & [f.x,f.y] in R by A4,A5; assume x in field Q & y in field Q & [f.x,f.y] in R; hence [x,y] in Q by A4,A5; end; then f" is_isomorphism_of R,Q by WELLORD1:49; then A8: Q is well-ordering by A1,WELLORD1:54; take Q; thus thesis by A5,A8,WELLORD1:8; end; theorem Th26: for X ex R st R well_orders X proof let X; consider Class being set such that A1: X in Class and A2: Y in Class & Z c= Y implies Z in Class and Y in Class implies bool Y in Class and A3: Y c= Class implies Y,Class are_equipotent or Y in Class by ZFMISC_1:136; defpred P[set] means $1 is Ordinal; consider ON being set such that A4: x in ON iff x in Class & P[x] from Separation; for Y st Y in ON holds Y is Ordinal & Y c= ON proof let Y; assume A5: Y in ON; hence Y is Ordinal by A4; reconsider A = Y as Ordinal by A4,A5; let x; assume A6: x in Y; then x in A; then reconsider B = x as Ordinal by ORDINAL1:23; B c= A & A in Class by A4,A5,A6,ORDINAL1:def 2; then B in Class by A2; hence x in ON by A4; end; then reconsider ON as Ordinal by ORDINAL1:31; A7: ON c= Class proof let x; thus x in ON implies x in Class by A4; end; A8: ON,Class are_equipotent proof assume not thesis; then ON in Class by A3,A7; then ON in ON by A4; hence contradiction; end; field RelIncl ON = ON & RelIncl ON is well-ordering by Def1,Th7; then consider R such that A9: R well_orders Class by A8,Lm1; set Q = R|_2 Class; A10: field Q = Class & Q is well-ordering by A9,Th25; deffunc F(set) = {$1}; consider f such that A11: dom f = X & for x st x in X holds f.x = F(x) from Lambda; A12: rng f c= Class proof let x; assume x in rng f; then consider y such that A13: y in dom f & x = f.y by FUNCT_1:def 5; A14: f.y = { y } by A11,A13; { y } c= X proof let z; assume z in { y }; hence z in X by A11,A13,TARSKI:def 1; end; hence x in Class by A1,A2,A13,A14; end; A15: X,rng f are_equipotent proof take f; thus f is one-to-one proof let x,y; assume A16: x in dom f & y in dom f & f.x = f.y; then f.x = { x } & f.y = { y } by A11; hence x = y by A16,ZFMISC_1:6; end; thus dom f = X & rng f = rng f by A11; end; A17: Q|_2 rng f is well-ordering by A10,WELLORD1:32; field(Q|_2 rng f) = rng f by A10,A12,WELLORD1:39; hence thesis by A15,A17,Lm1; end; reserve M for non empty set; :: :: Axiom of choice :: theorem (for X st X in M holds X <> {}) & (for X,Y st X in M & Y in M & X <> Y holds X misses Y) implies ex Choice being set st for X st X in M ex x st Choice /\ X = { x } proof assume that A1: for X st X in M holds X <> {} and A2: for X,Y st X in M & Y in M & X <> Y holds X misses Y; consider R such that A3: R well_orders union M by Th26; A4: R is_antisymmetric_in union M by A3,WELLORD1:def 5; A5: R is_well_founded_in union M by A3,WELLORD1:def 5; A6: R is_connected_in union M by A3,WELLORD1:def 5; A7: R is_reflexive_in union M by A3,WELLORD1:def 5; defpred Ch[set,set] means ex X st $1 = X & $2 in X & for z st z in X holds [$2,z] in R; A8: for x,y,z st x in M & Ch[x,y] & Ch[x,z] holds y = z proof let x,y,z such that A9: x in M; given Y such that A10: x = Y & y in Y & for u st u in Y holds [y,u] in R; given Z such that A11: x = Z & z in Z & for u st u in Z holds [z,u] in R; y in union M & z in union M & [y,z] in R & [z,y] in R by A9,A10,A11,TARSKI:def 4; hence y = z by A4,RELAT_2:def 4; end; A12: for x st x in M ex y st Ch[x,y] proof let x; assume x in M; then A13: x c= union M & x <> {} by A1,ZFMISC_1:92; then consider y such that A14: y in x & R-Seg(y) misses x by A5,WELLORD1:def 3; take y,x; thus x = x & y in x by A14; let z; assume A15: z in x; then A16: y <> z implies [y,z] in R or [z,y] in R by A6,A13,A14,RELAT_2:def 6; A17: y = z implies [y,z] in R by A7,A13,A15,RELAT_2:def 1; not z in R-Seg(y) by A14,A15,XBOOLE_0:3; hence thesis by A16,A17,WELLORD1:def 1; end; consider f such that A18: dom f = M & for x st x in M holds Ch[x,f.x] from FuncEx(A8,A12); take Choice = rng f; let X such that A19: X in M; take x = f.X; A20: for X st X in M holds f.X in X proof let X; assume X in M; then ex Y st X = Y & f.X in Y & for z st z in Y holds [f.X,z] in R by A18; hence thesis; end; thus Choice /\ X c= { x } proof let y; assume y in Choice /\ X; then A21: y in Choice & y in X by XBOOLE_0:def 3; then consider z such that A22: z in dom f & y = f.z by FUNCT_1:def 5; assume not y in { x }; then X <> z by A22,TARSKI:def 1; then X misses z by A2,A18,A19,A22; then A23: X /\ z = {} by XBOOLE_0:def 7; f.z in z by A18,A20,A22; hence contradiction by A21,A22,A23,XBOOLE_0:def 3; end; let y; assume y in { x }; then y = x by TARSKI:def 1; then y in Choice & y in X by A18,A19,A20,FUNCT_1:def 5; hence thesis by XBOOLE_0:def 3; end; theorem (for X st X in M holds X <> {}) implies ex Choice being Function st dom Choice = M & for X st X in M holds Choice.X in X proof assume A1: for X st X in M holds X <> {}; consider R such that A2: R well_orders union M by Th26; A3: R is_antisymmetric_in union M by A2,WELLORD1:def 5; A4: R is_well_founded_in union M by A2,WELLORD1:def 5; A5: R is_connected_in union M by A2,WELLORD1:def 5; A6: R is_reflexive_in union M by A2,WELLORD1:def 5; defpred Ch[set,set] means ex X st $1 = X & $2 in X & for z st z in X holds [$2,z] in R; A7: for x,y,z st x in M & Ch[x,y] & Ch[x,z] holds y = z proof let x,y,z such that A8: x in M; given Y such that A9: x = Y & y in Y & for u st u in Y holds [y,u] in R; given Z such that A10: x = Z & z in Z & for u st u in Z holds [z,u] in R; y in union M & z in union M & [y,z] in R & [z,y] in R by A8,A9,A10,TARSKI:def 4; hence y = z by A3,RELAT_2:def 4; end; A11: for x st x in M ex y st Ch[x,y] proof let x; assume x in M; then A12: x c= union M & x <> {} by A1,ZFMISC_1:92; then consider y such that A13: y in x & R-Seg(y) misses x by A4,WELLORD1:def 3; A14: R-Seg(y) /\ x = {} by A13,XBOOLE_0:def 7; take y,x; thus x = x & y in x by A13; let z; assume A15: z in x; then A16: y <> z implies [y,z] in R or [z,y] in R by A5,A12,A13,RELAT_2:def 6; A17: y = z implies [y,z] in R by A6,A12,A15,RELAT_2:def 1; not z in R-Seg(y) by A14,A15,XBOOLE_0:def 3; hence thesis by A16,A17,WELLORD1:def 1; end; consider f such that A18: dom f = M & for x st x in M holds Ch[x,f.x] from FuncEx(A7,A11); take Choice = f; thus dom Choice = M by A18; let X; assume X in M; then ex Y st X = Y & f.X in Y & for z st z in Y holds [f.X,z] in R by A18 ; hence thesis; end;

Back to top