### The Mizar article:

### Zermelo's Theorem

**by****Bogdan Nowak, and****Slawomir Bialecki**

- Received October 27, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: WELLSET1
- [ MML identifier index ]

environ vocabulary RELAT_1, FUNCT_1, BOOLE, WELLORD1, RELAT_2, TARSKI; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1; constructors TARSKI, RELAT_2, WELLORD1, SUBSET_1, XBOOLE_0; clusters RELAT_1, FUNCT_1, SUBSET_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, WELLORD1; theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1, XBOOLE_0, XBOOLE_1; schemes TARSKI, FUNCT_1, RELAT_1, XBOOLE_0; begin reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set, R,S,T,W,W1,W2 for Relation, F,H,H1 for Function; theorem Th1: x in field R iff ex y st ([x,y] in R or [y,x] in R) proof x in (dom R \/ rng R) iff x in dom R or x in rng R by XBOOLE_0:def 2; hence thesis by RELAT_1:def 4,def 5,def 6; end; canceled; theorem Th3: X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y proof consider a being Element of X, b being Element of Y; assume A1: X <> {} & Y <> {} & W = [: X,Y :]; A2: x in field W implies x in X \/ Y proof assume x in field W; then consider y such that A3: [x,y] in W or [y,x] in W by Th1; A4: [x,y] in W implies x in X \/ Y proof assume [x,y] in W; then x in X by A1,ZFMISC_1:106; hence thesis by XBOOLE_0:def 2; end; [y,x] in W implies x in X \/ Y proof assume [y,x] in W; then x in Y by A1,ZFMISC_1:106; hence thesis by XBOOLE_0:def 2; end; hence thesis by A3,A4; end; x in X \/ Y implies x in field W proof assume A5: x in X \/ Y; A6: x in X implies x in field W proof assume x in X; then [x,b] in W by A1,ZFMISC_1:106; hence thesis by Th1; end; x in Y implies x in field W proof assume x in Y; then [a,x] in W by A1,ZFMISC_1:106; hence thesis by Th1; end; hence thesis by A5,A6,XBOOLE_0:def 2; end; hence thesis by A2,TARSKI:2; end; scheme R_Separation { A()-> set, P[Relation] } : ex B st for R being Relation holds R in B iff R in A() & P[R] proof defpred p[set,set] means $1 = $2 & ex S st S = $2 & P[S]; A1: for y,t,v being set st p[y,t] & p[y,v] holds t = v; consider B such that A2: for t being set holds t in B iff ex y being set st y in A() & p[y,t] from Fraenkel(A1); take B; let R; A3: R in B iff ex T st T in A() & (T = R & P[R]) proof thus R in B implies ex T st T in A() & (T = R & P[R]) proof assume R in B; then consider y being set such that A4: y in A() & (y = R & ex S st S = R & P[S]) by A2; reconsider y as Relation by A4; take y; thus thesis by A4; end; thus thesis by A2; end; hence R in B implies R in A() & P[R]; thus thesis by A3; end; canceled 2; theorem Th6: for x,y,W st x in field W & y in field W & W is well-ordering holds not x in W-Seg(y) implies [y,x] in W proof let x,y,W; assume that A1: x in field W and A2: y in field W and A3: W is well-ordering; W is reflexive & W is connected by A3,WELLORD1:def 4; then A4: W is_reflexive_in field W & W is_connected_in field W by RELAT_2:def 9,def 14; then A5: x<>y implies [x,y] in W or [y,x] in W by A1,A2,RELAT_2:def 6; assume not x in W-Seg(y); then x=y or not [x,y] in W by WELLORD1:def 1; hence thesis by A1,A4,A5,RELAT_2:def 1; end; theorem Th7:for x,y,W st x in field W & y in field W & W is well-ordering holds x in W-Seg(y) implies not [y,x] in W proof let x,y,W; assume that A1: x in field W and A2: y in field W and A3: W is well-ordering; W is antisymmetric by A3,WELLORD1:def 4; then A4: W is_antisymmetric_in field W by RELAT_2:def 12; assume x in W-Seg(y); then A5: x<>y & [x,y] in W by WELLORD1:def 1; assume [y,x] in W; hence contradiction by A1,A2,A4,A5,RELAT_2:def 4; end; theorem Th8: for F,D st (for X st X in D holds not F.X in X & F.X in union D) ex R st field R c= union D & R is well-ordering & not field R in D & for y st y in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y proof let F,D; assume A1: for X st X in D holds not F.X in X & F.X in union D; set W0=bool [: union D, union D :]; defpred P[Relation] means $1 is well-ordering & for y st y in field $1 holds $1-Seg(y) in D & F.($1-Seg(y)) = y; consider G such that A2: W in G iff W in W0 & P[W] from R_Separation; A3: for W1,W2 holds W1 in G & W2 in G implies ((W1 c= W2 & for x st x in field W1 holds W1-Seg(x) = W2-Seg(x) ) or (W2 c= W1 & for x st x in field W2 holds W2-Seg(x) = W1-Seg(x) )) proof let W1,W2; assume A4: W1 in G & W2 in G; defpred P[set] means $1 in field W2 & W1 |_2 (W1-Seg($1)) = W2 |_2 (W2-Seg($1)); consider C such that A5: x in C iff x in field W1 & P[x] from Separation; A6: W1 is well-ordering & W2 is well-ordering by A2,A4; A7: x in C implies W1-Seg(x) = W2-Seg(x) proof assume A8: x in C; for y holds y in W1-Seg(x) iff y in W2-Seg(x) proof let y; A9: field (W1 |_2(W1-Seg(x))) = W1-Seg(x) by A6,WELLORD1:40; field (W2 |_2(W2-Seg(x))) = W2-Seg(x) by A6,WELLORD1:40; hence thesis by A5,A8,A9; end; hence thesis by TARSKI:2; end; A10: x in C implies W1-Seg(x) c= C proof assume A11: x in C; y in W1-Seg(x) implies y in C proof assume A12: y in W1-Seg(x); then A13:[y,x] in W1 by WELLORD1:def 1; then A14: y in field W1 by RELAT_1:30; A15: x in field W1 by A13,RELAT_1:30; then A16: W1-Seg(y) c= W1-Seg(x) by A6,A12,A14,WELLORD1:38; A17: y in W2-Seg(x) by A7,A11,A12; then A18: [y,x] in W2 by WELLORD1:def 1; then A19: y in field W2 by RELAT_1:30; A20: x in field W2 by A18,RELAT_1:30; then A21: W2-Seg(y) c= W2-Seg(x) by A6,A17,A19,WELLORD1:38; W1 |_2 (W1-Seg(y)) = W2 |_2 (W2-Seg(y)) proof A22: W1-Seg(y) = W2-Seg(y) proof W1-Seg(y)=(W1 |_2 (W1-Seg(x)))-Seg(y) by A6,A12,A15,WELLORD1:35 .=(W2 |_2 (W2-Seg(x)))-Seg(y) by A5,A11 .=W2-Seg(y) by A6,A17,A20,WELLORD1:35; hence thesis; end; W1 |_2 (W1-Seg(y)) = (W1 |_2 (W1-Seg(x))) |_2 (W1-Seg(y)) by A16,WELLORD1:29 .= (W2 |_2 (W2-Seg(x))) |_2 (W2-Seg(y)) by A5,A11,A22 .= W2 |_2 (W2-Seg(y)) by A21,WELLORD1:29; hence thesis; end; hence thesis by A5,A14,A19; end; hence thesis by TARSKI:def 3; end; A23: y1 in field W1 & not y1 in C implies ex y3 st y3 in field W1 & C=W1-Seg(y3) & not y3 in C proof assume A24: y1 in field W1 & not y1 in C; set Y = field W1 \ C; A25: Y c= field W1 by XBOOLE_1:36; Y <> {} by A24,XBOOLE_0:def 4; then consider a such that A26: a in Y and A27: for b st b in Y holds [a,b] in W1 by A6,A25,WELLORD1:10; take y3=a; A28: y3 in field W1 & not y3 in C by A26,XBOOLE_0:def 4; C= W1-Seg(y3) proof x in C iff x in W1-Seg(y3) proof thus x in C implies x in W1-Seg(y3) proof assume that A29: x in C and A30: not x in W1-Seg(y3); x in field W1 by A5,A29; then A31: [y3,x] in W1 by A6,A28,A30,Th6; A32: W1-Seg(x) c= C by A10,A29; y3 in C proof y3 <> x implies y3 in C proof assume y3 <> x; then y3 in W1-Seg(x) by A31,WELLORD1:def 1; hence y3 in C by A32; end; hence thesis by A29; end; hence contradiction by A26,XBOOLE_0:def 4; end; thus x in W1-Seg(y3) implies x in C proof assume that A33: x in W1-Seg(y3) and A34: not x in C; [x,y3] in W1 by A33,WELLORD1:def 1; then A35: x in field W1 by RELAT_1:30; then x in Y by A34,XBOOLE_0:def 4; then [y3,x] in W1 by A27; hence contradiction by A6,A28,A33,A35,Th7; end; end; hence thesis by TARSKI:2; end; hence thesis by A26,XBOOLE_0:def 4; end; A36: x in C implies W2-Seg(x) c= C proof assume A37: x in C; let y; assume A38: y in W2-Seg(x); then A39:[y,x] in W2 by WELLORD1:def 1; then A40: y in field W2 by RELAT_1:30; A41: x in field W2 by A39,RELAT_1:30; then A42: W2-Seg(y) c= W2-Seg(x) by A6,A38,A40,WELLORD1:38; A43: y in W1-Seg(x) by A7,A37,A38; then A44: [y,x] in W1 by WELLORD1:def 1; then A45: y in field W1 by RELAT_1:30; A46: x in field W1 by A44,RELAT_1:30; then A47: W1-Seg(y) c= W1-Seg(x) by A6,A43,A45,WELLORD1:38; W2 |_2 (W2-Seg(y)) = W1 |_2 (W1-Seg(y)) proof A48: W2-Seg(y) = W1-Seg(y) proof W2-Seg(y)=(W2 |_2 (W2-Seg(x)))-Seg(y) by A6,A38,A41,WELLORD1:35 .=(W1 |_2 (W1-Seg(x)))-Seg(y) by A5,A37 .=W1-Seg(y) by A6,A43,A46,WELLORD1:35; hence thesis; end; W2 |_2 (W2-Seg(y)) = (W2 |_2 (W2-Seg(x))) |_2 (W2-Seg(y)) by A42,WELLORD1:29 .= (W1 |_2 (W1-Seg(x))) |_2 (W1-Seg(y)) by A5,A37,A48 .= W1 |_2 (W1-Seg(y)) by A47,WELLORD1:29; hence thesis; end; hence thesis by A5,A40,A45; end; A49: y1 in field W2 & not y1 in C implies ex y3 st y3 in field W2 & C=W2-Seg(y3) & not y3 in C proof assume A50: y1 in field W2 & not y1 in C; set Y = field W2 \ C; A51: Y c= field W2 by XBOOLE_1:36; Y <> {} by A50,XBOOLE_0:def 4; then consider a such that A52: a in Y and A53: for b st b in Y holds [a,b] in W2 by A6,A51,WELLORD1:10; take y3=a; A54: y3 in field W2 & not y3 in C by A52,XBOOLE_0:def 4; C= W2-Seg(y3) proof x in C iff x in W2-Seg(y3) proof thus x in C implies x in W2-Seg(y3) proof assume that A55: x in C and A56: not x in W2-Seg(y3); x in field W2 by A5,A55; then A57: [y3,x] in W2 by A6,A54,A56,Th6; A58: W2-Seg(x) c= C by A36,A55; y3 <> x implies y3 in C proof assume y3 <> x; then y3 in W2-Seg(x) by A57,WELLORD1:def 1; hence y3 in C by A58; end; hence contradiction by A52,A55,XBOOLE_0:def 4; end; thus x in W2-Seg(y3) implies x in C proof assume that A59: x in W2-Seg(y3) and A60: not x in C; [x,y3] in W2 by A59,WELLORD1:def 1; then A61: x in field W2 by RELAT_1:30; then x in Y by A60,XBOOLE_0:def 4; then [y3,x] in W2 by A53; hence contradiction by A6,A54,A59,A61,Th7; end; end; hence thesis by TARSKI:2; end; hence thesis by A52,XBOOLE_0:def 4; end; A62: C = field W1 or C = field W2 proof assume not C = field W1; then A63: ex x st not (x in C implies x in field W1) or not (x in field W1 implies x in C) by TARSKI:2; assume not C = field W2; then A64: ex x st not (x in C implies x in field W2) or not (x in field W2 implies x in C) by TARSKI:2; consider y3 such that A65: y3 in field W1 & C=W1-Seg(y3) & not y3 in C by A5,A23,A63; consider y4 such that A66: y4 in field W2 & C=W2-Seg(y4) & not y4 in C by A5,A49,A64; A67: y3 = y4 proof y3 = F.(W2-Seg(y4)) by A2,A4,A65,A66 .= y4 by A2,A4,A66; hence thesis; end; W1 |_2 (W1-Seg(y3)) = W2 |_2 (W2-Seg(y3)) proof z in W1 |_2 (W1-Seg(y3)) iff z in W2 |_2 (W2-Seg(y3)) proof z in W1 & z in [: W1-Seg(y3),W1-Seg(y3) :] iff z in W2 & z in [: W2-Seg(y3),W2-Seg(y3) :] proof thus z in W1 & z in [: W1-Seg(y3),W1-Seg(y3) :] implies z in W2 & z in [: W2-Seg(y3),W2-Seg(y3) :] proof assume that A68: z in W1 and A69: z in [: W1-Seg(y3),W1-Seg(y3) :]; consider z1,z2 such that A70: z1 in W1-Seg(y3) and A71: z2 in W1-Seg(y3) and A72: z=[z1,z2] by A69,ZFMISC_1:def 2; A73: z1 in field W2 by A5,A65,A70; z1 in W1-Seg(z2) or (z1=z2 & not z1 in W1-Seg(z2)) by A68,A72,WELLORD1 :def 1; then z1 in W2-Seg(z2) or (z1=z2 & not z1 in W2-Seg(z2)) by A7,A65,A71; hence thesis by A6,A65,A66,A67,A69,A72,A73,Th6,WELLORD1:def 1; end; thus z in W2 & z in [: W2-Seg(y3),W2-Seg(y3) :] implies z in W1 & z in [: W1-Seg(y3),W1-Seg(y3) :] proof assume that A74: z in W2 and A75: z in [: W2-Seg(y3),W2-Seg(y3) :]; consider z1,z2 such that A76: z1 in W2-Seg(y3) and A77: z2 in W2-Seg(y3) and A78: z=[z1,z2] by A75,ZFMISC_1:def 2; A79: z1 in field W1 by A5,A66,A67,A76; z1 in W2-Seg(z2) or (z1=z2 & not z1 in W2-Seg(z2)) by A74,A78, WELLORD1:def 1; then z1 in W1-Seg(z2) or (z1=z2 & not z1 in W1-Seg(z2)) by A7,A66,A67,A77; hence thesis by A6,A65,A66,A67,A75,A78,A79,Th6,WELLORD1:def 1; end; end; hence thesis by WELLORD1:16; end; hence thesis by TARSKI:2; end; hence contradiction by A5,A65,A66,A67; end; A80: C = field W1 implies (W1 c= W2 & for x st x in field W1 holds W1-Seg(x) = W2-Seg(x) ) proof assume A81: C = field W1; [z1,z2] in W1 implies [z1,z2] in W2 proof assume A82: [z1,z2] in W1; then A83: z1 in C by A81,RELAT_1:30; A84: z2 in C by A81,A82,RELAT_1:30; A85: z1 in field W2 by A5,A83; z1 in W1-Seg(z2) or (z1=z2 & not z1 in W1-Seg(z2)) by A82,WELLORD1: def 1; then z1 in W2-Seg(z2) or (z1=z2 & not z1 in W2-Seg(z2)) by A7,A84; hence thesis by A6,A85,Th6,WELLORD1:def 1; end; hence thesis by A7,A81,RELAT_1:def 3; end; C = field W2 implies (W2 c= W1 & for x st x in field W2 holds W2-Seg(x) = W1-Seg(x) ) proof assume A86: C = field W2; [z1,z2] in W2 implies [z1,z2] in W1 proof assume A87: [z1,z2] in W2; then A88: z1 in C by A86,RELAT_1:30; A89: z2 in C by A86,A87,RELAT_1:30; A90: z1 in field W1 by A5,A88; z1 in W2-Seg(z2) or (z1=z2 & not z1 in W2-Seg(z2)) by A87,WELLORD1: def 1; then z1 in W1-Seg(z2) or (z1=z2 & not z1 in W1-Seg(z2)) by A7,A89; hence thesis by A6,A90,Th6,WELLORD1:def 1; end; hence thesis by A7,A86,RELAT_1:def 3; end; hence thesis by A62,A80; end; defpred P[set,set] means ex W st [$1,$2] in W & W in G; consider S such that A91: [x,y] in S iff x in union D & y in union D & P[x,y] from Rel_Existence; take R = S; A92: x in field R implies x in union D & ex W st (x in field W & W in G) proof assume x in field R; then consider y such that A93: ([x,y] in R or [y,x] in R) by Th1; A94: (x in union D & y in union D & ex S st [x,y] in S & S in G) or (y in union D & x in union D & ex S st [y,x] in S & S in G) by A91,A93; thus x in union D by A91,A93; consider S such that A95: ([x,y] in S or [y,x] in S ) and A96: S in G by A94; take S; thus thesis by A95,A96,Th1; end; then x in field R implies x in union D; hence field R c= union D by TARSKI:def 3; A97: W in G implies field W c= field R proof assume A98: W in G; let x; assume x in field W; then consider y such that A99: [x,y] in W or [y,x] in W by Th1; A100: [x,y] in W implies [x,y] in R proof assume A101: [x,y] in W; W in W0 by A2,A98; then ex z1,z2 st z1 in union D & z2 in union D & [x,y]=[z1,z2] by A101,ZFMISC_1:103; hence thesis by A91,A98,A101; end; [y,x] in W implies [y,x] in R proof assume A102: [y,x] in W; W in W0 by A2,A98; then ex z1,z2 st z1 in union D & z2 in union D & [y,x]=[z1,z2] by A102,ZFMISC_1:103; hence thesis by A91,A98,A102; end; hence thesis by A99,A100,Th1; end; A103: R is well-ordering proof A104: R is_reflexive_in field R proof x in field R implies [x,x] in R proof assume A105: x in field R; then A106: x in union D & ex W st (x in field W & W in G) by A92; consider W such that A107: x in field W & W in G by A92,A105; W is well-ordering by A2,A107; then W well_orders field W by WELLORD1:8; then W is_reflexive_in field W by WELLORD1:def 5; then [x,x] in W by A107,RELAT_2:def 1; hence thesis by A91,A106,A107; end; hence thesis by RELAT_2:def 1; end; A108: R is_transitive_in field R proof x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R implies [x,z] in R proof assume that x in field R and y in field R and z in field R and A109: [x,y] in R & [y,z] in R; A110: x in union D & y in union D & ex W st [x,y] in W & W in G by A91,A109; consider W1 such that A111: [x,y] in W1 & W1 in G by A91,A109; A112: y in union D & z in union D & ex W st [y,z] in W & W in G by A91,A109; consider W2 such that A113: [y,z] in W2 & W2 in G by A91,A109; ex W st [x,y] in W & [y,z] in W & W in G proof take W = W2; y in field W1 & y in field W by A111,A113,RELAT_1:30; then A114: W1-Seg(y) = W-Seg(y) by A3,A111,A113; not x in W1-Seg(y) implies [x,y] in W proof assume A115: not x in W1-Seg(y); A116: x in field W1 & y in field W1 by A111,RELAT_1:30; A117: W1 is well-ordering by A2,A111; then A118: [y,x] in W1 by A115,A116,Th6; W1 well_orders field W1 by A117,WELLORD1:8; then W1 is_antisymmetric_in field W1 by WELLORD1:def 5; then A119: x=y by A111,A116,A118,RELAT_2:def 4; A120: y in field W by A113,RELAT_1:30; W is well-ordering by A2,A113; then W well_orders field W by WELLORD1:8; then W is_reflexive_in field W by WELLORD1:def 5; hence thesis by A119,A120,RELAT_2:def 1; end; hence thesis by A113,A114,WELLORD1:def 1; end; then consider W such that A121: [x,y] in W & [y,z] in W & W in G; W is well-ordering by A2,A121; then W well_orders field W by WELLORD1:8; then A122: W is_transitive_in field W by WELLORD1:def 5; x in field W & y in field W & z in field W by A121,RELAT_1:30; then [x,z] in W by A121,A122,RELAT_2:def 8; hence thesis by A91,A110,A112,A121; end; hence thesis by RELAT_2:def 8; end; A123: R is_antisymmetric_in field R proof x in field R & y in field R & [x,y] in R & [y,x] in R implies x=y proof assume that x in field R and y in field R and A124: [x,y] in R & [y,x] in R; consider W1 such that A125: [x,y] in W1 & W1 in G by A91,A124; consider W2 such that A126: [y,x] in W2 & W2 in G by A91,A124; A127: W1 c= W2 implies x=y proof assume A128: W1 c= W2; then A129: x in field W2 & y in field W2 by A125,RELAT_1:30; W2 is well-ordering by A2,A126; then W2 well_orders field W2 by WELLORD1:8; then W2 is_antisymmetric_in field W2 by WELLORD1:def 5; hence thesis by A125,A126,A128,A129,RELAT_2:def 4; end; W2 c= W1 implies x=y proof assume A130: W2 c= W1; then A131: x in field W1 & y in field W1 by A126,RELAT_1:30; W1 is well-ordering by A2,A125; then W1 well_orders field W1 by WELLORD1:8; then W1 is_antisymmetric_in field W1 by WELLORD1:def 5; hence thesis by A125,A126,A130,A131,RELAT_2:def 4; end; hence thesis by A3,A125,A126,A127; end; hence thesis by RELAT_2:def 4; end; A132: R is_connected_in field R proof x in field R & y in field R & x <>y implies [x,y] in R or [y,x] in R proof assume that A133: x in field R and A134: y in field R and A135: x <>y; A136: x in union D & ex W st (x in field W & W in G) by A92,A133; consider W1 such that A137: x in field W1 & W1 in G by A92,A133; A138: y in union D & ex W st (y in field W & W in G) by A92,A134; consider W2 such that A139: y in field W2 & W2 in G by A92,A134; A140: W1 c= W2 implies [x,y] in R or [y,x] in R proof assume W1 c= W2; then A141: field W1 c= field W2 by RELAT_1:31; W2 is well-ordering by A2,A139; then W2 well_orders field W2 by WELLORD1:8; then W2 is_connected_in field W2 by WELLORD1:def 5; then [x,y] in W2 or [y,x] in W2 by A135,A137,A139,A141,RELAT_2: def 6; hence thesis by A91,A136,A138,A139; end; W2 c= W1 implies [x,y] in R or [y,x] in R proof assume W2 c= W1; then A142: field W2 c= field W1 by RELAT_1:31; W1 is well-ordering by A2,A137; then W1 well_orders field W1 by WELLORD1:8; then W1 is_connected_in field W1 by WELLORD1:def 5; then [x,y] in W1 or [y,x] in W1 by A135,A137,A139,A142,RELAT_2: def 6; hence thesis by A91,A136,A137,A138; end; hence thesis by A3,A137,A139,A140; end; hence thesis by RELAT_2:def 6; end; R is_well_founded_in field R proof let Y; assume that A143: Y c= field R and A144: Y <> {}; consider y being Element of Y; y in field R by A143,A144,TARSKI:def 3; then consider W such that A145: y in field W & W in G by A92; W is well-ordering by A2,A145; then W well_orders field W by WELLORD1:8; then A146: W is_well_founded_in field W by WELLORD1:def 5; set A = Y /\ field W; A147: A c= field W by XBOOLE_1:17; A <> {} by A144,A145,XBOOLE_0:def 3; then consider a such that A148: a in A and A149: W-Seg(a) misses A by A146,A147,WELLORD1:def 3; ex b st b in Y & R-Seg(b) misses Y proof take b= a; thus b in Y by A148,XBOOLE_0:def 3; assume not thesis; then consider x being set such that A150: x in R-Seg(b) & x in Y by XBOOLE_0:3; A151: [x,b] in R & x<>b by A150,WELLORD1:def 1; then consider W1 such that A152: [x,b] in W1 & W1 in G by A91; A153: x in field W1 & b in field W1 by A152,RELAT_1:30; x in W1-Seg(b) by A151,A152,WELLORD1:def 1; then A154: x in W-Seg(a) by A3,A145,A147,A148,A152,A153; then [x,a] in W by WELLORD1:def 1; then x in field W by RELAT_1:30; then x in A by A150,XBOOLE_0:def 3; hence contradiction by A149,A154,XBOOLE_0:3; end; hence thesis; end; then R well_orders field R by A104,A108,A123,A132,WELLORD1:def 5; hence thesis by WELLORD1:8; end; A155: for y st y in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y proof let y; assume A156: y in field R; then consider W such that A157: y in field W & W in G by A92; A158: y in union D by A92,A156; A159: field W c= field R by A97,A157; W-Seg(y) = R-Seg(y) proof A160: x in W-Seg(y) implies x in R-Seg(y) proof assume x in W-Seg(y); then A161: [x,y] in W & not x =y by WELLORD1:def 1; then x in field W by RELAT_1:30; then x in union D by A92,A159; then [x,y] in R by A91,A157,A158,A161; hence thesis by A161,WELLORD1:def 1; end; x in R-Seg(y) implies x in W-Seg(y) proof assume x in R-Seg(y); then A162: [x,y] in R & not x =y by WELLORD1:def 1; then consider W1 such that A163: [x,y] in W1 & W1 in G by A91; A164: x in W1-Seg(y) by A162,A163,WELLORD1:def 1; y in field W1 by A163,RELAT_1:30; hence thesis by A3,A157,A163,A164; end; hence thesis by A160,TARSKI:2; end; hence thesis by A2,A157; end; not field R in D proof assume A165: field R in D; set a0=F.(field R); A166: not a0 in field R by A1,A165; reconsider W3 = [: field R,{ a0 } :] as Relation by RELAT_1:6; reconsider W4 = { [a0,a0]} as Relation by RELAT_1:4; field W4 = {a0,a0} by RELAT_1:32; then A167: field W4 = {a0}\/{a0} by ENUMSET1:41; R \/ [: field R,{ a0 }:] \/ {[ a0,a0 ]} = R \/ W3 \/ W4; then reconsider W1=R \/ [: field R,{ a0 }:] \/ {[ a0,a0 ]} as Relation; A168: field W1 =field R \/ { a0 } proof A169: field R <> {} implies field W1 =field R \/ { a0 } proof assume field R <> {}; then A170: field W3 = field R \/ { a0 } by Th3; field W1 =field (R \/ W3) \/ field W4 by RELAT_1:33; then field W1 =field R \/ (field R \/ { a0 }) \/ {a0} by A167,A170,RELAT_1:33 ; then field W1 =(field R \/ field R) \/ { a0 } \/ {a0} by XBOOLE_1:4; then field W1 =(field R \/ field R) \/ ({ a0 } \/ {a0}) by XBOOLE_1:4 ; hence thesis; end; field R = {} implies field W1 =field R \/ { a0 } proof assume A171: field R = {}; A172: field W3 = {} proof consider z3 being Element of field W3; assume field W3 <> {}; then ex z2 st [z3,z2] in W3 or [z2,z3] in W3 by Th1; hence contradiction by A171,ZFMISC_1:113; end; field W1 =field (R \/ W3) \/ field W4 by RELAT_1:33; then field W1 =field R \/ {} \/ {a0} by A167,A172,RELAT_1:33; hence thesis; end; hence thesis by A169; end; A173:x in field W1 implies x in field R or x = a0 proof assume x in field W1; then x in field R or x in {a0} by A168,XBOOLE_0:def 2; hence thesis by TARSKI:def 1; end; A174: [: union D, union D :] is Relation by RELAT_1:6; A175: [x,y] in W1 iff [x,y] in R or [x,y] in W3 or [x,y] in W4 proof [x,y] in W1 iff ([x,y] in (R \/ W3) or [x,y] in W4) by XBOOLE_0:def 2; hence thesis by XBOOLE_0:def 2; end; A176: [x,y] in W1 & y in field R implies [x,y] in R & x in field R proof assume A177: [x,y] in W1 & y in field R; then A178: [x,y] in R or [x,y] in W3 or [x,y] in W4 by A175; A179: not [x,y] in W3 by A166,A177,ZFMISC_1:129; A180: not [x,y] in W4 proof assume [x,y] in W4; then [x,y] = [a0,a0] by TARSKI:def 1; hence contradiction by A166,A177,ZFMISC_1:33; end; hence [x,y] in R by A175,A177,A179; thus thesis by A178,A180,RELAT_1:30,ZFMISC_1:129; end; A181: y in field R implies W1-Seg(y) = R-Seg(y) proof assume A182: y in field R; A183: x in W1-Seg(y) implies x in R-Seg(y) proof assume x in W1-Seg(y); then A184: [x,y] in W1 & x<>y by WELLORD1:def 1; then [x,y] in R by A176,A182; hence thesis by A184,WELLORD1:def 1; end; x in R-Seg(y) implies x in W1-Seg(y) proof assume x in R-Seg(y); then A185: [x,y] in R & x<>y by WELLORD1:def 1; then [x,y] in W1 by A175; hence thesis by A185,WELLORD1:def 1; end; hence thesis by A183,TARSKI:2; end; A186: W1 in W0 proof for x,y holds [x,y] in W1 implies [x,y] in [: union D, union D :] proof let x,y; assume [x,y] in W1; then x in field W1 & y in field W1 by RELAT_1:30; then ( x in field R or x=a0) & (y in field R or y=a0) by A173; then x in union D & y in union D by A1,A92,A165; hence thesis by ZFMISC_1:def 2; end; then W1 c= [: union D,union D :] by A174,RELAT_1:def 3; hence thesis; end; A187: W1 is well-ordering proof A188: W1 is_reflexive_in field W1 proof x in field W1 implies [x,x] in W1 proof assume A189: x in field W1; A190: x in field R implies [x,x] in W1 proof assume A191: x in field R; R well_orders field R by A103,WELLORD1:8; then R is_reflexive_in field R by WELLORD1:def 5; then [x,x] in R by A191,RELAT_2:def 1; hence thesis by A175; end; x = a0 implies [x,x] in W1 proof assume A192: x=a0; [a0,a0] in W4 by TARSKI:def 1; hence thesis by A175,A192; end; hence thesis by A173,A189,A190; end; hence thesis by RELAT_2:def 1; end; A193: W1 is_transitive_in field W1 proof x in field W1 & y in field W1 & z in field W1 & [x,y] in W1 & [y,z] in W1 implies [x,z] in W1 proof assume that A194: x in field W1 and A195: y in field W1 and A196: z in field W1 and A197: [x,y] in W1 & [y,z] in W1; A198: z in field R implies [x,z] in W1 proof assume A199: z in field R; then A200: [y,z] in R & y in field R by A176,A197; then A201: [x,y] in R & x in field R by A176,A197; R well_orders field R by A103,WELLORD1:8; then R is_transitive_in field R by WELLORD1:def 5; then [x,z] in R by A199,A200,A201,RELAT_2:def 8; hence thesis by A175; end; z = a0 implies [x,z] in W1 proof assume A202: z = a0; A203: y in field R implies [x,z] in W1 proof assume y in field R; then [x,y] in R & x in field R by A176,A197; then [x,z] in W3 by A202,ZFMISC_1:129; hence thesis by A175; end; y = a0 implies [x,z] in W1 proof A204: x in field R implies [x,z] in W1 proof assume x in field R; then [x,z] in W3 by A202,ZFMISC_1:129; hence thesis by A175; end; x = a0 implies [x,z] in W1 proof assume x = a0; then [x,z] in W4 by A202,TARSKI:def 1; hence thesis by A175; end; hence thesis by A173,A194,A204; end; hence thesis by A173,A195,A203; end; hence thesis by A173,A196,A198; end; hence thesis by RELAT_2:def 8; end; A205: W1 is_antisymmetric_in field W1 proof x in field W1 & y in field W1 & [x,y] in W1 & [y,x] in W1 implies x=y proof assume that A206: x in field W1 and A207: y in field W1 and A208: [x,y] in W1 & [y,x] in W1; A209: y in field R or y =a0 by A173,A207; A210: x in field R implies x=y proof assume A211: x in field R; then A212: [y,x] in R & y in field R by A176,A208; then A213: [x,y] in R by A176,A208; R well_orders field R by A103,WELLORD1:8; then R is_antisymmetric_in field R by WELLORD1:def 5; hence thesis by A211,A212,A213,RELAT_2:def 4; end; y in field R implies x=y proof assume A214: y in field R; then A215: [x,y] in R & x in field R by A176,A208; then A216: [y,x] in R by A176,A208; R well_orders field R by A103,WELLORD1:8; then R is_antisymmetric_in field R by WELLORD1:def 5; hence thesis by A214,A215,A216,RELAT_2:def 4; end; hence thesis by A173,A206,A209,A210; end; hence thesis by RELAT_2:def 4; end; A217: W1 is_connected_in field W1 proof x in field W1 & y in field W1 & x <>y implies [x,y] in W1 or [y,x] in W1 proof assume that A218: x in field W1 and A219: y in field W1 and A220: x <>y; A221: x in field R & y in field R implies [x,y] in W1 or [y,x] in W1 proof assume A222: x in field R & y in field R; R well_orders field R by A103,WELLORD1:8; then R is_connected_in field R by WELLORD1:def 5; then [x,y] in R or [y,x] in R by A220,A222,RELAT_2:def 6 ; hence thesis by A175; end; A223: not x in field R implies [x,y] in W1 or [y,x] in W1 proof assume not x in field R; then A224: x = a0 by A173,A218; A225: y = a0 implies [x,y] in W1 or [y,x] in W1 proof assume y = a0; then [x,y] in W4 by A224,TARSKI:def 1; hence thesis by A175; end; y in field R implies [x,y] in W1 or [y,x] in W1 proof assume y in field R; then [y,x] in W3 by A224,ZFMISC_1:129; hence thesis by A175; end; hence thesis by A173,A219,A225; end; not y in field R implies [x,y] in W1 or [y,x] in W1 proof assume not y in field R; then A226: y = a0 by A173,A219; A227: x = a0 implies [y,x] in W1 or [x,y] in W1 proof assume x = a0; then [y,x] in W4 by A226,TARSKI:def 1; hence thesis by A175; end; x in field R implies [y,x] in W1 or [x,y] in W1 proof assume x in field R; then [x,y] in W3 by A226,ZFMISC_1:129; hence thesis by A175; end; hence thesis by A173,A218,A227; end; hence thesis by A221,A223; end; hence thesis by RELAT_2:def 6; end; W1 is_well_founded_in field W1 proof let Y; assume that A228: Y c= field W1 and A229: Y <> {}; R well_orders field R by A103,WELLORD1:8; then A230: R is_well_founded_in field R by WELLORD1:def 5; A231: Y c= field R implies ex a st a in Y & W1-Seg(a) misses Y proof assume A232: Y c= field R; then consider b such that A233: b in Y & R-Seg(b) misses Y by A229,A230,WELLORD1:def 3; take b; thus thesis by A181,A232,A233; end; not Y c=field R implies ex a st a in Y & W1-Seg(a) misses Y proof assume not Y c= field R; A234: (field R) /\ Y = {} implies ex a st a in Y & W1-Seg(a) misses Y proof assume A235: (field R) /\ Y = {}; consider y being Element of Y; A236: not y in field R by A229,A235,XBOOLE_0:def 3; y in field W1 by A228,A229,TARSKI:def 3; then A237: y = a0 by A173,A236; W1-Seg(a0) c= field R proof let z be set; assume z in W1-Seg(a0); then A238: [z,a0] in W1 & z <> a0 by WELLORD1:def 1; then z in field W1 by RELAT_1:30; hence thesis by A173,A238; end; then W1-Seg(y) /\ Y c= {} by A235,A237,XBOOLE_1:26; then W1-Seg(y) /\ Y = {} by XBOOLE_1:3; then W1-Seg(y) misses Y by XBOOLE_0:def 7; hence thesis by A229; end; not (field R) /\ Y = {} implies ex a st a in Y & W1-Seg(a) misses Y proof assume A239: not (field R) /\ Y = {}; set X = (field R) /\ Y; A240: X c= field R by XBOOLE_1:17; then consider y such that A241: y in X & R-Seg(y) misses X by A230,A239,WELLORD1:def 3; A242: y in Y by A241,XBOOLE_0:def 3; A243: R-Seg(y) /\ X = {} by A241,XBOOLE_0:def 7; R-Seg(y) /\ Y c= R-Seg(y) /\ X proof let x; assume x in R-Seg(y) /\ Y; then A244: x in R-Seg(y) & x in Y by XBOOLE_0:def 3; then [x,y] in R by WELLORD1:def 1; then x in field R by RELAT_1:30; then x in X by A244,XBOOLE_0:def 3; hence thesis by A244,XBOOLE_0:def 3; end; then R-Seg(y) /\ Y = {} by A243,XBOOLE_1:3; then W1-Seg(y) /\ Y = {} by A181,A240,A241; then W1-Seg(y) misses Y by XBOOLE_0:def 7; hence thesis by A242; end; hence thesis by A234; end; hence thesis by A231; end; then W1 well_orders field W1 by A188,A193,A205,A217,WELLORD1:def 5; hence thesis by WELLORD1:8; end; for y st y in field W1 holds W1-Seg(y) in D & F.(W1-Seg(y)) = y proof let y; assume y in field W1; then A245: y in field R or y=a0 by A173; A246: y in field R implies W1-Seg(y) = R-Seg(y) proof assume A247:y in field R; A248: x in W1-Seg(y) implies x in R-Seg(y) proof assume x in W1-Seg(y); then A249: [x,y] in W1 & not x=y by WELLORD1:def 1; then [x,y] in (R \/ W3) or [x,y] in W4 by XBOOLE_0:def 2; then A250: [x,y] in R or [x,y] in W3 or [x,y] in W4 by XBOOLE_0:def 2; [x,y] in W4 implies [x,y] = [a0,a0] by TARSKI:def 1; hence thesis by A166,A247,A249,A250,WELLORD1:def 1,ZFMISC_1:33,129; end; x in R-Seg(y) implies x in W1-Seg(y) proof assume x in R-Seg(y); then A251: [x,y] in R & not x=y by WELLORD1:def 1; then [x,y] in R \/ W3 by XBOOLE_0:def 2; then [x,y] in W1 by XBOOLE_0:def 2; hence thesis by A251,WELLORD1:def 1; end; hence thesis by A248,TARSKI:2; end; W1-Seg(a0) in D & F.(W1-Seg(a0)) = a0 proof W1-Seg(a0) = field R proof A252: x in W1-Seg(a0) implies x in field R proof assume x in W1-Seg(a0); then A253: [x,a0] in W1 & not x=a0 by WELLORD1:def 1; then x in field W1 by RELAT_1:30; hence thesis by A173,A253; end; x in field R implies x in W1-Seg(a0) proof assume A254:x in field R; then [x,a0] in W3 by ZFMISC_1:129; then [x,a0] in R \/ W3 by XBOOLE_0:def 2; then [x,a0] in W1 by XBOOLE_0:def 2; hence thesis by A166,A254,WELLORD1:def 1; end; hence thesis by A252,TARSKI:2; end; hence thesis by A165; end; hence thesis by A155,A245,A246; end; then W1 in G by A2,A186,A187; then A255: field W1 c= field R by A97; A256: {[ a0,a0 ]} c= W1 by XBOOLE_1:7; [ a0,a0 ] in {[ a0,a0 ]} by TARSKI:def 1; then a0 in field W1 by A256,RELAT_1:30; hence contradiction by A1,A165,A255; end; hence thesis by A103,A155; end; Lm1: X,M are_equipotent iff ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2 proof A1: X,M are_equipotent implies ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2 proof assume ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2; hence thesis; end; ( ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2 ) implies X,M are_equipotent proof assume ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2; hence ex Z st (for x st x in X ex y st y in M & [x,y] in Z) & (for y st y in M ex x st x in X & [x,y] in Z) & for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2; end; hence thesis by A1; end; theorem for N ex R st R is well-ordering & field R = N proof let N; consider M such that A1: N in M and A2: (for X,Y holds X in M & Y c= X implies Y in M) and A3: (for X holds X in M implies bool X in M) and A4: (for X holds X c= M implies X,M are_equipotent or X in M) by ZFMISC_1:136; defpred P[set] means not $1,M are_equipotent; consider D such that A5: A in D iff A in bool M & P[A] from Separation; A6: union D c= M proof let x; assume x in union D; then consider A such that A7: x in A & A in D by TARSKI:def 4; A in bool M & not A,M are_equipotent by A5,A7; hence thesis by A7; end; set F = id D; for Z st Z in D holds not F.Z in Z & F.Z in union D proof let Z; assume A8: Z in D; not Z in Z; hence not F.Z in Z by A8,FUNCT_1:35; X in D implies X in union D proof assume X in D; then X in bool M & not X,M are_equipotent by A5; then A9: X in M by A4; A10: { X } c= M proof x in {X} implies x in M by A9,TARSKI:def 1; hence thesis by TARSKI:def 3; end; not { X },M are_equipotent proof assume { X },M are_equipotent; then consider Z such that (for x st x in { X } ex y st y in M & [x,y] in Z) and A11: (for y st y in M ex x st x in { X } & [x,y] in Z) and A12: for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2 by Lm1; A13: bool X in M by A3,A9; A14: X <> bool X proof assume X = bool X; then not X in bool X; hence contradiction by ZFMISC_1:def 1; end; consider x such that A15: x in {X} & [x,X] in Z by A9,A11; consider y such that A16: y in {X} & [y,bool X] in Z by A11,A13; x=X by A15,TARSKI:def 1; then y=x by A16,TARSKI:def 1; hence contradiction by A12,A14,A15,A16; end; then A17: { X } in D by A5,A10; X in { X } by TARSKI:def 1; hence thesis by A17,TARSKI:def 4; end; then Z in union D by A8; hence thesis by A8,FUNCT_1:35; end; then consider S such that A18: field S c= union D and A19: S is well-ordering and A20: not field S in D and for y st y in field S holds S-Seg(y) in D & F.(S-Seg(y)) = y by Th8; not field S c= M or field S,M are_equipotent by A5,A20; then consider Z such that A21: (for x st x in field S ex y st y in M & [x,y] in Z) and A22: (for y st y in M ex x st x in field S & [x,y] in Z) and A23: for x,z1,y,z2 st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2 by A6,A18,Lm1,XBOOLE_1:1; defpred P[set,set] means [$2,$1] in Z; A24: for x,z1,z2 st x in M & P[x,z1] & P[x,z2] holds z1 = z2 by A23; A25: for x st x in M ex y st P[x,y] proof let x; assume x in M; then ex y st y in field S & [y,x] in Z by A22; hence thesis; end; consider H such that A26: dom H = M and A27: for x st x in M holds P[x, H.x] from FuncEx(A24,A25); for z1,z2 st z1 in dom H & z2 in dom H & H.z1 = H.z2 holds z1 = z2 proof let z1,z2; assume A28: z1 in dom H & z2 in dom H & H.z1 = H.z2; then [H.z1,z1] in Z & [H.z2,z2] in Z by A26,A27; hence thesis by A23,A28; end; then A29: H is one-to-one by FUNCT_1:def 8; defpred P[set] means ex x,y st $1=[x,y] & [H.x,H.y] in S; consider W0 such that A30: z in W0 iff z in [: M,M :] & P[z] from Separation; z in W0 implies ex x,y st z=[x,y] proof assume z in W0; then ex z1,z2 st z=[z1,z2] & [H.z1,H.z2] in S by A30; hence thesis; end; then reconsider W0 as Relation by RELAT_1:def 1; A31: rng H = field S proof A32: x in rng H implies x in field S proof assume x in rng H; then consider z1 such that A33: z1 in dom H and A34: x = H.z1 by FUNCT_1:def 5; A35: ex z2 st z2 in field S & [z2,z1] in Z by A22,A26,A33; [x,z1] in Z by A26,A27,A33,A34; hence thesis by A23,A35; end; x in field S implies x in rng H proof assume x in field S; then consider y such that A36: y in M and A37: [x,y] in Z by A21; set z1= H.y; A38: z1 in rng H by A26,A36,FUNCT_1:def 5; [z1,y] in Z by A27,A36; hence thesis by A23,A37,A38; end; hence thesis by A32,TARSKI:2; end; A39: field W0 = M proof A40: z in field W0 implies z in M proof assume z in field W0; then consider z1 such that A41: [z,z1] in W0 or [z1,z] in W0 by Th1; A42: [z,z1] in W0 implies z in M proof assume [z,z1] in W0; then [z,z1] in [: M,M :] by A30; hence thesis by ZFMISC_1:106; end; [z1,z] in W0 implies z in M proof assume [z1,z] in W0; then [z1,z] in [: M,M :] by A30; hence thesis by ZFMISC_1:106; end; hence thesis by A41,A42; end; z in M implies z in field W0 proof assume A43: z in M; ex z1 st [z,z1] in W0 or [z1,z] in W0 proof H.z in field S by A26,A31,A43,FUNCT_1:def 5; then consider z2 such that A44: [H.z,z2] in S or [z2,H.z] in S by Th1; A45: [z2,H.z] in S implies ex z1 st [z,z1] in W0 or [z1,z] in W0 proof assume A46: [z2,H.z] in S; then z2 in rng H by A31,RELAT_1:30; then consider z3 such that A47: z3 in dom H and A48: z2=H.z3 by FUNCT_1:def 5; A49: [z3,z] in [: M,M :] by A26,A43,A47,ZFMISC_1:106; take z3; thus thesis by A30,A46,A48,A49; end; [H.z,z2] in S implies ex z1 st [z,z1] in W0 or [z1,z] in W0 proof assume A50: [H.z,z2] in S; then z2 in rng H by A31,RELAT_1:30; then consider z3 such that A51: z3 in dom H and A52: z2=H.z3 by FUNCT_1:def 5; A53: [z,z3] in [: M,M :] by A26,A43,A51,ZFMISC_1:106; take z3; thus thesis by A30,A50,A52,A53; end; hence thesis by A44,A45; end; hence thesis by Th1; end; hence thesis by A40,TARSKI:2; end; for a,b holds [a,b] in W0 iff a in field W0 & b in field W0 & [H.a,H.b] in S proof let a,b; A54: [a,b] in W0 implies a in field W0 & b in field W0 & [H.a,H.b] in S proof assume A55: [a,b] in W0; then A56: [a,b] in [: M,M :] & ex x,y st [a,b]=[x,y] & [H.x,H.y] in S by A30; consider x,y such that A57: [a,b] = [x,y] and A58: [H.x,H.y] in S by A30,A55; a=x & b=y by A57,ZFMISC_1:33; hence thesis by A39,A56,A58,ZFMISC_1:106; end; a in field W0 & b in field W0 & [H.a,H.b] in S implies [a,b] in W0 proof assume A59:a in field W0 & b in field W0 & [H.a,H.b] in S; then [a,b] in [: M,M :] by A39,ZFMISC_1:106; hence thesis by A30,A59; end; hence thesis by A54; end; then H is_isomorphism_of W0,S by A26,A29,A31,A39,WELLORD1:def 7; then (H") is_isomorphism_of S, W0 by WELLORD1:49; then A60: W0 is well-ordering by A19,WELLORD1:54; defpred P[set,set] means $2={$1}; A61: for x,z1,z2 st x in N & P[x,z1] & P[x,z2] holds z1 = z2; A62: for x st x in N ex y st P[x,y]; consider H1 such that A63: dom H1 = N and A64: for x st x in N holds P[x, H1.x] from FuncEx(A61,A62); for z1,z2 st z1 in dom H1 & z2 in dom H1 & H1.z1 = H1.z2 holds z1 = z2 proof let z1,z2; assume A65: z1 in dom H1 & z2 in dom H1 & H1.z1 = H1.z2; then A66: H1.z1={z1} & H1.z2={z2} by A63,A64; then z1 in H1.z2 by A65,TARSKI:def 1; hence thesis by A66,TARSKI:def 1; end; then A67: H1 is one-to-one by FUNCT_1:def 8; A68: rng H1 c= M proof let x; assume x in rng H1; then consider y such that A69: y in dom H1 and A70: x = H1.y by FUNCT_1:def 5; A71: x = { y } by A63,A64,A69,A70; { y } c= N proof z1 in { y } implies z1 in N by A63,A69,TARSKI:def 1; hence thesis by TARSKI:def 3; end; hence thesis by A1,A2,A71; end; set S1=W0 |_2 rng H1; A72: S1 is well-ordering by A60,WELLORD1:32; A73: field S1 = rng H1 by A39,A60,A68,WELLORD1:39; defpred P[set] means ex x,y st $1=[x,y] & [H1.x,H1.y] in S1; consider W00 such that A74: z in W00 iff z in [: N,N :] & P[z] from Separation; z in W00 implies ex x,y st z=[x,y] proof assume z in W00; then ex z1,z2 st z=[z1,z2] & [H1.z1,H1.z2] in S1 by A74; hence thesis; end; then reconsider W00 as Relation by RELAT_1:def 1; A75: field W00 = N proof A76: z in field W00 implies z in N proof assume z in field W00; then consider z1 such that A77: [z,z1] in W00 or [z1,z] in W00 by Th1; A78: [z,z1] in W00 implies z in N proof assume [z,z1] in W00; then [z,z1] in [: N,N :] by A74; hence thesis by ZFMISC_1:106; end; [z1,z] in W00 implies z in N proof assume [z1,z] in W00; then [z1,z] in [: N,N :] by A74; hence thesis by ZFMISC_1:106; end; hence thesis by A77,A78; end; z in N implies z in field W00 proof assume A79: z in N; ex z1 st [z,z1] in W00 or [z1,z] in W00 proof H1.z in field S1 by A63,A73,A79,FUNCT_1:def 5; then consider z2 such that A80: [H1.z,z2] in S1 or [z2,H1.z] in S1 by Th1; A81: [z2,H1.z] in S1 implies ex z1 st [z,z1] in W00 or [z1,z] in W00 proof assume A82: [z2,H1.z] in S1; then z2 in rng H1 by A73,RELAT_1:30; then consider z3 such that A83: z3 in dom H1 and A84: z2=H1.z3 by FUNCT_1:def 5; A85: [z3,z] in [: N,N :] by A63,A79,A83,ZFMISC_1:106; take z3; thus thesis by A74,A82,A84,A85; end; [H1.z,z2] in S1 implies ex z1 st [z,z1] in W00 or [z1,z] in W00 proof assume A86: [H1.z,z2] in S1; then z2 in rng H1 by A73,RELAT_1:30; then consider z3 such that A87: z3 in dom H1 and A88: z2=H1.z3 by FUNCT_1:def 5; A89: [z,z3] in [: N,N :] by A63,A79,A87,ZFMISC_1:106; take z3; thus thesis by A74,A86,A88,A89; end; hence thesis by A80,A81; end; hence thesis by Th1; end; hence thesis by A76,TARSKI:2; end; for a,b holds [a,b] in W00 iff a in field W00 & b in field W00 & [H1.a,H1.b] in S1 proof let a,b; A90: [a,b] in W00 implies a in field W00 & b in field W00 & [H1.a,H1.b] in S1 proof assume A91: [a,b] in W00; then A92: [a,b] in [: N,N :] & ex x,y st [a,b]=[x,y] & [H1.x,H1.y] in S1 by A74; consider x,y such that A93: [a,b] = [x,y] and A94: [H1.x,H1.y] in S1 by A74,A91; a=x & b=y by A93,ZFMISC_1:33; hence thesis by A75,A92,A94,ZFMISC_1:106; end; a in field W00 & b in field W00 & [H1.a,H1.b] in S1 implies [a,b] in W00 proof assume A95:a in field W00 & b in field W00 & [H1.a,H1.b] in S1; then [a,b] in [: N,N :] by A75,ZFMISC_1:106; hence thesis by A74,A95; end; hence thesis by A90; end; then H1 is_isomorphism_of W00,S1 by A63,A67,A73,A75,WELLORD1:def 7; then (H1") is_isomorphism_of S1, W00 by WELLORD1:49; then W00 is well-ordering by A72,WELLORD1:54; hence thesis by A75; end;

Back to top