:: CLASSES1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let B be set ;
attr B is subset-closed means :Def1: :: CLASSES1:def 1
for X, Y being set st X in B & Y c= X holds
Y in B;
end;

:: deftheorem Def1 defines subset-closed CLASSES1:def 1 :
for B being set holds
( B is subset-closed iff for X, Y being set st X in B & Y c= X holds
Y in B );

definition
let B be set ;
attr B is being_Tarski-Class means :Def2: :: CLASSES1:def 2
( B is subset-closed & ( for X being set st X in B holds
bool X in B ) & ( for X being set holds
( not X c= B or X,B are_equipotent or X in B ) ) );
end;

:: deftheorem Def2 defines being_Tarski-Class CLASSES1:def 2 :
for B being set holds
( B is being_Tarski-Class iff ( B is subset-closed & ( for X being set st X in B holds
bool X in B ) & ( for X being set holds
( not X c= B or X,B are_equipotent or X in B ) ) ) );

notation
let B be set ;
synonym B is_Tarski-Class for being_Tarski-Class B;
end;

definition
let A, B be set ;
pred B is_Tarski-Class_of A means :Def3: :: CLASSES1:def 3
( A in B & B is_Tarski-Class );
end;

:: deftheorem Def3 defines is_Tarski-Class_of CLASSES1:def 3 :
for A, B being set holds
( B is_Tarski-Class_of A iff ( A in B & B is_Tarski-Class ) );

definition
let A be set ;
func Tarski-Class A -> set means :Def4: :: CLASSES1:def 4
( it is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
it c= D ) );
existence
ex b1 being set st
( b1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being set st b1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b1 c= D ) & b2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Tarski-Class CLASSES1:def 4 :
for A, b2 being set holds
( b2 = Tarski-Class A iff ( b2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b2 c= D ) ) );

registration
let A be set ;
cluster Tarski-Class A -> non empty ;
coherence
not Tarski-Class A is empty
proof end;
end;

theorem :: CLASSES1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CLASSES1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being set holds
( W is_Tarski-Class iff ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & Card X <` Card W holds
X in W ) ) )
proof end;

theorem :: CLASSES1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CLASSES1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: CLASSES1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds X in Tarski-Class X
proof end;

theorem Th6: :: CLASSES1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X, Z being set st Y in Tarski-Class X & Z c= Y holds
Z in Tarski-Class X
proof end;

theorem Th7: :: CLASSES1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y in Tarski-Class X holds
bool Y in Tarski-Class X
proof end;

theorem Th8: :: CLASSES1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set holds
( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )
proof end;

theorem :: CLASSES1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y c= Tarski-Class X & Card Y <` Card (Tarski-Class X) holds
Y in Tarski-Class X
proof end;

definition
let X be set ;
let A be Ordinal;
func Tarski-Class X,A -> set means :Def5: :: CLASSES1:def 5
ex L being T-Sequence st
( it = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in L . C }
)
\/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in L . C }
)
\/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) )
;
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in L . C }
)
\/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) & ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in L . C }
)
\/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines Tarski-Class CLASSES1:def 5 :
for X being set
for A being Ordinal
for b3 being set holds
( b3 = Tarski-Class X,A iff ex L being T-Sequence st
( b3 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in L . C }
)
\/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) );

Lm1: now
let X be set ; :: thesis: ( H1( {} ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) holds
Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X) ) )

deffunc H1( Ordinal) -> set = Tarski-Class X,$1;
deffunc H2( Ordinal, set ) -> set = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in $2 }
)
\/ ((bool $2) /\ (Tarski-Class X));
deffunc H3( Ordinal, T-Sequence) -> set = (union (rng $2)) /\ (Tarski-Class X);
A1: for A being Ordinal
for x being set holds
( x = H1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H2(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = H3(C,L | C) ) ) ) by Def5;
thus H1( {} ) = {X} from ORDINAL2:sch 8( {X} , A1); :: thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) holds
Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X) ) )

thus for A being Ordinal holds H1( succ A) = H2(A,H1(A)) from ORDINAL2:sch 9( {X} , A1); :: thesis: for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) holds
Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X)

