:: Zermelo Theorem and Axiom of Choice. The correspondence of
:: well ordering relations and ordinal numbers
:: by Grzegorz Bancerek
::
:: Received June 26, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, ORDINAL1, TARSKI, RELAT_2, WELLORD1, XBOOLE_0, SUBSET_1,
ZFMISC_1, FUNCT_1, WELLORD2;
notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, RELAT_1, RELAT_2,
FUNCT_1, WELLORD1, ORDINAL1;
constructors RELAT_2, ORDINAL1, WELLORD1, MCART_1, XTUPLE_0;
registrations RELAT_1, FUNCT_1, ORDINAL1, WELLORD1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, RELAT_2, WELLORD1;
equalities TARSKI, XBOOLE_0, RELAT_1, WELLORD1;
expansions TARSKI, XBOOLE_0, FUNCT_1, RELAT_2, WELLORD1;
theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ORDINAL1,
XBOOLE_0, XTUPLE_0;
schemes FUNCT_1, RELAT_1, ORDINAL1, XBOOLE_0;
begin
reserve X,Y,Z for set,
a,b,c,d,x,y,z,u for object,
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[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 & D1 c= D2;
consider R such that
A1: for x,y being object holds [x,y] in R iff x in X & y in X & P[x,y]
from RELAT_1:sch 1;
take R;
thus field R = X
proof
thus for x being object holds x in field R implies x in X
proof let x be object;
A2: now
assume x in dom R;
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
hence thesis by A1;
end;
A3: now
assume x in rng R;
then ex y being object st [y,x] in R by XTUPLE_0:def 13;
hence thesis by A1;
end;
assume x in field R;
hence thesis by A2,A3,XBOOLE_0:def 3;
end;
let x be object;
assume x in X;
then [x,x] in R by A1;
hence thesis by RELAT_1:15;
end;
let Y,Z such that
A4: Y in X & Z in X;
hereby assume
[Y,Z] in R;
then P[Y,Z] by A1;
hence Y c= Z;
end;
thus thesis by A1,A4;
end;
uniqueness
proof
let R1,R2 be Relation such that
A5: field R1 = X and
A6: for Y,Z st Y in X & Z in X holds [Y,Z] in R1 iff Y c= Z and
A7: field R2 = X and
A8: for Y,Z st Y in X & Z in X holds [Y,Z] in R2 iff Y c= Z;
let x,y be object;
thus [x,y] in R1 implies [x,y] in R2
proof
assume
A9: [x,y] in R1;
then
A10: x in field R1 & y in field R1 by RELAT_1:15;
reconsider x,y as set by TARSKI:1;
x c= y by A5,A6,A9,A10;
hence thesis by A5,A8,A10;
end;
assume
A11: [x,y] in R2;
then
A12: x in field R2 & y in field R2 by RELAT_1:15;
reconsider x,y as set by TARSKI:1;
x c= y by A7,A8,A11,A12;
hence thesis by A6,A7,A12;
end;
end;
::$CT 6
registration
let X;
cluster RelIncl X -> reflexive;
coherence
proof
A1: field RelIncl X = X by Def1;
let a be object;
assume a in field RelIncl X;
hence thesis by A1,Def1;
end;
cluster RelIncl X -> transitive;
coherence
proof
let a,b,c be object such that
A2: a in field RelIncl X and
A3: b in field RelIncl X and
A4: c in field RelIncl X and
A5: [a,b] in RelIncl X & [b,c] in RelIncl X;
reconsider a,b,c as set by TARSKI:1;
field RelIncl X = X by Def1;
then a c= b & b c= c by A2,A3,A4,A5,Def1;
then
A6: a c= c;
a in X & c in X by A2,A4,Def1;
hence thesis by A6,Def1;
end;
cluster RelIncl X -> antisymmetric;
coherence
proof
A7: field RelIncl X = X by Def1;
let a,b be object;
assume
A8: a in field RelIncl X & b in field RelIncl X & [a,b] in RelIncl X & [
b,a ] in RelIncl X;
reconsider a,b as set by TARSKI:1;
a c= b & b c= a by A7,Def1,A8;
hence thesis by XBOOLE_0:def 10;
end;
end;
registration
let A;
cluster RelIncl A -> connected;
coherence
proof
let a,b be object such that
A1: a in field RelIncl A & b in field RelIncl A and
a <> b;
A2: field RelIncl A = A by Def1;
then reconsider Y = a, Z = b as Ordinal by A1;
Y c= Z or Z c= Y;
hence thesis by A1,A2,Def1;
end;
cluster RelIncl A -> well_founded;
coherence
proof
let Y;
assume that
A3: Y c= field RelIncl A and
A4: Y <> {};
defpred P[set] means $1 in Y;
set x = the Element of Y;
A5: field RelIncl A = A by Def1;
then x in A by A3,A4;
then reconsider x as Ordinal;
x in Y by A4;
then
A6: ex B st P[B];
consider B such that
A7: P[B] & for C st P[C] holds B c= C from ORDINAL1:sch 1(A6);
reconsider x = B as set;
take x;
thus x in Y by A7;
set y = the Element of (RelIncl A)-Seg(x) /\ Y;
assume
A8: (RelIncl A)-Seg(x) /\ Y <> {};
then
A9: y in Y by XBOOLE_0:def 4;
then reconsider C = y as Ordinal by A3,A5;
A10: y in (RelIncl A)-Seg(x) by A8,XBOOLE_0:def 4;
then [y,x] in RelIncl A by WELLORD1:1;
then
A11: C c= B by A3,A5,A7,A9,Def1;
A12: y <> x by A10,WELLORD1:1;
B c= C by A7,A9;
hence contradiction by A12,A11;
end;
end;
theorem Th1:
Y c= X implies (RelIncl X) |_2 Y = RelIncl Y
proof
assume
A1: Y c= X;
let a,b be object;
thus [a,b] in (RelIncl X) |_2 Y implies [a,b] in RelIncl Y
proof
assume
A2: [a,b] in (RelIncl X) |_2 Y;
then [a,b] in [:Y,Y:] by XBOOLE_0:def 4;
then
A3: a in Y & b in Y by ZFMISC_1:87;
reconsider a,b as set by TARSKI:1;
[a,b] in RelIncl X by A2,XBOOLE_0:def 4;
then a c= b by A1,A3,Def1;
hence thesis by A3,Def1;
end;
assume
A4: [a,b] in RelIncl Y;
then
A5: a in field RelIncl Y & b in field RelIncl Y by RELAT_1:15;
reconsider a,b as set by TARSKI:1;
A6: field RelIncl Y = Y by Def1;
then a c= b by A4,A5,Def1;
then
A7: [a,b] in RelIncl X by A1,A5,A6,Def1;
[a,b] in [:Y,Y:] by A5,A6,ZFMISC_1:87;
hence thesis by A7,XBOOLE_0:def 4;
end;
theorem Th2:
for A,X st X c= A holds RelIncl X is well-ordering
proof
let A,X;
(RelIncl A) |_2 X is well-ordering by WELLORD1:25;
hence thesis by Th1;
end;
reserve H for Function;
theorem Th3:
A in B implies A = (RelIncl B)-Seg(A)
proof
assume
A1: A in B;
thus for a being object holds a in A implies a in (RelIncl B)-Seg(A)
proof let a be object;
assume
A2: a in A;
then reconsider C = a as Ordinal;
reconsider a as set by TARSKI:1;
not a in a; then
A3: a <> A by A2;
A4: A c= B by A1,ORDINAL1:def 2;
C c= A by A2,ORDINAL1:def 2;
then [C,A] in RelIncl B by A1,A2,A4,Def1;
hence thesis by A3,WELLORD1:1;
end;
let a be object;
assume
A5: a in (RelIncl B)-Seg(A);
then
A6: a <> A by WELLORD1:1;
A7: [a,A] in RelIncl B by A5,WELLORD1:1;
then
A8: a in field RelIncl B by RELAT_1:15;
A9: field RelIncl B = B by Def1;
then reconsider C = a as Ordinal by A8;
C c= A by A1,A7,A8,A9,Def1;
then C c< A by A6;
hence thesis by ORDINAL1:11;
end;
theorem Th4:
RelIncl A,RelIncl B are_isomorphic implies A = B
proof
A1: field RelIncl A = A by Def1;
assume
A2: RelIncl A,RelIncl B are_isomorphic;
A3: now
A4: field RelIncl B = B by Def1;
assume
A5: A in B;
then A = (RelIncl B)-Seg(A) by Th3;
then RelIncl A = (RelIncl B) |_2 ((RelIncl B)-Seg(A)) by A4,Th1,WELLORD1:9;
hence contradiction by A2,A5,A4,WELLORD1:40,46;
end;
assume A <> B;
then
A6: A in B or B in A by ORDINAL1:14;
then B = (RelIncl A)-Seg(B) by A3,Th3;
then RelIncl B = (RelIncl A) |_2 ((RelIncl A)-Seg(B)) by A1,Th1,WELLORD1:9;
hence contradiction by A2,A6,A3,A1,WELLORD1:46;
end;
theorem Th5:
R,RelIncl A are_isomorphic & R,RelIncl B are_isomorphic implies A = B
proof
assume that
A1: R,RelIncl A are_isomorphic and
A2: R,RelIncl B are_isomorphic;
RelIncl A,R are_isomorphic by A1,WELLORD1:40;
hence thesis by A2,Th4,WELLORD1:42;
end;
theorem Th6:
for R st R is well-ordering &
for a being object 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;
defpred P[object,object] means
for A holds A = $2 iff R |_2 (R-Seg $1),RelIncl A are_isomorphic;
assume
A2: for a being object st a in field R
ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic;
A3: for a being object st a in field R ex b being object st P[a,b]
proof
let a be object;
assume a in field R;
then consider A such that
A4: 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 A4;
assume R |_2 (R-Seg(a)),RelIncl B are_isomorphic;
hence thesis by A4,Th5;
end;
A5: for b,c,d being object st b in field R & P[b,c] & P[b,d] holds c = d
proof
let b,c,d be object such that
A6: b in field R and
A7: A = c iff R |_2 (R-Seg(b)),RelIncl A are_isomorphic and
A8: B = d iff R |_2 (R-Seg(b)),RelIncl B are_isomorphic;
consider A such that
A9: R |_2 (R-Seg(b)),RelIncl A are_isomorphic by A2,A6;
A = c by A7,A9;
hence thesis by A8,A9;
end;
consider H such that
A10: dom H = field R & for b being object st b in field R holds P[b, H.b] from
FUNCT_1:sch 2(A5,A3);
for a st a in rng H holds a is Ordinal
proof
let b;
assume b in rng H;
then consider c being object such that
A11: c in dom H and
A12: b = H.c by FUNCT_1:def 3;
ex A st R |_2 (R-Seg(c)),RelIncl A are_isomorphic by A2,A10,A11;
hence thesis by A10,A11,A12;
end;
then consider C such that
A13: rng H c= C by ORDINAL1:24;
A14: now
let b be object;
assume
A15: b in rng H;
then consider b9 being object such that
A16: b9 in dom H and
A17: b = H.b9 by FUNCT_1:def 3;
set V = R-Seg(b9);
set P = R |_2 V;
consider A such that
A18: P,RelIncl A are_isomorphic by A2,A10,A16;
let c be object such that
A19: [c,b] in RelIncl C;
A20: A = b by A10,A16,A17,A18;
now
A21: C = field RelIncl C by Def1;
then
A22: c in C by A19,RELAT_1:15;
then reconsider B = c as Ordinal;
b in C by A19,A21,RELAT_1:15;
then
A23: B c= A by A20,A19,A22,Def1;
then
A24: (RelIncl A) |_2 B = RelIncl B by Th1;
assume c <> b;
then
A25: B c< A by A20,A23;
then
A26: B = (RelIncl A)-Seg(B) by Th3,ORDINAL1:11;
A27: A = field RelIncl A by Def1;
RelIncl A,P are_isomorphic by A18,WELLORD1:40;
then
canonical_isomorphism_of(RelIncl A,P) is_isomorphism_of RelIncl A,P
by WELLORD1:def 9;
then consider d being object such that
A28: d in field P and
A29: (RelIncl A) |_2 ((RelIncl A)-Seg(B)),P |_2 (P-Seg(d))
are_isomorphic by A25,A27,ORDINAL1:11,WELLORD1:50;
A30: d in field R by A28,WELLORD1:12;
A31: P-Seg(d) = R-Seg(d) by A1,A28,WELLORD1:12,27;
d in V by A28,WELLORD1:12;
then [d,b9] in R by WELLORD1:1;
then R-Seg(d) c= R-Seg(b9) by A1,A10,A16,A30,WELLORD1:29;
then RelIncl B,R |_2 (R-Seg(d)) are_isomorphic by A29,A26,A24,A31,
WELLORD1:22;
then R |_2 (R-Seg(d)),RelIncl B are_isomorphic by WELLORD1:40;
then B = H.d by A10,A30;
hence c in rng H by A10,A30,FUNCT_1:def 3;
end;
hence c in rng H by A15;
end;
A32: (ex a being object st a in C & rng H = (RelIncl C)-Seg(a))
implies rng H is Ordinal
by Th3;
C = field RelIncl C & RelIncl C is well-ordering by Def1;
then reconsider A = rng H as Ordinal by A13,A14,A32,WELLORD1:28;
take A;
take H;
thus dom H = field R by A10;
thus rng H = field RelIncl A by Def1;
A33: a in dom H implies H.a is Ordinal
proof
assume a in dom H;
then H.a in A by FUNCT_1:def 3;
hence thesis;
end;
thus
A34: H is one-to-one
proof
let a,b be object;
assume that
A35: a in dom H and
A36: b in dom H and
A37: H.a = H.b;
reconsider B = H.a as Ordinal by A33,A35;
R |_2 (R-Seg(b)),RelIncl B are_isomorphic by A10,A36,A37;
then
A38: RelIncl B,R |_2 (R-Seg(b)) are_isomorphic by WELLORD1:40;
R |_2 (R-Seg(a)),RelIncl B are_isomorphic by A10,A35;
then R |_2 (R-Seg(a)),R |_2 (R-Seg(b)) are_isomorphic by A38,WELLORD1:42;
hence thesis by A1,A10,A35,A36,WELLORD1:47;
end;
let a,b be object;
thus [a,b] in R implies a in field R & b in field R & [H.a,H.b] in RelIncl A
proof
set Z = R-Seg(b);
set P = R |_2 Z;
A39: A = field RelIncl A & P is well-ordering by A1,Def1,WELLORD1:25;
assume
A40: [a,b] in R;
hence
A41: a in field R & b in field R by RELAT_1:15;
then reconsider A9 = H.a, B9 = H.b as Ordinal by A10,A33;
A42: R |_2 (R-Seg(b)),RelIncl B9 are_isomorphic by A10,A41;
A43: A9 in A by A10,A41,FUNCT_1:def 3;
A44: B9 in A by A10,A41,FUNCT_1:def 3;
A45: R |_2 (R-Seg(a)),RelIncl A9 are_isomorphic by A10,A41;
now
assume a <> b;
then
A46: a in Z by A40,WELLORD1:1;
then
A47: P-Seg(a) = R-Seg(a) by A1,WELLORD1:27;
Z c= field R by WELLORD1:9;
then
A48: a in field P by A1,A46,WELLORD1:31;
A9 c= A by A43,ORDINAL1:def 2;
then
A49: (RelIncl A) |_2 A9 = RelIncl A9 by Th1;
A9 = (RelIncl A)-Seg(A9) & R-Seg(a) c= R-Seg(b) by A1,A40,A41,A43,Th3,
WELLORD1:29;
then
A50: P |_2 (P-Seg(a)),(RelIncl A) |_2 ((RelIncl A)-Seg(A9))
are_isomorphic by A45,A49,A47,WELLORD1:22;
B9 = (RelIncl A)-Seg(B9) & B9 c= A by A44,Th3,ORDINAL1:def 2;
then P,(RelIncl A) |_2 ((RelIncl A)-Seg(B9)) are_isomorphic by A42,Th1;
hence [A9,B9] in RelIncl A by A43,A44,A39,A48,A50,WELLORD1:51;
end;
hence thesis by A43,Def1;
end;
assume that
A51: a in field R and
A52: b in field R and
A53: [H.a,H.b] in RelIncl A;
assume
A54: not [a,b] in R;
R is_reflexive_in field R by A1,RELAT_2:def 9;
then
A55: a <> b by A51,A54;
R is_connected_in field R by A1,RELAT_2:def 14;
then
A56: [b,a] in R by A51,A52,A54,A55;
then
A57: R-Seg(b) c= R-Seg(a) by A1,A51,A52,WELLORD1:29;
A58: RelIncl A is_antisymmetric_in field RelIncl A by RELAT_2:def 12;
A59: A = field RelIncl A by Def1;
reconsider A9 = H.a, B9 = H.b as Ordinal by A10,A33,A51,A52;
A60: R |_2 (R-Seg(a)),RelIncl A9 are_isomorphic by A10,A51;
A61: R |_2 (R-Seg(b)),RelIncl B9 are_isomorphic by A10,A52;
A62: B9 in A by A10,A52,FUNCT_1:def 3;
then B9 c= A by ORDINAL1:def 2;
then
A63: (RelIncl A) |_2 B9 = RelIncl B9 by Th1;
set Z = R-Seg(a);
set P = R |_2 Z;
A64: A9 in A by A10,A51,FUNCT_1:def 3;
then A9 = (RelIncl A)-Seg(A9) & A9 c= A by Th3,ORDINAL1:def 2;
then
A65: P,(RelIncl A) |_2 ((RelIncl A)-Seg(A9)) are_isomorphic by A60,Th1;
A66: b in Z by A54,A56,WELLORD1:1;
then
A67: P-Seg(b) = R-Seg(b) by A1,WELLORD1:27;
B9 = (RelIncl A)-Seg(B9) by A62,Th3;
then
A68: P |_2 (P-Seg(b)),(RelIncl A) |_2 ((RelIncl A)-Seg(B9)) are_isomorphic
by A61,A63,A67,A57,WELLORD1:22;
Z c= field R by WELLORD1:9;
then
A69: b in field P by A1,A66,WELLORD1:31;
P is well-ordering by A1,WELLORD1:25;
then [B9,A9] in RelIncl A by A69,A64,A62,A59,A65,A68,WELLORD1:51;
then H.a = H.b by A53,A58,A64,A62,A59;
hence contradiction by A10,A34,A51,A52,A55;
end;
theorem Th7:
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[object] means ex A st R |_2 (R-Seg($1)),RelIncl A are_isomorphic;
consider Z such that
A2: for a being object holds a in Z iff a in field R & P[a]
from XBOOLE_0:sch 1;
now
let a be object such that
A3: a in field R and
A4: R-Seg(a) c= Z;
set P = R |_2 (R-Seg(a));
now
let b be object;
assume
A5: b in field P;
then
A6: b in R-Seg(a) by WELLORD1:12;
then
A7: [b,a] in R by WELLORD1:1;
b in field R by A5,WELLORD1:12;
then
A8: R-Seg(b) c= R-Seg(a) by A1,A3,A7,WELLORD1:29;
consider A such that
A9: R |_2 (R-Seg(b)),RelIncl A are_isomorphic by A2,A4,A6;
take A;
P-Seg(b) = R-Seg(b) by A1,A5,WELLORD1:12,27;
hence P |_2 (P-Seg(b)),RelIncl A are_isomorphic by A9,A8,WELLORD1:22;
end;
then ex A st P,RelIncl A are_isomorphic by A1,Th6,WELLORD1:25;
hence a in Z by A2,A3;
end;
then field R c= Z by A1,WELLORD1:33;
then
for a being object st a in field R
ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic
by A2;
hence thesis by A1,Th6;
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,Th7;
uniqueness by Th5;
end;
definition
let A,R;
pred A is_order_type_of R means
A = order_type_of R;
end;
theorem
X c= A implies order_type_of RelIncl X c= A
proof
assume
A1: X c= A;
then
A2: (RelIncl A) |_2 X = RelIncl X by Th1;
A3: RelIncl X is well-ordering by A1,Th2;
A4: now
assume RelIncl A,(RelIncl A) |_2 X are_isomorphic;
then RelIncl X,RelIncl A are_isomorphic by A2,WELLORD1:40;
hence thesis by A3,Def2;
end;
A5: now
given a being object such that
A6: a in A and
A7: (RelIncl A) |_2 ((RelIncl A)-Seg(a)),(RelIncl A) |_2 X are_isomorphic;
reconsider a as Ordinal by A6;
A8: (RelIncl A)-Seg(a) = a by A6,Th3;
A9: a c= A by A6,ORDINAL1:def 2;
then (RelIncl A) |_2 a = RelIncl a by Th1;
then RelIncl X,RelIncl a are_isomorphic by A2,A7,A8,WELLORD1:40;
hence thesis by A3,A9,Def2;
end;
field RelIncl A = A by Def1;
hence thesis by A1,A4,A5,WELLORD1:53;
end;
reserve f,g for Function;
definition
let X,Y;
redefine pred X,Y are_equipotent means :: redefines are_equipotent (TARSKI, definition)
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 be object st x in X ex y be object st y in Y & [x,y] in Z and
A2: for y be object st y in Y ex x be object st x in X & [x,y] in Z and
A3: for x,y,z,u be object st [x,y] in Z & [z,u] in Z holds x = z iff y = u;
set F = Z /\ [:X,Y:];
for x,y,z being object st [x,y] in F & [x,z] in F holds y = z
proof
let x,y,z be object;
assume [x,y] in F & [x,z] in F;
then [x,y] in Z & [x,z] in Z by XBOOLE_0:def 4;
hence thesis by A3;
end;
then reconsider F as Function by FUNCT_1:def 1;
take f = F;
thus f is one-to-one
proof
let x,y be object;
assume that
A4: x in dom f and
A5: y in dom f and
A6: f.x = f.y;
[y,f.y] in f by A5,FUNCT_1:1;
then
A7: [y,f.y] in Z by XBOOLE_0:def 4;
[x,f.x] in f by A4,FUNCT_1:1;
then [x,f.x] in Z by XBOOLE_0:def 4;
hence thesis by A3,A6,A7;
end;
thus dom f c= X
proof
let x be object;
assume x in dom f;
then [x,f.x] in f by FUNCT_1:1;
then [x,f.x] in [:X,Y:] by XBOOLE_0:def 4;
hence thesis by ZFMISC_1:87;
end;
thus X c= dom f
proof
let x be object;
assume
A8: x in X;
then consider y be object such that
A9: y in Y and
A10: [x,y] in Z by A1;
[x,y] in [:X,Y:] by A8,A9,ZFMISC_1:87;
then [x,y] in f by A10,XBOOLE_0:def 4;
hence thesis by FUNCT_1:1;
end;
thus rng f c= Y
proof
let y be object;
assume y in rng f;
then consider x being object such that
A11: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A11,FUNCT_1:1;
then [x,y] in [:X,Y:] by XBOOLE_0:def 4;
hence thesis by ZFMISC_1:87;
end;
thus Y c= rng f
proof
let y be object;
assume
A12: y in Y;
then consider x be object such that
A13: x in X and
A14: [x,y] in Z by A2;
[x,y] in [:X,Y:] by A12,A13,ZFMISC_1:87;
then [x,y] in f by A14,XBOOLE_0:def 4;
then x in dom f & y = f.x by FUNCT_1:1;
hence thesis by FUNCT_1:def 3;
end;
end;
(ex f st f is one-to-one & dom f = X & rng f = Y) implies
ex Z st
(for x be object st x in X ex y be object st y in Y & [x,y] in Z) &
(for y be object st y in Y ex x be object st x in X & [x,y] in Z) &
for x,y,z,u be object st [x,y] in Z & [z,u] in Z holds x = z iff y = u
proof
given f such that
A15: f is one-to-one and
A16: dom f = X and
A17: rng f = Y;
take Z = f;
thus for x be object holds
x in X implies ex y be object st y in Y & [x,y] in Z
proof
let x be object;
assume
A18: x in X;
take f.x;
thus f.x in Y by A16,A17,A18,FUNCT_1:def 3;
thus thesis by A16,A18,FUNCT_1:1;
end;
thus for y be object st y in Y ex x be object st x in X & [x,y] in Z
proof
let y be object such that
A19: y in Y;
take f".y;
A20: dom(f") = rng f by A15,FUNCT_1:33;
then
A21: f".y in rng(f") by A17,A19,FUNCT_1:def 3;
A22: rng(f") = dom f by A15,FUNCT_1:33;
hence f".y in X by A16,A17,A19,A20,FUNCT_1:def 3;
y = f.(f".y) by A15,A17,A19,FUNCT_1:35;
hence thesis by A22,A21,FUNCT_1:1;
end;
let x,y,z,u be object;
assume
A23: [x,y] in Z & [z,u] in Z;
then
A24: x in dom f & z in dom f by FUNCT_1:1;
y = f.x & u = f.z by A23,FUNCT_1:1;
hence thesis by A15,A24;
end;
hence thesis;
end;
reflexivity
proof
let X;
take id X;
thus thesis;
end;
symmetry
proof
let X,Y;
given f such that
A25: f is one-to-one & dom f = X & rng f = Y;
take f";
thus thesis by A25,FUNCT_1:33;
end;
end;
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,RELAT_1:27,28;
end;
theorem Th10:
R well_orders X implies field(R|_2 X) = X & R|_2 X is well-ordering
proof
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
A4: R is_connected_in X and
A5: R is_well_founded_in X;
A6: R|_2 X is_antisymmetric_in X
proof
let x,y be object;
assume that
A7: x in X & y in X and
A8: [x,y] in R|_2 X & [y,x] in R|_2 X;
[x,y] in R & [y,x] in R by A8,XBOOLE_0:def 4;
hence thesis by A3,A7;
end;
A9: R|_2 X is_well_founded_in X
proof
let Y;
assume Y c= X & Y <> {};
then consider a being object such that
A10: a in Y and
A11: R-Seg(a) misses Y by A5;
take a;
thus a in Y by A10;
assume not thesis;
then consider x being object such that
A12: x in (R|_2 X)-Seg(a) and
A13: x in Y by XBOOLE_0:3;
[x,a] in R|_2 X by A12,WELLORD1:1;
then
A14: [x,a] in R by XBOOLE_0:def 4;
x <> a by A12,WELLORD1:1;
then x in R-Seg(a) by A14,WELLORD1:1;
hence contradiction by A11,A13,XBOOLE_0:3;
end;
A15: R|_2 X is_transitive_in X
proof
let x,y,z be object;
assume that
A16: x in X and
A17: y in X and
A18: z in X and
A19: [x,y] in R|_2 X & [y,z] in R|_2 X;
[x,y] in R & [y,z] in R by A19,XBOOLE_0:def 4;
then
A20: [x,z] in R by A2,A16,A17,A18;
[x,z] in [:X,X:] by A16,A18,ZFMISC_1:87;
hence thesis by A20,XBOOLE_0:def 4;
end;
A21: R|_2 X is_connected_in X
proof
let x,y be object;
assume that
A22: x in X & y in X and
A23: x <> y;
A24: [x,y] in [:X,X:] & [y,x] in [:X,X :] by A22,ZFMISC_1:87;
[x,y] in R or [y,x] in R by A4,A22,A23;
hence thesis by A24,XBOOLE_0:def 4;
end;
thus
A25: field(R|_2 X) = X
proof
thus field(R|_2 X) c= X by WELLORD1:13;
let x be object;
assume x in X;
then [x,x] in R & [x,x] in [:X,X:] by A1,ZFMISC_1:87;
then [x,x] in R|_2 X by XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
R|_2 X is_reflexive_in X
proof
let x be object;
assume x in X;
then [x,x] in R & [x,x] in [:X,X:] by A1,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 4;
end;
then R|_2 X well_orders X by A15,A6,A21,A9;
hence thesis by A25,WELLORD1:4;
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;
given f such that
A2: f is one-to-one and
A3: dom f = X and
A4: rng f = field R;
defpred P[object,object] means [f.$1,f.$2] in R;
consider Q being Relation such that
A5: for x,y being object holds [x,y] in Q iff x in X & y in X & P[x,y]
from RELAT_1:sch 1;
take Q;
A6: R is_reflexive_in field R by A1,RELAT_2:def 9;
A7: field Q = X
proof
thus field Q c= X
proof
let x be object;
assume that
A8: x in field Q and
A9: not x in X;
for y being object holds not [y,x] in Q by A5,A9;
then
A10: not x in rng Q by XTUPLE_0:def 13;
for y being object holds not [x,y] in Q by A5,A9;
then not x in dom Q by XTUPLE_0:def 12;
hence contradiction by A8,A10,XBOOLE_0:def 3;
end;
let x be object;
assume
A11: x in X;
then f.x in rng f by A3,FUNCT_1:def 3;
then [f.x,f.x] in R by A6,A4;
then [x,x] in Q by A5,A11;
hence thesis by RELAT_1:15;
end;
f is_isomorphism_of Q,R
by A2,A3,A4,A7,A5;
then f" is_isomorphism_of R,Q by WELLORD1:39;
then Q is well-ordering by A1,WELLORD1:44;
hence thesis by A7,WELLORD1:4;
end;
::$N Zermelo Theorem
theorem Th11:
for X ex R st R well_orders X
proof
deffunc F(object) = {$1};
defpred P[object] means $1 is Ordinal;
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:112;
consider ON being set such that
A4: for x being object holds x in ON iff x in Class & P[x]
from XBOOLE_0:sch 1;
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 be object;
assume
A6: x in Y;
then x in A;
then reconsider B = x as Ordinal;
A7: B c= A by A6,ORDINAL1:def 2;
A in Class by A4,A5;
then B in Class by A2,A7;
hence thesis by A4;
end;
then reconsider ON as epsilon-transitive epsilon-connected set
by ORDINAL1:19;
A8: ON c= Class
by A4;
A9: ON,Class are_equipotent
proof
assume not thesis;
then ON in Class by A3,A8;
then ON in ON by A4;
hence contradiction;
end;
field RelIncl ON = ON by Def1;
then consider R such that
A10: R well_orders Class by A9,Lm1;
consider f such that
A11: dom f = X & for x being object st x in X holds f.x = F(x)
from FUNCT_1:sch 3;
A12: rng f c= Class
proof
let x be object;
assume x in rng f;
then consider y being object such that
A13: y in dom f and
A14: x = f.y by FUNCT_1:def 3;
A15: { y } c= X
by A11,A13,TARSKI:def 1;
f.y = { y } by A11,A13;
hence thesis by A1,A2,A14,A15;
end;
A16: X,rng f are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A17: x in dom f & y in dom f and
A18: f.x = f.y;
f.x = { x } & f.y = { y } by A11,A17;
hence thesis by A18,ZFMISC_1:3;
end;
thus thesis by A11;
end;
set Q = R|_2 Class;
field Q = Class by A10,Th10;
then
A19: field(Q|_2 rng f) = rng f by A10,A12,Th10,WELLORD1:31;
Q is well-ordering by A10,Th10;
hence thesis by A16,A19,Lm1,WELLORD1:25;
end;
reserve M for non empty set;
::$N 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 being object 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 Th11;
A4: R is_reflexive_in union M by A3;
A5: R is_connected_in union M by A3;
defpred Ch[object,object] means
ex D1 being set st D1 = $1 &
$2 in D1 & for z st z in D1 holds [$2,z] in R;
A6: R is_antisymmetric_in union M by A3;
A7: for x,y,z being object st x in M & Ch[x,y] & Ch[x,z] holds y = z
proof
let x,y,z be object such that
A8: x in M;
given X such that
A9: X = x and
A10: y in X and
A11: for u st u in X holds [y,u] in R;
A12: y in union M by A8,A10,TARSKI:def 4,A9;
given X such that
A13: X = x and
A14: z in X and
A15: for u st u in X holds [z,u] in R;
A16: z in union M by A8,A14,TARSKI:def 4,A13;
[y,z] in R & [z,y] in R by A10,A11,A14,A15,A9,A13;
hence thesis by A6,A12,A16;
end;
A17: R is_well_founded_in union M by A3;
A18: for x being object st x in M ex y being object st Ch[x,y]
proof
let x be object;
assume
A19: x in M;
reconsider xx=x as set by TARSKI:1;
A20: xx c= union M by ZFMISC_1:74,A19;
x <> {} by A1,A19;
then consider y being object such that
A21: y in xx and
A22: R-Seg(y) misses xx by A17,A20;
take y;
take xx;
thus xx = x;
thus y in xx by A21;
let z;
assume
A23: z in xx;
then
A24: not z in R-Seg(y) by A22,XBOOLE_0:3;
y <> z implies [y,z] in R or [z,y] in R by A5,A20,A21,A23;
hence thesis by A4,A20,A23,A24,WELLORD1:1;
end;
consider f such that
A25: dom f = M & for x being object st x in M holds Ch[x,f.x]
from FUNCT_1:sch 2(A7, A18 );
take Choice = rng f;
let X such that
A26: X in M;
take x = f.X;
thus Choice /\ X c= { x }
proof
let y be object;
assume
A27: y in Choice /\ X;
then
A28: y in X by XBOOLE_0:def 4;
y in Choice by A27,XBOOLE_0:def 4;
then consider z being object such that
A29: z in dom f and
A30: y = f.z by FUNCT_1:def 3;
reconsider z as set by TARSKI:1;
assume not y in { x };
then X <> z by A30,TARSKI:def 1;
then X misses z by A2,A25,A26,A29;
then
A31: X /\ z = {};
Ch[z,f.z] by A25,A29;
then f.z in z;
hence contradiction by A28,A30,A31,XBOOLE_0:def 4;
end;
let y be object;
assume y in { x };
then
A32: y = x by TARSKI:def 1;
Ch[X,f.X] by A25,A26;
then
A33: y in X by A32;
y in Choice by A25,A26,A32,FUNCT_1:def 3;
hence thesis by A33,XBOOLE_0:def 4;
end;
begin :: Addenda
theorem :: WAYBEL35:1, AK, 21.02.2006
for X being set holds RelIncl X is_reflexive_in X
by Def1;
theorem :: WAYBEL35:1, AK, 21.02.2006
for X being set holds RelIncl X is_transitive_in X
proof
let X be set;
RelIncl X is transitive & field RelIncl X = X by Def1;
hence thesis;
end;
theorem :: WAYBEL35:1, AK, 21.02.2006
for X being set holds RelIncl X is_antisymmetric_in X
proof
let X be set;
RelIncl X is antisymmetric & field RelIncl X = X by Def1;
hence thesis;
end;
:: from AMISTD_2, 2010.01.10, A.T
registration
cluster RelIncl {} -> empty;
coherence
proof
for Y,Z being set st Y in {} & Z in {} holds [Y,Z] in {} iff Y c= Z;
hence thesis by Def1,RELAT_1:40;
end;
end;
registration
let X be non empty set;
cluster RelIncl X -> non empty;
coherence
proof
set a = the Element of X;
[a,a] in RelIncl X by Def1;
hence thesis;
end;
end;
theorem
RelIncl {x} = {[x,x]}
proof
A1: for Y,Z being set st Y in {x} & Z in {x} holds [Y,Z] in {[x,x]} iff Y c= Z
proof
let Y,Z be set;
assume that
A2: Y in {x} and
A3: Z in {x};
A4: Y = x by A2,TARSKI:def 1;
hence [Y,Z] in {[x,x]} implies Y c= Z by A3,TARSKI:def 1;
Z = x by A3,TARSKI:def 1;
hence thesis by A4,TARSKI:def 1;
end;
field {[x,x]} = {x} by RELAT_1:173;
hence thesis by A1,Def1;
end;
theorem
RelIncl X c= [:X,X:]
proof
set R = RelIncl X;
let a,b be object;
assume
A1: [a,b] in R;
then b in field R by RELAT_1:15;
then
A2: b in X by Def1;
a in field R by A1,RELAT_1:15;
then a in X by Def1;
hence thesis by A2,ZFMISC_1:87;
end;