:: Tarski's Classes and Ranks
:: by Grzegorz Bancerek
::
:: Received March 23, 1990
:: 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 FUNCT_1, TARSKI, ZFMISC_1, SETFAM_1, XBOOLE_0, CARD_1, SUBSET_1,
ORDINAL1, ORDINAL2, RELAT_1, FUNCT_2, CLASSES1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, CARD_1, ORDINAL1, MCART_1, ORDINAL2;
constructors SETFAM_1, MCART_1, WELLORD2, ORDINAL2, CARD_1, FUNCT_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, RELSET_1,
RELAT_1;
requirements SUBSET, BOOLE;
definitions ORDINAL1, TARSKI, WELLORD2, FUNCT_1, XBOOLE_0, RELAT_1;
equalities ORDINAL1, TARSKI, RELAT_1;
expansions ORDINAL1, TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, SETFAM_1, ZFMISC_1, ORDINAL1, FUNCT_1, CARD_1, WELLORD2,
ENUMSET1, XBOOLE_0, XBOOLE_1, ORDINAL2, RELAT_1, FUNCT_2, XTUPLE_0;
schemes ORDINAL1, ORDINAL2, TARSKI, PARTFUN1, XBOOLE_0, FUNCT_1, XFAMILY;
begin
reserve W,X,Y,Z for set,
f,g for Function,
a,x,y,z for set;
definition
let B be set;
attr B is subset-closed means
:Def1:
for X,Y holds X in B & Y c= X implies Y in B;
end;
definition
let B be set;
attr B is Tarski means
B is subset-closed & (for X holds X in B implies bool X in B) &
for X holds X c= B implies X,B are_equipotent or X in B;
end;
definition
let A,B be set;
pred B is_Tarski-Class_of A means
A in B & B is Tarski;
irreflexivity;
end;
definition
let A be set;
func Tarski-Class A -> set means
:Def4:
it is_Tarski-Class_of A &
for D being set st D is_Tarski-Class_of A holds it c= D;
existence
proof
consider Big being set such that
A1: A in Big and
A2: for X,Y holds X in Big & Y c= X implies Y in Big and
A3: (
for X holds X in Big implies bool X in Big)& for X holds X c= Big implies X,
Big are_equipotent or X in Big
by ZFMISC_1:112;
A4: Big is Tarski by A3,A2,Def1;
defpred P[set] means $1 is_Tarski-Class_of A;
consider Classes being set such that
A5: X in Classes iff X in bool Big & P[X] from XFAMILY:sch 1;
set IT = meet Classes;
A6: Big
in bool Big & Big is_Tarski-Class_of A by A1,A4,ZFMISC_1:def 1;
then A7: Big in Classes by A5;
A8: Classes <> {} by A5,A6;
A9: now
let X;
assume X in Classes; then
X is_Tarski-Class_of A by A5;
hence A in X;
end;
then A10: A in IT by A8,SETFAM_1:def 1;
take IT;
thus A in IT by A8,A9,SETFAM_1:def 1;
thus
A11: X in IT & Y c= X implies Y in IT
proof
assume that
A12: X in IT and
A13: Y c= X;
now
let Z;
assume
A14: Z in Classes;
then Z is_Tarski-Class_of A by A5;
then Z is Tarski;
then A15: Z is subset-closed;
X in Z by A12,A14,SETFAM_1:def 1;
hence Y in Z by A13,A15;
end;
hence thesis by A8,SETFAM_1:def 1;
end;
thus
A16: X in IT implies bool X in IT
proof
assume
A17: X in IT;
now
let Z;
assume
A18: Z in Classes;
then Z is_Tarski-Class_of A by A5;
then A19: Z is Tarski;
X in Z by A17,A18,SETFAM_1:def 1;
hence bool X in Z by A19;
end;
hence thesis by A8,SETFAM_1:def 1;
end;
thus
A20: X c= IT implies X,IT are_equipotent or X in IT
proof
assume that
A21: X c= IT and
A22: not X,IT are_equipotent;
now
let Z;
assume
A23: Z in Classes;
then Z is_Tarski-Class_of A by A5;
then A24: Z is Tarski;
A25: IT c= Z by A23,SETFAM_1:3;
then X c= Z by A21;
then X,Z are_equipotent or X in Z by A24;
hence X in Z by A21,A22,A25,CARD_1:24;
end;
hence thesis by A8,SETFAM_1:def 1;
end;
let D be set;
assume
A26: D is_Tarski-Class_of A;
then A27: A in D;
A28: D is Tarski by A26;
then A29: D is subset-closed;
A30: IT /\ D is_Tarski-Class_of A
proof
thus A in IT /\ D by A10,A27,XBOOLE_0:def 4;
thus X in IT /\ D & Y c= X implies Y in IT /\ D
proof
assume that
A31: X in IT /\ D and
A32: Y c= X;
A33: X in IT by A31,XBOOLE_0:def 4;
A34: X in D by A31,XBOOLE_0:def 4;
A35: Y in IT by A11,A32,A33;
Y in D by A29,A32,A34;
hence thesis by A35,XBOOLE_0:def 4;
end;
thus X in IT /\ D implies bool X in IT /\ D
proof
assume
A36: X in IT /\ D;
then A37: X in IT by XBOOLE_0:def 4;
A38: X in D by A36,XBOOLE_0:def 4;
A39: bool X in IT by A16,A37;
bool X in D by A28,A38;
hence thesis by A39,XBOOLE_0:def 4;
end;
let X such that
A40: X c= IT /\ D and
A41: not X,IT /\ D are_equipotent;
A42: IT /\ D c= IT by XBOOLE_1:17;
A43: IT /\ D c= D by XBOOLE_1:17;
A44: not X,IT are_equipotent by A40,A41,A42,CARD_1:24;
A45: X c= D & not X,D are_equipotent by A40,A41,A43,CARD_1:24;
A46: X in IT by A20,A40,A42,A44,XBOOLE_1:1;
X in D by A28,A45;
hence thesis by A46,XBOOLE_0:def 4;
end;
IT /\ D c= Big
proof
let x be object;
assume x in IT /\ D;
then x in IT by XBOOLE_0:def 4;
hence thesis by A7,SETFAM_1:def 1;
end;
then A47: IT c= IT /\ D by SETFAM_1:3,A5,A30;
IT /\ D c= D by XBOOLE_1:17;
hence thesis by A47;
end;
uniqueness;
end;
registration
let A be set;
cluster Tarski-Class A -> non empty;
coherence
proof
Tarski-Class A is_Tarski-Class_of A by Def4;
hence thesis;
end;
end;
theorem
W is Tarski iff W is subset-closed & (for X st X in W holds bool X in W) &
for X st X c= W & card X in card W holds X in W
proof
hereby
assume
A1: W is Tarski;
hence
W is subset-closed & for X st X in W holds bool X in W;
let X;
assume that
A2: X c= W and
A3: card X in card W;
card X <> card W by A3;
then not X,W are_equipotent by CARD_1:5;
hence X in W by A1,A2;
end;
now
assume
A4: for X st X c= W & card X in card W holds X in W;
let X;
assume X c= W;
then card X c= card W & not card X in card W or X in W by A4,CARD_1:11;
hence X,W are_equipotent or X in W by CARD_1:3,5;
end;
hence thesis;
end;
theorem Th2:
X in Tarski-Class X
proof
Tarski-Class X is_Tarski-Class_of X by Def4;
hence thesis;
end;
theorem Th3:
Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X
proof
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski;
then Tarski-Class X is subset-closed;
hence thesis;
end;
theorem Th4:
Y in Tarski-Class X implies bool Y in Tarski-Class X
proof
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski;
hence thesis;
end;
theorem Th5:
Y c= Tarski-Class X implies
Y,Tarski-Class X are_equipotent or Y in Tarski-Class X
proof
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski;
hence thesis;
end;
theorem
Y c= Tarski-Class X & card Y in card Tarski-Class X implies
Y in Tarski-Class X
proof
assume that
A1: Y c= Tarski-Class X and
A2: card Y in card Tarski-Class X;
card Y <> card Tarski-Class X by A2;
hence thesis by A1,Th5,CARD_1:5;
end;
reserve u,v for Element of Tarski-Class(X),
A,B,C for Ordinal,
L for Sequence;
definition
let X,A;
func Tarski-Class(X,A) -> set means
:Def5:
ex L st it = last L & dom L = succ A & L.0 = { X } &
(for C st succ C in succ A holds
L.succ C = { u : ex v st v in L.C & u c= v } \/ { bool v : v in L.C } \/
bool(L.C) /\ Tarski-Class X) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = (union rng(L|C)) /\ Tarski-Class X;
correctness
proof
deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/
{ bool v : v in $2 } \/ bool $2 /\ Tarski-Class X;
deffunc D(Ordinal,Sequence) = (union rng $2) /\ Tarski-Class X;
(ex x being object,L st x = last L & dom L = succ A & L.0 = {X} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) & for x1,x2 being set st
(ex L st x1 = last L & dom L = succ A & L.0 = {X} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) &
(ex L st x2 = last L & dom L = succ A & L.0 = {X} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) )
holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
Lm1: now
let X;
deffunc F(Ordinal) = Tarski-Class(X,$1);
deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/
{ bool v : v in $2 } \/ bool $2 /\ Tarski-Class X;
deffunc D(Ordinal,Sequence) = (union rng $2) /\ Tarski-Class X;
A1: for A for x being object holds x = F(A) iff
ex L st x = last L & dom L = succ A & L.0 = { X } &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) by Def5;
thus F(0) = { X } from ORDINAL2:sch 8(A1);
thus for A holds F(succ A) = C(A,F(A)) from ORDINAL2:sch 9(A1);
thus A <> 0 & A is limit_ordinal & dom L = A &
(for B st B in A holds L.B = Tarski-Class(X,B)) implies
Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X
proof
assume that
A2: A <> 0 & A is limit_ordinal and
A3: dom L = A and
A4: for B st B in A holds L.B = F(B);
thus F(A) = D(A,L) from ORDINAL2:sch 10(A1,A2,A3,A4);
end;
end;
definition
let X,A;
redefine func Tarski-Class(X,A) -> Subset of Tarski-Class X; :: redefines Tarski-Class (CLASSES1, definition)
coherence
proof
defpred P[Ordinal] means Tarski-Class(X,$1) is Subset of Tarski-Class X;
{ X } c= Tarski-Class X
proof
let x be object;
assume x in { X };
then x = X by TARSKI:def 1;
hence thesis by Th2;
end;
then A1: P[0] by Lm1;
A2: P[B] implies P[succ B]
proof
assume Tarski-Class(X,B) is Subset of Tarski-Class X;
then reconsider S = Tarski-Class(X,B) as Subset of Tarski-Class X;
set Y = Tarski-Class(X,succ B);
Y c= Tarski-Class X
proof
let x be object;
assume x in Y;
then x in { u : ex v st v in S & u c= v } \/ { bool v : v in S } \/
bool S /\ Tarski-Class X by Lm1;
then
A3: x in { u : ex v st v in S & u c= v } \/ { bool v : v in S } or
x in bool S /\ Tarski-Class X by XBOOLE_0:def 3;
A4: now
assume x in { u : ex v st v in S & u c= v };
then ex u st x = u & ex v st v in S & u c= v;
hence thesis;
end;
now
assume x in { bool v : v in S };
then ex v st x = bool v & v in S;
hence thesis by Th4;
end;
hence thesis by A3,A4,XBOOLE_0:def 3,def 4;
end;
hence thesis;
end;
A5: for B st B <> 0 & B is limit_ordinal &
for C st C in B holds P[C] holds P[B]
proof
let B such that
A6: B <> 0 & B is limit_ordinal and
for C st C in B holds Tarski-Class(X,C) is Subset of Tarski-Class X;
deffunc f(Ordinal) = Tarski-Class(X,$1);
consider L such that
A7: dom L = B & for C st C in B holds L.C = f(C) from ORDINAL2:sch 2;
Tarski-Class(X,B) = (union rng L) /\ Tarski-Class X by A6,A7,Lm1;
hence thesis by XBOOLE_1:17;
end;
for A holds P[A] from ORDINAL2:sch 1(A1,A2,A5);
hence thesis;
end;
end;
theorem
Tarski-Class(X,{}) = { X } by Lm1;
theorem
Tarski-Class(X,succ A) = { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
theorem Th9:
A <> {} & A is limit_ordinal implies
Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
proof
assume
A1: A <> {} & A is limit_ordinal;
deffunc f(Ordinal) = Tarski-Class(X,$1);
consider L such that
A2: dom L = A & for B st B in A holds L.B = f(B) from ORDINAL2:sch 2;
A3: Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X by A1,A2,Lm1;
thus
Tarski-Class(X,A) c= { u : ex B st B in A & u in Tarski-Class(X,B) }
proof
let x be object;
assume x in Tarski-Class(X,A);
then x in union rng L by A3,XBOOLE_0:def 4;
then consider Y such that
A4: x in Y and
A5: Y in rng L by TARSKI:def 4;
consider y being object such that
A6: y in dom L and
A7: Y = L.y by A5,FUNCT_1:def 3;
reconsider y as Ordinal by A6;
Y = Tarski-Class(X,y) by A2,A6,A7;
hence thesis by A2,A4,A6;
end;
let x be object;
assume x in { u : ex B st B in A & u in Tarski-Class(X,B) };
then consider u such that
A8: x = u and
A9: ex B st B in A & u in Tarski-Class(X,B);
consider B such that
A10: B in A and
A11: u in Tarski-Class(X,B) by A9;
L.B = Tarski-Class(X,B) by A2,A10;
then Tarski-Class(X,B) in rng L by A2,A10,FUNCT_1:def 3;
then u in union rng L by A11,TARSKI:def 4;
hence thesis by A3,A8,XBOOLE_0:def 4;
end;
theorem Th10:
Y in Tarski-Class(X,succ A) iff
Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
proof
set T1 = { u : ex v st v in Tarski-Class(X,A) & u c= v };
set T2 = { bool v : v in Tarski-Class(X,A) };
set T3 = bool Tarski-Class(X,A) /\ Tarski-Class X;
A1: Tarski-Class(X,succ A) = T1 \/ T2 \/ T3 by Lm1;
thus Y in Tarski-Class(X,succ A) implies
Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
proof
assume Y in Tarski-Class(X,succ A);
then A2: Y in T1 \/ T2 or Y in T3 by A1,XBOOLE_0:def 3;
A3: now
assume Y in T1;
then ex u st Y = u & ex v st v in Tarski-Class(X,A) & u c= v;
hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
end;
now
assume Y in T2;
then ex v st Y = bool v & v in Tarski-Class(X,A);
hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
end;
hence thesis by A2,A3,XBOOLE_0:def 3,def 4;
end;
assume
A4: Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
A5: now
assume Y c= Tarski-Class(X,A) & Y in Tarski-Class X;
then Y in T3 by XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:def 3;
end;
now
given Z such that
A6: Z in Tarski-Class(X,A) and
A7: Y c= Z or Y = bool Z;
reconsider Z as Element of Tarski-Class X by A6;
reconsider y = Y as Element of Tarski-Class X by A6,A7,Th3,Th4;
A8: now
assume Y c= Z;
then y in T1 by A6;
then Y in T1 \/ T2 by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
now
assume Y = bool Z;
then y in T2 by A6;
then Y in T1 \/ T2 by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
hence thesis by A7,A8;
end;
hence thesis by A4,A5;
end;
theorem
Y c= Z & Z in Tarski-Class(X,A) implies Y in Tarski-Class(X,succ A) by Th10;
theorem
Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,succ A) by Th10;
theorem Th13:
A <> {} & A is limit_ordinal implies
(x in Tarski-Class(X,A) iff ex B st B in A & x in Tarski-Class(X,B))
proof
assume
A1: A <> {} & A is limit_ordinal;
then A2: Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
by Th9;
thus
x in Tarski-Class(X,A) implies ex B st B in A & x in Tarski-Class(X,B)
proof
assume x in Tarski-Class(X,A);
then ex u st x = u & ex B st B in A & u in Tarski-Class(X,B) by A2;
hence thesis;
end;
given B such that
A3: B in A and
A4: x in Tarski-Class(X,B);
reconsider u = x as Element of Tarski-Class X by A4;
u in { v : ex B st B in A & v in Tarski-Class(X,B) } by A3,A4;
hence thesis by A1,Th9;
end;
theorem
A <> {} & A is limit_ordinal & Y in Tarski-Class(X,A) &
(Z c= Y or Z = bool Y) implies Z in Tarski-Class(X,A)
proof
assume that
A1: A <> {} and
A2: A is limit_ordinal and
A3: Y in Tarski-Class(X,A);
consider B such that
A4: B in A and
A5: Y in Tarski-Class(X,B) by A1,A2,A3,Th13;
A6: bool Y in Tarski-Class(X,succ B) by A5,Th10;
A7: Z c= Y implies Z in Tarski-Class(X,succ B) by A5,Th10;
A8: succ B in A by A2,A4,ORDINAL1:28;
assume Z c= Y or Z = bool Y;
hence thesis by A2,A6,A7,A8,Th13;
end;
theorem Th15:
Tarski-Class(X,A) c= Tarski-Class(X,succ A)
proof
let x be object;
assume x in Tarski-Class(X,A);
then x in { u : ex v st v in Tarski-Class(X,A) & u c= v };
then A1: x in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 3;
Tarski-Class
(X,succ A) = { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th16:
A c= B implies Tarski-Class(X,A) c= Tarski-Class(X,B)
proof
defpred OnP[Ordinal] means
A c= $1 implies Tarski-Class(X,A) c= Tarski-Class(X,$1);
A1: for B st for C st C in B holds OnP[C] holds OnP[B]
proof
let B such that
A2: for C st C in B holds OnP[C] and
A3: A c= B;
let x be object;
assume
A4: x in Tarski-Class(X,A);
now
assume
A5: A <> B;
then A6: A in B by ORDINAL1:11,A3,XBOOLE_0:def 8;
A7: B <> {} by A3,A5;
A8: now
given C such that
A9: B = succ C;
A c= C & C in B by A6,A9,ORDINAL1:22;
then A10: Tarski-Class(X,A) c= Tarski-Class(X,C) by A2;
Tarski-Class(X,C) c= Tarski-Class(X,B) by A9,Th15;
then Tarski-Class(X,A) c= Tarski-Class(X,B) by A10;
hence thesis by A4;
end;
now
assume for C holds B <> succ C;
then Tarski-Class(X,B) = { v : ex C st C in B & v in Tarski-Class(X,C)
} by A7,Th9,ORDINAL1:29;
hence thesis by A4,A6;
end;
hence thesis by A8;
end;
hence thesis by A4;
end;
for B holds OnP[B] from ORDINAL1:sch 2(A1);
hence thesis;
end;
theorem Th17:
ex A st Tarski-Class(X,A) = Tarski-Class(X,succ A)
proof
assume
A1: for A holds Tarski-Class(X,A) <> Tarski-Class(X,succ A);
defpred P[object] means ex A st $1 in Tarski-Class(X,A);
consider Z such that
A2: for x being object holds x in Z iff x in Tarski-Class X & P[x]
from XBOOLE_0:sch 1;
defpred P[object,object] means
ex A st $2 = A & $1 in Tarski-Class(X,succ A) & not $1 in Tarski-Class(X,A);
A3: for x,y,z being object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
given A such that
A4: y = A and
A5: x in Tarski-Class(X,succ A) and
A6: not x in Tarski-Class(X,A);
given B such that
A7: z = B and
A8: x in Tarski-Class(X,succ B) and
A9: not x in Tarski-Class(X,B);
assume
A10: y <> z;
A c= B or B c= A;
then A11: A c< B or B c< A by A4,A7,A10;
now
assume A c< B;
then succ A c= B by ORDINAL1:11,21;
then Tarski-Class(X,succ A) c= Tarski-Class(X,B) by Th16;
hence contradiction by A5,A9;
end;
then succ B c= A by ORDINAL1:11,21,A11;
then Tarski-Class(X,succ B) c= Tarski-Class(X,A) by Th16;
hence contradiction by A6,A8;
end;
consider Y such that
A12: for x being object holds x in Y iff
ex y being object st y in Z & P[y,x] from TARSKI:sch 1(A3);
now
let A;
A13: Tarski-Class(X,A) c= Tarski-Class(X,succ A) by Th15;
consider x being object such that
A14: not (x in Tarski-Class(X,A) iff x in Tarski-Class(X,succ A)) by A1,
TARSKI:2;
x in Z by A2,A14;
hence A in Y by A12,A13,A14;
end;
hence contradiction by ORDINAL1:26;
end;
theorem Th18:
Tarski-Class(X,A) = Tarski-Class(X,succ A) implies
Tarski-Class(X,A) = Tarski-Class X
proof
assume
A1: Tarski-Class(X,A) = Tarski-Class(X,succ A);
{} c= A;
then A2: Tarski-Class(X,{}) c= Tarski-Class(X,A) by Th16;
A3: Tarski-Class(X,{}) = { X } & X in { X } by Lm1,TARSKI:def 1;
Tarski-Class(X,A) is_Tarski-Class_of X
proof
thus X in Tarski-Class(X,A) by A2,A3;
A4: Tarski-Class(X,succ A) = { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
Tarski-Class X is_Tarski-Class_of X by Def4;
then A5: Tarski-Class X is Tarski;
thus for Z,Y being set st
Z in Tarski-Class(X,A) & Y c= Z holds Y in Tarski-Class(X,A)
proof
let Z, Y be set;
assume
A6: Z in Tarski-Class(X,A) & Y c= Z;
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is Tarski;
then Tarski-Class X is subset-closed;
then reconsider y = Y as Element of Tarski-Class X by A6;
ex v st v in Tarski-Class(X,A) & y c= v by A6;
then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v };
then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 3;
hence thesis by A1,A4,XBOOLE_0:def 3;
end;
thus Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,A)
proof
assume Y in Tarski-Class(X,A);
then bool Y in { bool u : u in Tarski-Class(X,A) };
then bool Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 3;
hence thesis by A1,A4,XBOOLE_0:def 3;
end;
let Y;
assume that
A7: Y c= Tarski-Class(X,A) and
A8: not Y,Tarski-Class(X,A) are_equipotent;
Y c= Tarski-Class X by A7,XBOOLE_1:1;
then
Y,Tarski-Class X are_equipotent or Y in Tarski-Class X by A5;
hence thesis by A1,A7,A8,Th10,CARD_1:24;
end;
hence Tarski-Class(X,A) c= Tarski-Class X &
Tarski-Class X c= Tarski-Class(X,A) by Def4;
end;
theorem Th19:
ex A st Tarski-Class(X,A) = Tarski-Class X
proof
consider A such that
A1: Tarski-Class(X,A) = Tarski-Class(X,succ A) by Th17;
take A;
thus thesis by A1,Th18;
end;
theorem
ex A st Tarski-Class(X,A) = Tarski-Class X &
for B st B in A holds Tarski-Class(X,B) <> Tarski-Class X
proof
defpred P[Ordinal] means Tarski-Class(X,$1) = Tarski-Class X;
A1: ex A st P[A] by Th19;
consider A such that
A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A1);
take A;
thus Tarski-Class(X,A) = Tarski-Class X by A2;
let B;
assume B in A;
hence thesis by A2,ORDINAL1:5;
end;
theorem
Y <> X & Y in Tarski-Class X implies
ex A st not Y in Tarski-Class(X,A) & Y in Tarski-Class(X,succ A)
proof
assume that
A1: Y <> X and
A2: Y in Tarski-Class X;
defpred P[Ordinal] means Y in Tarski-Class(X,$1);
ex A st Tarski-Class(X,A) = Tarski-Class X by Th19;
then A3: ex A st P[A] by A2;
consider A such that
A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A3);
A5: not Y in { X } by A1,TARSKI:def 1;
A6: Tarski-Class(X,{}) = { X } by Lm1;
now
assume A is limit_ordinal;
then ex B st B in A & Y in Tarski-Class(X,B) by A4,A5,A6,Th13;
hence contradiction by A4,ORDINAL1:5;
end;
then consider B such that
A7: A = succ B by ORDINAL1:29;
take B;
not A c= B by A7,ORDINAL1:5,6;
hence thesis by A4,A7;
end;
theorem Th22:
X is epsilon-transitive implies
for A st A <> {} holds Tarski-Class(X,A) is epsilon-transitive
proof
assume
A1: Y in X implies Y c= X;
defpred OnP[Ordinal] means
$1 <> {} implies Tarski-Class(X,$1) is epsilon-transitive;
A2: for A st for B st B in A holds OnP[B] holds OnP[A]
proof
let A such that
A3: for B st B in A holds OnP[B] and
A4: A <> {};
let Y such that
A5: Y in Tarski-Class(X,A);
A6: now
given B such that
A7: A = succ B;
A8: B c= A by ORDINAL1:6,def 2,A7;
A9: OnP[B] by A3,A7,ORDINAL1:6;
A10: Tarski-Class(X,B) c= Tarski-Class(X,A) by A8,Th16;
now
assume not Y c= Tarski-Class(X,B);
then consider Z such that
A11: Z in Tarski-Class(X,B) and
A12: Y c= Z or Y = bool Z by A5,A7,Th10;
A13: Y = bool Z implies thesis by A7,A11,Th10;
now
assume
A14: Y c= Z;
thus thesis
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A15: x in Y;
then A16: x in Z by A14;
A17: now
assume B = {};
then Tarski-Class(X,B) = { X } by Lm1;
then Z = X by A11,TARSKI:def 1;
hence thesis by A7,A11,Th10,A1,A14,A15;
end;
now
assume B <> {};
then Z c= Tarski-Class(X,B) by A9,A11,ORDINAL1:def 2;
then x in Tarski-Class(X,B) by A16;
hence thesis by A10;
end;
hence thesis by A17;
end;
end;
hence thesis by A12,A13;
end;
hence thesis by A10;
end;
now
assume
A18: for B holds A <> succ B;
then A is limit_ordinal by ORDINAL1:29;
then consider B such that
A19: B in A and
A20: Y in Tarski-Class(X,B) by A4,A5,Th13;
A21: succ B <> A by A18;
A22: Tarski-Class(X,B) c= Tarski-Class(X,succ B) by Th15;
A23: succ B c< A by A19,ORDINAL1:21,A21;
A24: Tarski-Class(X,succ B) c= Tarski-Class(X,A) by A19,ORDINAL1:21,Th16;
Tarski-Class(X,succ B) is epsilon-transitive by A3,A23,ORDINAL1:11;
then Y c= Tarski-Class(X,succ B) by A20,A22;
hence thesis by A24;
end;
hence thesis by A6;
end;
thus for A holds OnP[A] from ORDINAL1:sch 2(A2);
end;
theorem Th23:
X is epsilon-transitive implies Tarski-Class X is epsilon-transitive
proof
consider A such that
A1: Tarski-Class(X,A) = Tarski-Class X by Th19;
Tarski-Class(X,A) c= Tarski-Class(X,succ A) by Th15;
then A2: Tarski-Class(X,A) = Tarski-Class(X,succ A) by A1;
assume X is epsilon-transitive;
hence thesis by A1,A2,Th22;
end;
theorem Th24:
Y in Tarski-Class X implies card Y in card Tarski-Class X
proof
assume
A1: Y in Tarski-Class X;
bool Y c= Tarski-Class X by A1,Th3;
then card
Y in card bool Y & card bool Y c= card Tarski-Class X by CARD_1:11,14;
hence thesis;
end;
theorem Th25:
Y in Tarski-Class X implies not Y,Tarski-Class X are_equipotent
proof
assume Y in Tarski-Class X;
then card Y in card Tarski-Class X by Th24;
then card Y <> card Tarski-Class X;
hence thesis by CARD_1:5;
end;
theorem Th26:
(x in Tarski-Class X implies {x} in Tarski-Class X) &
(x in Tarski-Class X & y in Tarski-Class X implies
{x,y} in Tarski-Class X)
proof
thus
Z1: now assume x in Tarski-Class X; then
bool x in Tarski-Class X by Th4;
hence {x} in Tarski-Class X by Th3,ZFMISC_1:68;
end;
assume that
A1: x in Tarski-Class X and
A2: y in Tarski-Class X;
A3: {x} in Tarski-Class X by Z1,A1;
bool {x} = {{},{x}} by ZFMISC_1:24;
then A4: not {{},{x}},Tarski-Class X are_equipotent by A3,Th4,Th25;
now
assume
A5: x <> y;
{{},{x}},{x,y} are_equipotent
proof
defpred C[object] means $1 = {};
deffunc f(object) = x;
deffunc g(object) = y;
consider f such that
A6: dom f = {{},{x}} & for z being object st z in {{},{x}} holds
(C[z] implies f.z = f(z)) & (not C[z] implies f.z = g(z))
from PARTFUN1:sch 1;
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A7: x1 in dom f and
A8: x2 in dom f;
A9: x2 = {} or x2 = {x} by A6,A8,TARSKI:def 2;
A10: x1 = {} implies f.x1 = x by A6,A7;
x1 <> {} implies f.x1 = y by A6,A7;
hence thesis by A5,A6,A7,A8,A9,A10,TARSKI:def 2;
end;
thus dom f = {{},{x}} by A6;
thus rng f c= {x,y}
proof
let z be object;
assume z in rng f; then
ex u being object st u in dom f & z = f.u by FUNCT_1:def 3; then
z = x or z = y by A6;
hence thesis by TARSKI:def 2;
end;
let z be object;
assume z in {x,y}; then
A11: z = x or z = y by TARSKI:def 2;
A12: {} in dom f by A6,TARSKI:def 2;
A13: {x} in dom f by A6,TARSKI:def 2;
A14: f.{} = x by A6,A12;
f.{x} = y by A6,A13;
hence thesis by A11,A12,A13,A14,FUNCT_1:def 3;
end;
then A15: not {x,y},Tarski-Class X are_equipotent by A4,WELLORD2:15;
{x,y} c= Tarski-Class X by A1,A2,ZFMISC_1:32;
hence thesis by A15,Th5;
end;
hence thesis by A3,ENUMSET1:29;
end;
theorem Th27:
x in Tarski-Class X & y in Tarski-Class X implies [x,y] in Tarski-Class X
proof
assume x in Tarski-Class X & y in Tarski-Class X;
then {x,y} in Tarski-Class X & {x} in Tarski-Class X by Th26;
hence thesis by Th26;
end;
theorem
Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X
proof
assume
A1: Y c= Tarski-Class X & Z c= Tarski-Class X;
let x,y be object;
assume [x,y] in [:Y,Z:];
then x in Y & y in Z by ZFMISC_1:87;
hence thesis by A1,Th27;
end;
definition
let A;
func Rank(A) -> set means
:Def6:
ex L st it = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = bool(L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = union rng(L|C);
correctness
proof
deffunc C(Ordinal,set) = bool $2;
deffunc D(Ordinal,Sequence) = union rng $2;
(ex x being object,L st x = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) & for x1,x2 being set st
(ex L st x1 = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) &
(ex L st x2 = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) )
holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
deffunc F(Ordinal) = Rank $1;
Lm2: now
deffunc C(Ordinal,set) = bool $2;
deffunc D(Ordinal,Sequence) = union rng $2;
A1: for A for x being object holds x = F(A) iff
ex L st x = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = C(C,L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) by Def6;
thus F(0) = {} from ORDINAL2:sch 8(A1);
thus for A holds F(succ A) = C(A,F(A)) from ORDINAL2:sch 9(A1);
thus A <> 0 & A is limit_ordinal & dom L = A &
(for B st B in A holds L.B = Rank B) implies Rank A = union rng L
proof
assume that
A2: A <> 0 & A is limit_ordinal and
A3: dom L = A and
A4: for B st B in A holds L.B = F(B);
thus F(A) = D(A,L) from ORDINAL2:sch 10(A1,A2,A3,A4);
end;
end;
theorem Th29:
Rank {} = {} by Lm2;
theorem
Rank succ A = bool Rank A by Lm2;
theorem Th31:
A is limit_ordinal implies
for x holds x in Rank A iff ex B st B in A & x in Rank B
proof
assume
A1: A is limit_ordinal;
let x;
consider L such that
A2: dom L = A & for B st B in A holds L.B = F(B) from ORDINAL2:sch 2;
thus x in Rank A implies ex B st B in A & x in Rank B
proof
assume
A3: x in Rank A;
then A is non empty by Th29;
then Rank A = union rng L by A1,A2,Lm2;
then consider Y such that
A4: x in Y and
A5: Y in rng L by A3,TARSKI:def 4;
consider y being object such that
A6: y in dom L and
A7: Y = L.y by A5,FUNCT_1:def 3;
reconsider y as Ordinal by A6;
take y;
thus thesis by A2,A4,A6,A7;
end;
given B such that
A8: B in A and
A9: x in Rank B;
A10: Rank A = union rng L by A1,A2,A8,Lm2;
L.B = Rank B by A2,A8;
then Rank B in rng L by A2,A8,FUNCT_1:def 3;
hence thesis by A9,A10,TARSKI:def 4;
end;
theorem Th32:
X c= Rank A iff X in Rank succ A
proof
thus X c= Rank A implies X in Rank succ A
proof
assume X c= Rank A;
then X in bool Rank A;
hence thesis by Lm2;
end;
assume X in Rank succ A;
then X in bool Rank A by Lm2;
hence thesis;
end;
registration
let A;
cluster Rank A -> epsilon-transitive;
coherence
proof
defpred P[Ordinal] means for X holds X in Rank $1 implies X c= Rank $1;
A1: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A2: for B st B in A holds P[B];
let X such that
A3: X in Rank A;
let x be object such that
A4: x in X;
reconsider xx=x as set by TARSKI:1;
A5: now
assume
A6: A is limit_ordinal;
then consider B such that
A7: B in A and
A8: X in Rank B by A3,Th31;
X c= Rank B by A2,A7,A8;
hence thesis by A4,A6,A7,Th31;
end;
now
assume not A is limit_ordinal;
then consider B such that
A9: A = succ B by ORDINAL1:29;
X c= Rank B by A3,A9,Th32; then
xx c= Rank B by A2,A4,A9,ORDINAL1:6;
hence thesis by A9,Th32;
end;
hence thesis by A5;
end;
for A holds P[A] from ORDINAL1:sch 2(A1);
hence P[A];
end;
end;
theorem
Rank A c= Rank succ A
proof
Rank A in bool Rank A by ZFMISC_1:def 1;
then Rank A in Rank succ A by Lm2;
hence thesis by ORDINAL1:def 2;
end;
theorem Th34:
union Rank A c= Rank A
proof
let x be object;
assume x in union Rank A;
then consider X such that
A1: x in X and
A2: X in Rank A by TARSKI:def 4;
X c= Rank A by A2,ORDINAL1:def 2;
hence thesis by A1;
end;
theorem
X in Rank A implies union X in Rank A
proof
assume
A1: X in Rank A;
A2: now
given B such that
A3: A = succ B;
A4: union X c= union Rank B by ZFMISC_1:77,A1,A3,Th32;
union Rank B c= Rank B by Th34;
hence thesis by A3,Th32,A4,XBOOLE_1:1;
end;
now
assume
A6: for B holds A <> succ B;
A7: A is limit_ordinal by A6,ORDINAL1:29;
then consider B such that
A8: B in A and
A9: X in Rank B by A1,Th31;
A10: union X c= union Rank B by ZFMISC_1:77,A9,ORDINAL1:def 2;
A11: union Rank B c= Rank B by Th34;
succ B <> A by A6;
then A12: succ B c< A by A8,ORDINAL1:21;
A13: union X in Rank succ B by A11,Th32,A10,XBOOLE_1:1;
succ B in A by A12,ORDINAL1:11;
hence thesis by A7,A13,Th31;
end;
hence thesis by A2;
end;
theorem Th36:
A in B iff Rank A in Rank B
proof
defpred OnP[Ordinal,Ordinal] means $1 in $2 implies Rank $1 in Rank $2;
A1: now
let A;
defpred P[Ordinal] means OnP[A,$1];
A2: for B st for C st C in B holds P[C] holds P[B]
proof
let B such that
A3: for C st C in B holds OnP[A,C] and
A4: A in B;
A5: now
given C such that
A6: B = succ C;
A7: A in C implies Rank A in Rank C by A3,A6,ORDINAL1:6;
now
assume
A8: not A in C;
A c= C & A <> C iff A c< C;
hence Rank A = Rank C by A4,A6,A8,ORDINAL1:11,22;
end;
then Rank A c= Rank C by A7,ORDINAL1:def 2;
hence thesis by A6,Th32;
end;
now
assume
A9: for C holds B <> succ C;
then A10: B is limit_ordinal by ORDINAL1:29;
A11: B <> succ A by A9;
succ A c< B by A11,A4,ORDINAL1:21;
then A12: succ A in B by ORDINAL1:11;
Rank A in Rank succ A by Th32;
hence thesis by A10,A12,Th31;
end;
hence thesis by A5;
end;
thus for B holds P[B] from ORDINAL1:sch 2(A2);
end;
hence OnP[A,B];
assume that
A13: Rank A in Rank B and
A14: not A in B;
B in A or B = A by A14,ORDINAL1:14;
hence contradiction by A1,A13;
end;
theorem Th37:
A c= B iff Rank A c= Rank B
proof
thus A c= B implies Rank A c= Rank B
proof
A1: A c< B iff A c= B & A <> B;
assume A c= B;
then Rank A = Rank B or Rank A in Rank B by Th36,A1,ORDINAL1:11;
hence thesis by ORDINAL1:def 2;
end;
assume that
A2: Rank A c= Rank B and
A3: not A c= B;
B in A by A3,ORDINAL1:16;
hence contradiction by A2,ORDINAL1:5,Th36;
end;
theorem Th38:
A c= Rank A
proof
defpred P[Ordinal] means $1 c= Rank $1;
A1: P[0] by XBOOLE_1:2;
A2: P[B] implies P[succ B]
proof
assume B c= Rank B;
then B in Rank succ B by Th32;
then
B c= Rank succ B & {B} c= Rank succ B by ORDINAL1:def 2,ZFMISC_1:31;
hence thesis by XBOOLE_1:8;
end;
A3: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof
let A such that
A <> 0 and
A4: A is limit_ordinal and
A5: for B st B in A holds B c= Rank B;
let x be object;
assume
A6: x in A;
then reconsider B = x as Ordinal;
A7: B c= Rank B by A5,A6;
A8: succ B c= A by A4,A6,ORDINAL1:28,def 2;
A9: B in Rank succ B by A7,Th32;
Rank succ B c= Rank A by A8,Th37;
hence thesis by A9;
end;
for B holds P[B] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis;
end;
theorem
for A,X st X in Rank A holds
not X,Rank A are_equipotent & card X in card Rank A
proof
defpred OnP[Ordinal] means
for X st X in Rank $1 holds not X,Rank $1 are_equipotent;
A1: for A st for B st B in A holds OnP[B] holds OnP[A]
proof
let A such that
A2: for B st B in A holds OnP[B];
let X;
assume
A3: X in Rank A;
A4: now
given B such that
A5: A = succ B;
A6: B c= A by A5,ORDINAL1:6,def 2;
A7: Rank succ B = bool Rank B by Lm2;
then A8: not Rank B,Rank A are_equipotent by A5,CARD_1:13;
Rank B c= Rank A by A6,Th37;
hence thesis by A3,A5,A7,A8,CARD_1:24;
end;
now
assume that
A10: for B holds A <> succ B;
A is limit_ordinal by A10,ORDINAL1:29;
then consider B such that
A11: B in A and
A12: X in Rank B by A3,Th31;
A13: (not X,Rank B are_equipotent) & X c= Rank B
by A2,A11,A12,ORDINAL1:def 2;
Rank B c= Rank A by A11,Th36,ORDINAL1:def 2;
hence thesis by A13,CARD_1:24;
end;
hence thesis by A4;
end;
A14: for A holds OnP[A] from ORDINAL1:sch 2(A1);
let A,X;
assume
A15: X in Rank A;
A16: card X c= card Rank A by A15,CARD_1:11,ORDINAL1:def 2;
card X <> card Rank A by A14,A15,CARD_1:5;
hence thesis by A14,A15,A16,CARD_1:3;
end;
theorem
X c= Rank A iff bool X c= Rank succ A
proof
thus X c= Rank A implies bool X c= Rank succ A
proof
assume
A1: X c= Rank A;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in bool X;
then A2: xx c= Rank A by A1;
Rank succ A = bool Rank A by Lm2;
hence thesis by A2;
end;
assume
A3: bool X c= Rank succ A;
let x be object;
assume x in X;
then { x } c= X by ZFMISC_1:31;
then A4: { x } in bool X;
Rank succ A = bool Rank A & x in { x } by Lm2,TARSKI:def 1;
hence thesis by A3,A4;
end;
theorem Th41:
X c= Y & Y in Rank A implies X in Rank A
proof
assume that
A1: X c= Y and
A2: Y in Rank A;
A3: now
given B such that
A4: A = succ B;
A5: Rank succ B = bool Rank B by Lm2;
then X c= Rank B by A1,A2,A4,XBOOLE_1:1;
hence thesis by A4,A5;
end;
now
assume
A6: for B holds A <> succ B;
then A7: A is limit_ordinal by ORDINAL1:29;
then consider B such that
A8: B in A and
A9: Y in Rank B by A2,Th31;
Y c= Rank B by A9,ORDINAL1:def 2;
then A10: X c= Rank B by A1;
A11: bool Rank B = Rank succ B by Lm2;
succ B in A by A6,A8,ORDINAL1:28,29;
hence thesis by A7,A10,A11,Th31;
end;
hence thesis by A3;
end;
theorem Th42:
X in Rank A iff bool X in Rank succ A
proof
thus X in Rank A implies bool X in Rank succ A
proof
assume
A1: X in Rank A;
bool X c= Rank A
by A1,Th41;
hence thesis by Th32;
end;
assume bool X in Rank succ A;
then X in bool X & bool X c= Rank A by Th32,ZFMISC_1:def 1;
hence thesis;
end;
theorem Th43:
x in Rank A iff {x} in Rank succ A
proof
x in Rank A iff {x} c= Rank A by ZFMISC_1:31;
hence thesis by Th32;
end;
theorem Th44:
x in Rank A & y in Rank A iff {x,y} in Rank succ A
proof
x in Rank A & y in Rank A iff {x,y} c= Rank A by ZFMISC_1:32;
hence thesis by Th32;
end;
theorem
x in Rank A & y in Rank A iff [x,y] in Rank succ succ A
proof
A1: x in Rank A iff {x} in Rank succ A by Th43;
x in Rank A & y in Rank A iff {x,y} in Rank succ A by Th44;
hence thesis by A1,Th44;
end;
theorem Th46:
X is epsilon-transitive &
Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X implies
Tarski-Class X c= Rank A
proof
assume that
A1: X is epsilon-transitive and
A2: Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X;
given x being object such that
A3: x in Tarski-Class X & not x in Rank A;
x in (Tarski-Class X) \ Rank A by A3,XBOOLE_0:def 5;
then consider Y such that
A4: Y in (Tarski-Class X) \ Rank A and
A5: not ex x be object st x in (Tarski-Class X) \ Rank A & x in Y by TARSKI:3;
A6: Y c= Tarski-Class X by A4,ORDINAL1:def 2,A1,Th23;
Y c= Rank A
proof
let x be object;
assume
A7: x in Y;
then not x in (Tarski-Class X) \ Rank A by A5;
hence thesis by A6,A7,XBOOLE_0:def 5;
end;
then Y in Rank succ A by Th32;
then A8: Y in Rank succ A /\ Tarski-Class X by A4,XBOOLE_0:def 4;
not Y in Rank A by A4,XBOOLE_0:def 5;
hence contradiction by A2,A8,XBOOLE_0:def 4;
end;
theorem Th47:
X is epsilon-transitive implies ex A st Tarski-Class X c= Rank A
proof
assume
A1: X is epsilon-transitive;
assume
A2: not Tarski-Class X c= Rank A;
defpred P[object] means ex A st $1 in Rank A;
consider Power being set such that
A3: for x being object holds x in Power iff x in Tarski-Class X & P[x]
from XBOOLE_0:sch 1;
defpred P[object,object] means
ex A st $2 = A & not $1 in Rank A & $1 in Rank succ A;
A4: for x,y,z being object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
given A1 being Ordinal such that
A5: y = A1 and
A6: not x in Rank A1 and
A7: x in Rank succ A1;
given A2 being Ordinal such that
A8: z = A2 and
A9: not x in Rank A2 and
A10: x in Rank succ A2;
assume y <> z;
then
A11: A1 in A2 or A2 in A1 by A5,A8,ORDINAL1:14;
now
assume succ A1 c= A2;
then Rank succ A1 c= Rank A2 by Th37;
hence contradiction by A7,A9;
end;
then Rank succ A2 c= Rank A1 by A11,Th37,ORDINAL1:21;
hence contradiction by A6,A10;
end;
consider Y such that
A12: for x being object holds x in Y iff
ex y being object st y in Power & P[y,x] from TARSKI:sch 1(A4);
now
let A;
Rank A /\ Tarski-Class X <> Rank succ A /\ Tarski-Class X by A1,A2,Th46;
then consider y being object such that
A13: not
(y in Rank A /\ Tarski-Class X iff y in Rank succ A /\ Tarski-Class X)
by TARSKI:2;
A14: A c= succ A by ORDINAL1:6,def 2;
then
A15: Rank A c= Rank succ A by Th37;
Rank A /\ Tarski-Class X c= Rank succ A /\ Tarski-Class X
by XBOOLE_1:26,A14,Th37;
then A16: y in Rank succ A by A13,XBOOLE_0:def 4;
A17: y in Tarski-Class X by A13,XBOOLE_0:def 4;
then
A18: not y in Rank A by A13,A15,XBOOLE_0:def 4;
y in Power by A3,A16,A17;
hence A in Y by A12,A16,A18;
end;
hence contradiction by ORDINAL1:26;
end;
theorem Th48:
X is epsilon-transitive implies union X c= X
proof
assume
A1: Y in X implies Y c= X;
let x be object;
assume x in union X;
then consider Y such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
Y c= X by A1,A3;
hence thesis by A2;
end;
theorem Th49:
X is epsilon-transitive & Y is epsilon-transitive implies
X \/ Y is epsilon-transitive
proof
assume that
A1: ( Z in X implies Z c= X) and
A2: ( Z in Y implies Z c= Y);
let Z;
assume Z in X \/ Y;
then Z in X or Z in Y by XBOOLE_0:def 3;
then A3: Z c= X or Z c= Y by A1,A2;
X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
hence thesis by A3;
end;
theorem
X is epsilon-transitive & Y is epsilon-transitive implies
X /\ Y is epsilon-transitive
proof
assume that
A1: Z in X implies Z c= X and
A2: Z in Y implies Z c= Y;
let Z;
assume
A3: Z in X /\ Y;
then A4: Z in X by XBOOLE_0:def 4;
A5: Z in Y by A3,XBOOLE_0:def 4;
A6: Z c= X by A1,A4;
Z c= Y by A2,A5;
hence thesis by A6,XBOOLE_1:19;
end;
reserve n for Element of omega;
deffunc f(set,set) = union $2;
definition
let X;
func the_transitive-closure_of X -> set means
:Def7:
for x being object
holds x in it iff ex f,n st x in f.n & dom f = omega & f.0 = X &
for k being Nat holds f.(succ k) = union(f.k);
existence
proof
consider f such that
A1: dom f = omega & f.0 = X &
for n being Nat holds f.(succ n) = f(n,f.n)
from ORDINAL2:sch 18;
take UNI = union rng f;
let x be object;
thus x in UNI implies ex f,n st x in f.n & dom f = omega & f.0 = X &
for k being Nat holds f.(succ k) = union(f.k)
proof
assume x in UNI;
then consider Y such that
A2: x in Y and
A3: Y in rng f by TARSKI:def 4;
consider y being object such that
A4: y in dom f and
A5: Y = f.y by A3,FUNCT_1:def 3;
reconsider y as Element of omega by A1,A4;
take f,y;
thus thesis by A1,A2,A5;
end;
deffunc f(set,set) = union $2;
given g,n such that
A6: x in g.n and
A7: dom g = omega and
A8: g.0 = X and
A9: for k being Nat holds g.(succ k) = f(k,g.k);
A10: dom f = omega by A1;
A11: f.0 = X by A1;
A12: for n being Nat holds f.(succ n) = f(n,f.n) by A1;
g = f from ORDINAL2:sch 20(A7,A8,A9,A10,A11,A12);
then g.n in rng f by A1,FUNCT_1:def 3;
hence thesis by A6,TARSKI:def 4;
end;
uniqueness
proof
defpred P[object] means ex f,n st $1 in f.n & dom f = omega & f.0 = X &
for k being Nat holds f.(succ k) = union(f.k);
let U1,U2 be set such that
A13: for x being object holds x in U1 iff P[x] and
A14: for x being object holds x in U2 iff P[x];
thus U1 = U2 from XBOOLE_0:sch 2(A13,A14);
end;
end;
registration let X;
cluster the_transitive-closure_of X -> epsilon-transitive;
coherence
proof
let Y;
assume Y in the_transitive-closure_of X;
then consider f,n such that
A1: Y in f.n and
A2: dom f = omega & f.0 = X and
A3: for k being Nat holds f.(succ k) = union(f.k) by Def7;
let x be object;
assume x in Y;
then A4: x in union(f.n) by A1,TARSKI:def 4;
reconsider m = succ n as Element of omega by ORDINAL1:def 12;
x in f.m by A3,A4;
hence x in the_transitive-closure_of X by A2,A3,Def7;
end;
end;
theorem
the_transitive-closure_of X is epsilon-transitive;
theorem Th52:
X c= the_transitive-closure_of X
proof
let x be object such that
A1: x in X;
consider f such that
A2: dom f = omega and
A3: f.0 = X and
A4: for n being Nat holds f.(succ n) = f(n,f.n)
from ORDINAL2:sch 18;
reconsider z = 0 as Element of omega by ORDINAL1:def 12;
x in f.z by A1,A3;
hence x in the_transitive-closure_of X by A2,A3,A4,Def7;
end;
theorem Th53:
X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y
proof
assume that
A1: X c= Y and
A2: Y is epsilon-transitive;
let x be object;
assume x in the_transitive-closure_of X;
then consider f,n such that
A3: x in f.n and dom f = omega and
A4: f.0 = X and
A5: for k being Nat holds f.(succ k) = union(f.k) by Def7;
defpred P[Nat] means f.$1 c= Y;
A6: P[0] by A1,A4;
A7: for k being Nat st P[k] holds P[succ k]
proof
let k be Nat;
assume f.k c= Y;
then A8: union (f.k) c= union Y by ZFMISC_1:77;
f.(succ k) = union (f.k) & union Y c= Y by A2,A5,Th48;
hence thesis by A8,XBOOLE_1:1;
end;
P[n] from ORDINAL2:sch 17(A6,A7);
hence thesis by A3;
end;
theorem Th54:
(for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y &
Y is epsilon-transitive implies the_transitive-closure_of X = Y
by Th53,Th52;
theorem Th55:
X is epsilon-transitive implies the_transitive-closure_of X = X
proof
for Z st X c= Z & Z is epsilon-transitive holds X c= Z;
hence thesis by Th54;
end;
theorem
the_transitive-closure_of {} = {} by Th55;
theorem
the_transitive-closure_of A = A by Th55;
theorem Th58:
X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y
proof
assume
A1: X c= Y;
Y c= the_transitive-closure_of Y by Th52;
then X c= the_transitive-closure_of Y by A1;
hence thesis by Th53;
end;
theorem
the_transitive-closure_of the_transitive-closure_of X =
the_transitive-closure_of X by Th55;
theorem
the_transitive-closure_of (X \/ Y) =
the_transitive-closure_of X \/ the_transitive-closure_of Y
proof
X
c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y by Th52;
then
A1: X \/ Y c= the_transitive-closure_of X \/ the_transitive-closure_of Y by
XBOOLE_1:13;
the_transitive-closure_of (X \/ Y) c= the_transitive-closure_of (
the_transitive-closure_of X \/ the_transitive-closure_of Y) by A1,Th58;
hence the_transitive-closure_of (X \/ Y) c=
the_transitive-closure_of X \/ the_transitive-closure_of Y by Th49,Th55;
the_transitive-closure_of X c= the_transitive-closure_of (X \/ Y) &
the_transitive-closure_of Y c= the_transitive-closure_of (X \/ Y) by Th58,
XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem
the_transitive-closure_of (X /\ Y) c=
the_transitive-closure_of X /\ the_transitive-closure_of Y
proof
the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of X &
the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of Y by Th58,
XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
theorem Th62:
ex A st X c= Rank A
proof
consider A such that
A1: Tarski-Class the_transitive-closure_of X c= Rank A by Th47;
take A;
the_transitive-closure_of X in Tarski-Class the_transitive-closure_of X
by Th2;
then X in Tarski-Class the_transitive-closure_of X by Th3,Th52;
hence thesis by A1,ORDINAL1:def 2;
end;
definition
let x be object;
func the_rank_of x -> Ordinal means
:Def8:
x in Rank succ it & for B st x in Rank succ B holds it c= B;
existence
proof
defpred P[Ordinal] means x in Rank succ $1;
reconsider x as set by TARSKI:1;
consider A such that
A1: x c= Rank A by Th62;
x in bool Rank A by A1;
then x in Rank succ A by Lm2;
then
A2: ex A st P[A];
thus ex A st P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A2);
end;
uniqueness;
end;
definition
let X;
redefine func the_rank_of X means :: redefines the_rank_of (CLASSES1, definition)
:Def9:
X c= Rank it & for B st X c= Rank B holds it c= B;
compatibility
proof let O be Ordinal;
thus O = the_rank_of X implies
X c= Rank O & for B st X c= Rank B holds O c= B
proof assume
A1: O = the_rank_of X;
then X in Rank succ O by Def8;
then X in bool Rank O by Lm2;
hence X c= Rank O;
let B;
assume X c= Rank B;
then X in bool Rank B;
then X in Rank succ B by Lm2;
hence O c= B by A1,Def8;
end;
assume X c= Rank O;
then X in bool Rank O;
then
A2: X in Rank succ O by Lm2;
assume
A3: for B st X c= Rank B holds O c= B;
for B st X in Rank succ B holds O c= B
proof let B;
assume X in Rank succ B;
then X in bool Rank B by Lm2;
hence O c= B by A3;
end;
hence O = the_rank_of X by A2,Def8;
end;
end;
theorem Th63:
the_rank_of bool X = succ the_rank_of X
proof
A1: X c= Rank the_rank_of X by Def9;
A2: bool X c= Rank succ the_rank_of X
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in bool X;
then A3: xx c= Rank the_rank_of X by A1;
bool Rank the_rank_of X = Rank succ the_rank_of X by Lm2;
hence thesis by A3;
end;
for A st bool X c= Rank A holds succ the_rank_of X c= A
proof
let A such that
A4: bool X c= Rank A;
defpred P[Ordinal] means X in Rank $1;
A5: X in bool X by ZFMISC_1:def 1;
then A6: ex A st P[A] by A4;
consider B such that
A7: P[B] & for C st P[C] holds B c= C from ORDINAL1:sch 1(A6);
now
assume for C holds B <> succ C;
then B is limit_ordinal by ORDINAL1:29;
then ex C st C in B & X in Rank C by A7,Th31;
hence contradiction by A7,ORDINAL1:5;
end;
then consider C such that
A8: B = succ C;
X c= Rank C by A7,A8,Th32;
then the_rank_of X c= C by Def9;
then A9: the_rank_of X in B by A8,ORDINAL1:22;
B c= A by A4,A5,A7;
hence thesis by A9,ORDINAL1:21;
end;
hence thesis by A2,Def9;
end;
theorem
the_rank_of Rank A = A
proof
for B st Rank A c= Rank B holds A c= B by Th37;
hence thesis by Def9;
end;
theorem Th65:
X c= Rank A iff the_rank_of X c= A
proof
thus X c= Rank A implies the_rank_of X c= A by Def9;
assume the_rank_of X c= A;
then A1: Rank the_rank_of X c= Rank A by Th37;
X c= Rank the_rank_of X by Def9;
hence thesis by A1;
end;
theorem Th66:
X in Rank A iff the_rank_of X in A
proof
thus X in Rank A implies the_rank_of X in A
proof
assume X in Rank A;
then bool X in Rank succ A by Th42;
then A1: bool X c= Rank A by Th32;
the_rank_of bool X = succ the_rank_of X by Th63;
then A2: the_rank_of X in the_rank_of bool X by ORDINAL1:6;
the_rank_of bool X c= A by A1,Def9;
hence thesis by A2;
end;
assume
A3: the_rank_of X in A;
X c= Rank the_rank_of X by Def9;
then A4: X in Rank succ the_rank_of X by Th32;
Rank succ the_rank_of X c= Rank A by A3,Th37,ORDINAL1:21;
hence thesis by A4;
end;
theorem
X c= Y implies the_rank_of X c= the_rank_of Y
proof
assume
A1: X c= Y;
Y c= Rank the_rank_of Y by Def9;
then X c= Rank the_rank_of Y by A1;
hence thesis by Def9;
end;
theorem Th68:
X in Y implies the_rank_of X in the_rank_of Y
proof
assume
A1: X in Y;
Y c= Rank the_rank_of Y by Def9;
hence thesis by A1,Th66;
end;
theorem Th69:
the_rank_of X c= A iff for Y st Y in X holds the_rank_of Y in A
proof
set R = the_rank_of X;
A1: X c= Rank R by Def9;
thus
the_rank_of X c= A implies for Y st Y in X holds the_rank_of Y in A
by A1,Th66;
assume
A2: for Y st Y in X holds the_rank_of Y in A;
X c= Rank A
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in X;
then the_rank_of xx in A by A2;
hence thesis by Th66;
end;
hence thesis by Def9;
end;
theorem Th70:
A c= the_rank_of X iff for B st B in A ex Y st Y in X & B c= the_rank_of Y
proof
thus A c= the_rank_of X implies
for B st B in A ex Y st Y in X & B c= the_rank_of Y
proof
assume
A1: A c= the_rank_of X;
let B;
assume B in A;
then not the_rank_of X c= B by A1,ORDINAL1:5;
then not X c= Rank B by Def9;
then A2: X \ Rank B <> {} by XBOOLE_1:37;
set x = the Element of X \ Rank B;
take x;
A3: not x in Rank B by A2,XBOOLE_0:def 5;
thus x in X by A2,XBOOLE_0:def 5;
thus thesis by ORDINAL1:16,A3,Th66;
end;
assume
A4: for B st B in A ex Y st Y in X & B c= the_rank_of Y;
let x be object;
assume
A5: x in A;
then reconsider x as Ordinal;
consider Y such that
A6: Y in X and
A7: x c= the_rank_of Y by A4,A5;
the_rank_of Y in the_rank_of X by A6,Th68;
hence thesis by A7,ORDINAL1:12;
end;
theorem
the_rank_of X = {} iff X = {}
proof
thus the_rank_of X = {} implies X = {}
proof
assume the_rank_of X = {};
then X c= Rank {} by Def9;
hence thesis by Lm2;
end;
assume X = {};
then for Y st Y in X holds the_rank_of Y in {};
hence the_rank_of X c= {} by Th69;
thus {} c= the_rank_of X;
end;
theorem Th72:
the_rank_of X = succ A implies ex Y st Y in X & the_rank_of Y = A
proof
assume
A1: the_rank_of X = succ A;
consider Y such that
A2: Y in X and
A3: A c= the_rank_of Y by A1,Th70,ORDINAL1:6;
take Y;
the_rank_of Y c= A by A1,ORDINAL1:22,A2,Th68;
hence thesis by A2,A3;
end;
theorem
the_rank_of A = A
proof
A c= Rank A by Th38;
hence the_rank_of A c= A by Th65;
defpred P[Ordinal] means $1 c= the_rank_of $1;
A1: for A st for B st B in A holds P[B] holds P[A]
proof
let A such that
A2: for B st B in A holds B c= the_rank_of B;
now
let B such that
A3: B in A;
reconsider Y = B as set;
take Y;
thus Y in A & B c= the_rank_of Y by A2,A3;
end;
hence thesis by Th70;
end;
P[B] from ORDINAL1:sch 2(A1);
hence thesis;
end;
theorem
the_rank_of Tarski-Class X <> {} &
the_rank_of Tarski-Class X is limit_ordinal
proof
A1: Tarski-Class X c= Rank the_rank_of Tarski-Class X by Def9;
thus the_rank_of Tarski-Class X <> {}
proof
assume the_rank_of Tarski-Class X = {};
then Tarski-Class X c= {} by Def9,Lm2;
hence contradiction;
end;
assume not thesis;
then consider A such that
A2: the_rank_of Tarski-Class X = succ A by ORDINAL1:29;
consider Y such that
A3: Y in Tarski-Class X and
A4: the_rank_of Y = A by A2,Th72;
A5: bool Y in Tarski-Class X by A3,Th4;
A6: the_rank_of bool Y = succ A by A4,Th63;
bool Y c= Rank A by A1,A2,A5,Th32;
then succ A c= A by A6,Def9;
then A in A by ORDINAL1:21;
hence contradiction;
end;
begin :: Addenda
:: from ZFREFLE1, 2007.03, A.T.
reserve e,u for set;
scheme NonUniqFuncEx { X() -> set, P[object,object] }:
ex f being Function st dom f = X() &
for e being object st e in X() holds P[e,f.e]
provided
A1: for e being object st e in X() ex u being object st P[e,u]
proof
per cases;
suppose
X() = {};
then A2: for e being object st e in X()
ex u being object st u in {} & P[e,u];
ex f being Function st dom f = X() & rng f c= {} &
for e being object st e in X() holds P[e,f.e] from FUNCT_1:sch 6(A2);
hence thesis;
end;
suppose
X() <> {};
then reconsider D = X() as non empty set;
defpred Q[set,Ordinal] means ex u st u in Rank $2 & P[$1,u];
A3: for e being Element of D ex A st Q[e,A]
proof
let e be Element of D;
consider u being object such that
A4: P[e,u] by A1;
reconsider u as set by TARSKI:1;
u c= Rank the_rank_of u by Def9;
then u in Rank succ the_rank_of u by Th32;
hence thesis by A4;
end;
consider F be Function such that
A5: dom F = D & for d being Element of D ex A st A = F.d & Q[d,A] &
for B st Q[d,B] holds A c= B from ORDINAL1:sch 6(A3);
A6: for e being object st e in X()
ex u being object st u in Rank sup rng F & P[e,u]
proof
let e be object;
assume
A7: e in X();
then consider A such that
A8: A = F.e and
A9: ex u st u in Rank A & P[e,u]
and for B st ex u st u in Rank B & P[e,u] holds A c= B by A5;
consider u such that
A10: u in Rank A & P[e,u] by A9;
take u;
A in rng F by A5,A7,A8,FUNCT_1:def 3;
then A in sup rng F by ORDINAL2:19;
then Rank A c= Rank sup rng F by Th37,ORDINAL1:def 2;
hence thesis by A10;
end;
ex f being Function st dom f = X() & rng f c= Rank sup rng F &
for e being object st e in X() holds P[e, f.e] from FUNCT_1:sch 6(A6);
hence thesis;
end;
end;
:: from RFINSEQ, 2008.10.10, A.T.
definition
let F,G be Relation;
pred F,G are_fiberwise_equipotent means
for x be object holds card Coim(F,x) = card Coim(G,x);
reflexivity;
symmetry;
end;
Lm3: for F be Function, x be object st not x in rng F holds Coim(F,x) = {}
proof
let F be Function, x be object;
assume
A1: not x in rng F;
now
assume rng F meets {x};
then ex y being object st y in rng F & y in {x} by XBOOLE_0:3;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis by RELAT_1:138;
end;
theorem Th75:
for F,G be Function st F,G are_fiberwise_equipotent holds rng F = rng G
proof
let F,G be Function;
assume
A1: F,G are_fiberwise_equipotent;
thus rng F c= rng G
proof
let x be object;
assume that
A2: x in rng F and
A3: not x in rng G;
A4: card Coim(F,x) = card Coim(G,x) by A1;
A5: ex y being object st y in dom F & F.y = x by A2,FUNCT_1:def 3;
Coim(G,x) = {} by A3,Lm3;
then x in {x} & F"{x} = {} by A4,CARD_1:5,26,TARSKI:def 1;
hence contradiction by A5,FUNCT_1:def 7;
end;
let x be object;
assume that
A6: x in rng G and
A7: not x in rng F;
A8: card Coim(G,x) = card Coim(F,x) by A1;
A9: ex y being object st y in dom G & G.y = x by A6,FUNCT_1:def 3;
Coim(F,x) = {} by A7,Lm3;
then x in {x} & Coim(G,x) = {} by A8,CARD_1:5,26,TARSKI:def 1;
hence contradiction by A9,FUNCT_1:def 7;
end;
theorem
for F,G,H be Function
st F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent holds
G,H are_fiberwise_equipotent
proof
let F,G,H be Function;
assume that
A1: F,G are_fiberwise_equipotent and
A2: F,H are_fiberwise_equipotent;
let x be object;
thus card Coim(G,x) = card Coim(F,x) by A1
.= card Coim(H,x) by A2;
end;
theorem Th77:
for F,G be Function holds F,G are_fiberwise_equipotent iff
ex H be Function st dom H = dom F & rng H = dom G & H is one-to-one & F = G*H
proof
let F,G be Function;
thus F,G are_fiberwise_equipotent implies
ex H be Function st dom H = dom F & rng H = dom G & H is one-to-one & F = G*H
proof
assume
A1: F,G are_fiberwise_equipotent;
defpred P[object,object] means $2 is Function &
for f be Function st $2 = f holds dom f = F"{$1} & rng f = G"{$1} &
f is one-to-one;
A2: for x being object st x in rng F ex y being object st P[x,y]
proof
let x be object;
assume x in rng F;
card Coim(F,x) = card Coim(G,x) by A1;
then consider H be Function such that
A3: H is one-to-one & dom H = F"{x} & rng H = G"{x}
by WELLORD2:def 4, CARD_1:5;
take H;
thus H is Function;
let g be Function;
assume g = H;
hence thesis by A3;
end;
consider W be Function such that
A4: dom W = rng F & for x being object st x in rng F holds P[x,W.x]
from NonUniqFuncEx(A2);
defpred Q[object,object] means
for H be Function st H = W.(F.$1) holds $2 = H.$1;
set df = dom F, dg = dom G;
A5: for x being object st x in df ex y being object st y in dg & Q[x,y]
proof
let x be object;
assume
A6: x in df;
then A7: F.x in rng F by FUNCT_1:def 3;
then reconsider f = W.(F.x) as Function by A4;
A8: dom f = F"{F.x} & rng f = G"{F.x} by A4,A7;
take y = f.x;
F.x in {F.x} by TARSKI:def 1;
then x in F"{F.x} by A6,FUNCT_1:def 7;
then f.x in G"{F.x} by A8,FUNCT_1:def 3;
hence y in dg by FUNCT_1:def 7;
let g be Function;
assume g = W.(F.x);
hence thesis;
end;
consider IT be Function such that
A9: dom IT = df & rng IT c= dg &
for x being object st x in df holds Q[x,IT.x] from FUNCT_1:sch 6(A5);
take IT;
thus dom IT = df by A9;
dom G c= rng IT
proof
let x be object;
assume
A10: x in dg;
then A11: G.x in rng G by FUNCT_1:def 3;
A12: rng F = rng G by A1,Th75;
then reconsider f = W.(G.x) as Function by A4,A11;
A13: dom f = F"{G.x} by A4,A11,A12;
A14: rng f = G"{G.x} by A4,A11,A12;
G.x in {G.x} by TARSKI:def 1;
then x in rng f by A10,A14,FUNCT_1:def 7;
then consider z be object such that
A15: z in dom f and
A16: f.z = x by FUNCT_1:def 3;
A17: z in df by A13,A15,FUNCT_1:def 7;
F.z in {G.x} by A13,A15,FUNCT_1:def 7;
then F.z = G.x by TARSKI:def 1;
then IT.z = x by A9,A16,A17;
hence thesis by A9,A17,FUNCT_1:def 3;
end;
hence rng IT = dg by A9;
now
let x,y be object;
assume that
A18: x in dom IT and
A19: y in dom IT and
A20: IT.x = IT.y;
A21: F.x in rng F by A9,A18,FUNCT_1:def 3;
A22: F.y in rng F by A9,A19,FUNCT_1:def 3;
then reconsider f1 = W.(F.x), f2 = W.(F.y) as Function by A4,A21;
A23: IT.x = f1.x & IT.y = f2.y by A9,A18,A19;
A24: dom f1 = F"{F.x} by A4,A21;
A25: rng f1 = G"{F.x} by A4,A21;
A26: f1 is one-to-one by A4,A21;
A27: dom f2 = F"{F.y} by A4,A22;
A28: rng f2 = G"{F.y} by A4,A22;
A29: F.x in {F.x} by TARSKI:def 1;
A30: F.y in {F.y} by TARSKI:def 1;
A31: x in F"{F.x} by A9,A18,A29,FUNCT_1:def 7;
A32: y in F"{F.y} by A9,A19,A30,FUNCT_1:def 7;
A33: f1.x in rng f1 by A24,A31,FUNCT_1:def 3;
f2.y in rng f2 by A27,A32,FUNCT_1:def 3;
then
f1.x in G"{F.x} /\ G"{F.y} by A20,A23,A25,A28,A33,XBOOLE_0:def 4;
then f1.x in G"({F.x} /\ {F.y}) by FUNCT_1:68;
then A34: G.(f1.x) in {F.x} /\ {F.y} by FUNCT_1:def 7;
then A35: G.(f1.x) in {F.x} by XBOOLE_0:def 4;
A36: G.(f1.x) in {F.y} by A34,XBOOLE_0:def 4;
A37: G.(f1.x) = F.x by A35,TARSKI:def 1;
G.(f1.x) = F.y by A36,TARSKI:def 1;
hence x = y by A20,A23,A24,A26,A31,A32,A37;
end;
hence IT is one-to-one;
A38: dom(G*IT) = df by A9,RELAT_1:27;
now
let x be object;
assume
A39: x in df;
then A40: F.x in rng F by FUNCT_1:def 3;
then reconsider f = W.(F.x) as Function by A4;
A41: dom f = F"{F.x} & rng f = G"{F.x} by A4,A40;
F.x in {F.x} by TARSKI:def 1;
then x in F"{F.x} by A39,FUNCT_1:def 7;
then f.x in G"{F.x} by A41,FUNCT_1:def 3;
then G.(f.x) in {F.x} by FUNCT_1:def 7;
then A42: G.(f.x) = F.x by TARSKI:def 1;
IT.x = f.x by A9,A39;
hence F.x = (G*IT).x by A9,A39,A42,FUNCT_1:13;
end;
hence thesis by A38;
end;
given H be Function such that
A43: dom H = dom F and
A44: rng H = dom G and
A45: H is one-to-one and
A46: F = G*H;
let x be object;
set t = H|(F"{x});
A47: t is one-to-one by A45,FUNCT_1:52;
A48: dom t = F"{x} by A43,RELAT_1:62,132;
rng t = G"{x}
proof
thus rng t c= G"{x}
proof
let z be object;
assume z in rng t;
then consider y being object such that
A49: y in dom t and
A50: t.y = z by FUNCT_1:def 3;
F.y in {x} by A48,A49,FUNCT_1:def 7;
then A51: F.y = x by TARSKI:def 1;
A52: z = H.y by A49,A50,FUNCT_1:47;
dom t = dom H /\ F"{x} by RELAT_1:61;
then A53: y in dom H by A49,XBOOLE_0:def 4;
then A54: z in dom G by A44,A52,FUNCT_1:def 3;
x = G.z by A46,A51,A52,A53,FUNCT_1:13;
then G.z in {x} by TARSKI:def 1;
hence thesis by A54,FUNCT_1:def 7;
end;
let z be object;
assume
A55: z in G"{x};
then A56: z in dom G by FUNCT_1:def 7;
G.z in {x} by A55,FUNCT_1:def 7;
then A57: G.z = x by TARSKI:def 1;
consider y being object such that
A58: y in dom H and
A59: H.y = z by A44,A56,FUNCT_1:def 3;
F.y = x by A46,A57,A58,A59,FUNCT_1:13;
then F.y in {x} by TARSKI:def 1;
then A60: y in dom t by A43,A48,A58,FUNCT_1:def 7;
then t.y in rng t by FUNCT_1:def 3;
hence thesis by A59,A60,FUNCT_1:47;
end;
hence thesis by CARD_1:5,A47,A48,WELLORD2:def 4;
end;
theorem Th78:
for F,G be Function holds
F,G are_fiberwise_equipotent iff for X be set holds card (F"X) = card (G"X)
proof
let F,G be Function;
thus F,G are_fiberwise_equipotent implies
for X be set holds card(F"X) = card(G"X)
proof
assume F,G are_fiberwise_equipotent;
then consider H be Function such that
A1: dom H = dom F and
A2: rng H = dom G and
A3: H is one-to-one and
A4: F = G*H by Th77;
let X be set;
set t = H|(F"X);
A5: t is one-to-one by A3,FUNCT_1:52;
A6: dom t = F"X by A1,RELAT_1:62,132;
rng t = G"X
proof
thus rng t c= G"X
proof
let z be object;
assume z in rng t;
then consider y being object such that
A7: y in dom t and
A8: t.y = z by FUNCT_1:def 3;
A9: F.y in X by A6,A7,FUNCT_1:def 7;
A10: z = H.y by A7,A8,FUNCT_1:47;
dom t = dom H /\ F"X by RELAT_1:61;
then A11: y in dom H by A7,XBOOLE_0:def 4;
then A12: z in dom G by A2,A10,FUNCT_1:def 3;
G.z in X by A4,A9,A10,A11,FUNCT_1:13;
hence thesis by A12,FUNCT_1:def 7;
end;
let z be object;
assume
A13: z in G"X;
then A14: z in dom G by FUNCT_1:def 7;
A15: G.z in X by A13,FUNCT_1:def 7;
consider y being object such that
A16: y in dom H and
A17: H.y = z by A2,A14,FUNCT_1:def 3;
F.y in X by A4,A15,A16,A17,FUNCT_1:13;
then A18: y in dom t by A1,A6,A16,FUNCT_1:def 7;
then t.y in rng t by FUNCT_1:def 3;
hence thesis by A17,A18,FUNCT_1:47;
end;
hence thesis by CARD_1:5,A5,A6,WELLORD2:def 4;
end;
assume for X be set holds card(F"X) = card(G"X);
hence for x being object holds card Coim(F,x) = card Coim(G,x);
end;
theorem
for D be non empty set, F,G be Function st rng F c= D & rng G c= D &
for d be Element of D holds card Coim(F,d) = card Coim(G,d)
holds F,G are_fiberwise_equipotent
proof
let D be non empty set, F,G be Function;
assume that
A1: rng F c= D and
A2: rng G c= D;
assume
A3: for d be Element of D holds card Coim(F,d) = card Coim(G,d);
let x be object;
per cases;
suppose not x in rng F; then
A4: Coim(F,x) = {} by Lm3;
now assume
A5: x in rng G;
then reconsider d = x as Element of D by A2;
card Coim(G,d) = card Coim(F,d) by A3; then
A6: G"{x} = {} by A4,CARD_1:5,26;
consider y being object such that
A7: y in dom G and
A8: G.y = x by A5,FUNCT_1:def 3;
G.y in {x} by A8,TARSKI:def 1;
hence contradiction by A6,A7,FUNCT_1:def 7;
end;
hence thesis by A4,Lm3;
end;
suppose x in rng F;
then reconsider d = x as Element of D by A1;
card Coim(F,d) = card Coim(G,d) by A3;
hence thesis;
end;
end;
theorem Th80:
for F,G be Function st dom F = dom G holds
F,G are_fiberwise_equipotent iff ex P be Permutation of dom F st F = G*P
proof
let F,G be Function;
assume
A1: dom F = dom G;
thus F,G are_fiberwise_equipotent implies
ex P be Permutation of dom F st F = G*P
proof
assume F,G are_fiberwise_equipotent;
then consider I be Function such that
A2: dom I = dom F and
A3: rng I = dom G and
A4: I is one-to-one and
A5: F = G*I by Th77;
reconsider I as Function of dom F,dom F by A1,A2,A3,FUNCT_2:2;
reconsider I as Permutation of dom F by A1,A3,A4,FUNCT_2:57;
take I;
thus thesis by A5;
end;
given P be Permutation of dom F such that
A6: F = G*P;
P is Function of dom F,dom F & dom F = {} implies dom F ={};
then rng P = dom F & dom P = dom F by FUNCT_2:def 1,def 3;
hence thesis by A1,A6,Th77;
end;
theorem
for F,G be Function
st F,G are_fiberwise_equipotent holds card dom F = card dom G
proof
let F,G be Function;
assume F,G are_fiberwise_equipotent;
then card(F"(rng F)) = card(G"(rng F)) & rng F = rng G by Th75,Th78;
hence card(dom F) = card(G"(rng G)) by RELAT_1:134
.= card(dom G) by RELAT_1:134;
end;
:: from CIRCCOMB, 2009.01.26, A.T.
theorem
for f being set, p being Relation
for x being set st x in rng p holds the_rank_of x in the_rank_of [p,f]
proof
let f be set;
let p be Relation;
let y be set;
assume y in rng p;
then consider x being object such that
A1: [x,y] in p by XTUPLE_0:def 13;
A2: p in {p,f} by TARSKI:def 2;
A3: {p,f} in {{p,f},{p}} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
A5: {x,y} in {{x,y},{x}} by TARSKI:def 2;
A6: the_rank_of y in the_rank_of {x,y} by A4,Th68;
A7: the_rank_of {x,y} in the_rank_of [x,y] by A5,Th68;
A8: the_rank_of p in the_rank_of {p,f} by A2,Th68;
A9: the_rank_of {p,f} in the_rank_of [p,f] by A3,Th68;
A10: the_rank_of y in the_rank_of [x,y] by A6,A7,ORDINAL1:10;
A11: the_rank_of [x,y] in the_rank_of p by A1,Th68;
A12: the_rank_of p in the_rank_of [p,f] by A8,A9,ORDINAL1:10;
the_rank_of y in the_rank_of p by A10,A11,ORDINAL1:10;
hence thesis by A12,ORDINAL1:10;
end;
:: from BAGORDER, 2011.07.24, A.T.
theorem
for f, g, h being Function
st dom f = dom g & rng f c= dom h & rng g c= dom h &
f, g are_fiberwise_equipotent holds h*f, h*g are_fiberwise_equipotent
proof
let f, g, h be Function such that
A1: dom f = dom g and
A2: rng f c= dom h and
A3: rng g c= dom h and
A4: f, g are_fiberwise_equipotent;
consider p being Permutation of dom f such that
A5: f = g*p by A1,A4,Th80;
A6: dom (h*f) = dom f by A2,RELAT_1:27;
A7: dom (h*g) = dom g by A3,RELAT_1:27;
h*f = h*g*p by A5,RELAT_1:36;
hence thesis by A1,A6,A7,Th80;
end;
scheme
LambdaAB { A, B()->set, F(Element of B())->set } :
ex f being Function st
dom f = A() & for x being Element of B() st x in A() holds f.x = F(x)
proof
defpred P[object,object] means
($1 is Element of B() implies ex x being Element of
B() st x=$1 & $2=F(x)) & (not $1 is Element of B() implies $2=0);
A1: for x being object st x in A() ex y being object st P[x,y]
proof
let x be object;
assume x in A();
per cases;
suppose
x is Element of B();
then reconsider z=x as Element of B();
take F(z);
thus thesis;
end;
suppose x is not Element of B();
hence thesis;
end;
end;
consider f being Function such that
A2: dom f = A() and
A3: for x being object st x in A() holds P[x,f.x] from NonUniqFuncEx(A1);
take f;
thus dom f = A() by A2;
let x be Element of B();
assume x in A();
then P[x,f.x] by A3;
hence f.x=F(x);
end;
theorem
for x,y being set holds the_rank_of x in the_rank_of [x,y] &
the_rank_of y in the_rank_of [x,y]
proof
let x,y be set;
{x} in { { x,y }, { x } } by TARSKI:def 2;
then
A1: the_rank_of {x} in the_rank_of { { x,y }, { x } } by Th68;
x in {x} by TARSKI:def 1;
then the_rank_of x in the_rank_of {x} by Th68;
hence the_rank_of x in the_rank_of [x,y] by A1,ORDINAL1:10;
{x,y} in { { x,y }, { x } } by TARSKI:def 2;
then
A2: the_rank_of {x,y} in the_rank_of { { x,y }, { x } } by Th68;
y in {x,y} by TARSKI:def 2;
then the_rank_of y in the_rank_of {x,y} by Th68;
hence thesis by A2,ORDINAL1:10;
end;