thus for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) holds
Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X) :: thesis: verum
proof
let A be Ordinal; :: thesis: for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) holds
Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X)

let L be T-Sequence; :: thesis: ( A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class X,B ) implies Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X) )

assume that
A2: ( A <> {} & A is_limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H1(B) ; :: thesis: Tarski-Class X,A = (union (rng L)) /\ (Tarski-Class X)
thus H1(A) = H3(A,L) from ORDINAL2:sch 10( Y A {X} , A1, A2, A3, A4); :: thesis: verum
end;
end;

definition
let X be set ;
let A be Ordinal;
:: original: Tarski-Class
redefine func Tarski-Class X,A -> Subset of (Tarski-Class X);
coherence
Tarski-Class X,A is Subset of (Tarski-Class X)
proof end;
end;

theorem :: CLASSES1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Tarski-Class X,{} = {X} by Lm1;

theorem :: CLASSES1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds Tarski-Class X,(succ A) = ({ u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class X,A & u c= v )
}
\/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class X,A }
)
\/ ((bool (Tarski-Class X,A)) /\ (Tarski-Class X)) by Lm1;

theorem Th12: :: CLASSES1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st A <> {} & A is_limit_ordinal holds
Tarski-Class X,A = { u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class X,B )
}
proof end;

theorem Th13: :: CLASSES1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set
for A being Ordinal holds
( Y in Tarski-Class X,(succ A) iff ( ( Y c= Tarski-Class X,A & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class X,A & ( Y c= Z or Y = bool Z ) ) ) )
proof end;

theorem :: CLASSES1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, Z, X being set
for A being Ordinal st Y c= Z & Z in Tarski-Class X,A holds
Y in Tarski-Class X,(succ A) by Th13;

theorem :: CLASSES1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set
for A being Ordinal st Y in Tarski-Class X,A holds
bool Y in Tarski-Class X,(succ A) by Th13;

theorem Th16: :: CLASSES1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x being set
for A being Ordinal st A <> {} & A is_limit_ordinal holds
( x in Tarski-Class X,A iff ex B being Ordinal st
( B in A & x in Tarski-Class X,B ) )
proof end;

theorem :: CLASSES1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X, Z being set
for A being Ordinal st A <> {} & A is_limit_ordinal & Y in Tarski-Class X,A & ( Z c= Y or Z = bool Y ) holds
Z in Tarski-Class X,A
proof end;

theorem Th18: :: CLASSES1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds Tarski-Class X,A c= Tarski-Class X,(succ A)
proof end;

theorem Th19: :: CLASSES1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A, B being Ordinal st A c= B holds
Tarski-Class X,A c= Tarski-Class X,B
proof end;

theorem Th20: :: CLASSES1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set ex A being Ordinal st Tarski-Class X,A = Tarski-Class X,(succ A)
proof end;

theorem Th21: :: CLASSES1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st Tarski-Class X,A = Tarski-Class X,(succ A) holds
Tarski-Class X,A = Tarski-Class X
proof end;

theorem Th22: :: CLASSES1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set ex A being Ordinal st Tarski-Class X,A = Tarski-Class X
proof end;

theorem :: CLASSES1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set ex A being Ordinal st
( Tarski-Class X,A = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class X,B <> Tarski-Class X ) )
proof end;

theorem :: CLASSES1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y <> X & Y in Tarski-Class X holds
ex A being Ordinal st
( not Y in Tarski-Class X,A & Y in Tarski-Class X,(succ A) )
proof end;

theorem Th25: :: CLASSES1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is epsilon-transitive holds
for A being Ordinal st A <> {} holds
Tarski-Class X,A is epsilon-transitive
proof end;

theorem :: CLASSES1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( Tarski-Class X,{} in Tarski-Class X,one & Tarski-Class X,{} <> Tarski-Class X,one )
proof end;

theorem Th27: :: CLASSES1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is epsilon-transitive holds
Tarski-Class X is epsilon-transitive
proof end;

theorem Th28: :: CLASSES1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y in Tarski-Class X holds
Card Y <` Card (Tarski-Class X)
proof end;

theorem Th29: :: CLASSES1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y in Tarski-Class X holds
not Y, Tarski-Class X are_equipotent
proof end;

theorem Th30: :: CLASSES1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x, y being set st x in Tarski-Class X & y in Tarski-Class X holds
( {x} in Tarski-Class X & {x,y} in Tarski-Class X )
proof end;

theorem Th31: :: CLASSES1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x, y being set st x in Tarski-Class X & y in Tarski-Class X holds
[x,y] in Tarski-Class X
proof end;

theorem :: CLASSES1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X, Z being set st Y c= Tarski-Class X & Z c= Tarski-Class X holds
[:Y,Z:] c= Tarski-Class X
proof end;

definition
let A be Ordinal;
func Rank A -> set means :Def6: :: CLASSES1:def 6
ex L being T-Sequence st
( it = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = union (rng (L | C)) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = union (rng (L | C)) ) )
;
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = union (rng (L | C)) ) ) & ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = union (rng (L | C)) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def6 defines Rank CLASSES1:def 6 :
for A being Ordinal
for b2 being set holds
( b2 = Rank A iff ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = union (rng (L | C)) ) ) );

deffunc H1( Ordinal) -> set = Rank $1;

Lm2: now
deffunc H2( Ordinal, set ) -> set = bool $2;
deffunc H3( Ordinal, T-Sequence) -> set = union (rng $2);
A1: for A being Ordinal
for x being set holds
( x = H1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H2(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = H3(C,L | C) ) ) ) by Def6;
thus H1( {} ) = {} from ORDINAL2:sch 8( {} , A1); :: thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L) ) )

thus for A being Ordinal holds H1( succ A) = H2(A,H1(A)) from ORDINAL2:sch 9( {} , A1); :: thesis: for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L)

thus for A being Ordinal
for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L) :: thesis: verum
proof
let A be Ordinal; :: thesis: for L being T-Sequence st A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L)

let L be T-Sequence; :: thesis: ( A <> {} & A is_limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) implies Rank A = union (rng L) )

assume that
A2: ( A <> {} & A is_limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H1(B) ; :: thesis: Rank A = union (rng L)
thus H1(A) = H3(A,L) from ORDINAL2:sch 10( A X {} , A1, A2, A3, A4); :: thesis: verum
end;
end;

theorem :: CLASSES1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Rank {} = {} by Lm2;

theorem :: CLASSES1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds Rank (succ A) = bool (Rank A) by Lm2;

theorem Th35: :: CLASSES1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal st A <> {} & A is_limit_ordinal holds
for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
proof end;

theorem Th36: :: CLASSES1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( X c= Rank A iff X in Rank (succ A) )
proof end;

theorem Th37: :: CLASSES1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds Rank A is epsilon-transitive
proof end;

theorem Th38: :: CLASSES1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st X in Rank A holds
X c= Rank A
proof end;

theorem :: CLASSES1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds Rank A c= Rank (succ A)
proof end;

theorem Th40: :: CLASSES1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds union (Rank A) c= Rank A
proof end;

theorem :: CLASSES1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st X in Rank A holds
union X in Rank A
proof end;

theorem Th42: :: CLASSES1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal holds
( A in B iff Rank A in Rank B )
proof end;

theorem Th43: :: CLASSES1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal holds
( A c= B iff Rank A c= Rank B )
proof end;

theorem Th44: :: CLASSES1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds A c= Rank A
proof end;

theorem :: CLASSES1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal
for X being set st X in Rank A holds
( not X, Rank A are_equipotent & Card X <` Card (Rank A) )
proof end;

theorem :: CLASSES1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( X c= Rank A iff bool X c= Rank (succ A) )
proof end;

theorem Th47: :: CLASSES1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for A being Ordinal st X c= Y & Y in Rank A holds
X in Rank A
proof end;

theorem Th48: :: CLASSES1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( X in Rank A iff bool X in Rank (succ A) )
proof end;

theorem Th49: :: CLASSES1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for A being Ordinal holds
( x in Rank A iff {x} in Rank (succ A) )
proof end;

theorem Th50: :: CLASSES1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )
proof end;

theorem :: CLASSES1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
proof end;

theorem Th52: :: CLASSES1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) holds
Tarski-Class X c= Rank A
proof end;

theorem Th53: :: CLASSES1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is epsilon-transitive holds
ex A being Ordinal st Tarski-Class X c= Rank A
proof end;

theorem Th54: :: CLASSES1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is epsilon-transitive holds
union X c= X
proof end;

theorem Th55: :: CLASSES1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds
X \/ Y is epsilon-transitive
proof end;

theorem :: CLASSES1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds
X /\ Y is epsilon-transitive
proof end;

deffunc H2( set , set ) -> set = union $2;

definition
let X be set ;
func the_transitive-closure_of X -> set means :Def7: :: CLASSES1:def 7
for x being set holds
( x in it iff ex f being Function ex n being Nat st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function ex n being Nat st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function ex n being Nat st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function ex n being Nat st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def 7 :
for X, b2 being set holds
( b2 = the_transitive-closure_of X iff for x being set holds
( x in b2 iff ex f being Function ex n being Nat st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) ) );

theorem :: CLASSES1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th58: :: CLASSES1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the_transitive-closure_of X is epsilon-transitive
proof end;

theorem Th59: :: CLASSES1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds X c= the_transitive-closure_of X
proof end;

theorem Th60: :: CLASSES1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X c= Y
proof end;

theorem Th61: :: CLASSES1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st ( for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ) & X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X = Y
proof end;

theorem Th62: :: CLASSES1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st X is epsilon-transitive holds
the_transitive-closure_of X = X
proof end;

theorem :: CLASSES1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_transitive-closure_of {} = {} by Th62;

theorem :: CLASSES1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds the_transitive-closure_of A = A by Th62;

theorem Th65: :: CLASSES1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
the_transitive-closure_of X c= the_transitive-closure_of Y
proof end;

theorem :: CLASSES1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the_transitive-closure_of (the_transitive-closure_of X) = the_transitive-closure_of X
proof end;

theorem :: CLASSES1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)
proof end;

theorem :: CLASSES1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y)
proof end;

theorem Th69: :: CLASSES1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set ex A being Ordinal st X c= Rank A
proof end;

definition
let X be set ;
func the_rank_of X -> Ordinal means :Def8: :: CLASSES1:def 8
( X c= Rank it & ( for B being Ordinal st X c= Rank B holds
it c= B ) );
existence
ex b1 being Ordinal st
( X c= Rank b1 & ( for B being Ordinal st X c= Rank B holds
b1 c= B ) )
proof end;
uniqueness
for b1, b2 being Ordinal st X c= Rank b1 & ( for B being Ordinal st X c= Rank B holds
b1 c= B ) & X c= Rank b2 & ( for B being Ordinal st X c= Rank B holds
b2 c= B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :
for X being set
for b2 being Ordinal holds
( b2 = the_rank_of X iff ( X c= Rank b2 & ( for B being Ordinal st X c= Rank B holds
b2 c= B ) ) );

theorem :: CLASSES1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th71: :: CLASSES1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the_rank_of (bool X) = succ (the_rank_of X)
proof end;

theorem :: CLASSES1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds the_rank_of (Rank A) = A
proof end;

theorem Th73: :: CLASSES1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( X c= Rank A iff the_rank_of X c= A )
proof end;

theorem Th74: :: CLASSES1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( X in Rank A iff the_rank_of X in A )
proof end;

theorem :: CLASSES1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
the_rank_of X c= the_rank_of Y
proof end;

theorem Th76: :: CLASSES1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X in Y holds
the_rank_of X in the_rank_of Y
proof end;

theorem Th77: :: CLASSES1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
proof end;

theorem Th78: :: CLASSES1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal holds
( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
proof end;

theorem :: CLASSES1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( the_rank_of X = {} iff X = {} )
proof end;

theorem Th80: :: CLASSES1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Ordinal st the_rank_of X = succ A holds
ex Y being set st
( Y in X & the_rank_of Y = A )
proof end;

theorem :: CLASSES1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds the_rank_of A = A
proof end;

theorem :: CLASSES1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is_limit_ordinal )
proof end;