:: by Grzegorz Bancerek

::

:: Received March 23, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let B be set ;

end;
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;

for X, Y being set st X in B & Y c= X holds

Y in B;

:: 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 );

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 ;

end;
attr B is Tarski 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 ) ) );

( 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 ) ) );

:: deftheorem Def2 defines Tarski CLASSES1:def 2 :

for B being set holds

( B is Tarski 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 ) ) ) );

for B being set holds

( B is Tarski 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 ) ) ) );

:: 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 ) );

for A, B being set holds

( B is_Tarski-Class_of A iff ( A in B & B is Tarski ) );

definition

let A be set ;

ex b_{1} being set st

( b_{1} is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds

b_{1} c= D ) )

for b_{1}, b_{2} being set st b_{1} is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds

b_{1} c= D ) & b_{2} is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds

b_{2} c= D ) holds

b_{1} = b_{2}

end;
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 ( it is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines Tarski-Class CLASSES1:def 4 :

for A, b_{2} being set holds

( b_{2} = Tarski-Class A iff ( b_{2} is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds

b_{2} c= D ) ) );

for A, b

( b

b

theorem :: CLASSES1:1

for W being set holds

( W is Tarski 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 in card W holds

X in W ) ) )

( W is Tarski 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 in card W holds

X in W ) ) )

proof end;

theorem Th5: :: CLASSES1:5

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 )

( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )

proof end;

theorem :: CLASSES1:6

for Y, X being set st Y c= Tarski-Class X & card Y in card (Tarski-Class X) holds

Y in Tarski-Class X

Y in Tarski-Class X

proof end;

definition

let X be set ;

let A be Ordinal;

existence

ex b_{1} being set ex L being T-Sequence st

( b_{1} = 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 b_{1}, b_{2} being set st ex L being T-Sequence st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2};

end;
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 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) ) );

existence

ex b

( b

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 b

( b

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

( b

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

b

proof end;

:: deftheorem Def5 defines Tarski-Class CLASSES1:def 5 :

for X being set

for A being Ordinal

for b_{3} being set holds

( b_{3} = Tarski-Class (X,A) iff ex L being T-Sequence st

( b_{3} = 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) ) ) );

for X being set

for A being Ordinal

for b

( b

( b

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 :: thesis: for X being set holds

( H_{1}( {} ) = {X} & ( for A being Ordinal holds H_{1}( succ A) = H_{2}(A,H_{1}(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) ) )

( H

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 X be set ; :: thesis: ( H_{1}( {} ) = {X} & ( for A being Ordinal holds H_{1}( succ A) = H_{2}(A,H_{1}(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 H_{1}( Ordinal) -> set = Tarski-Class (X,$1);

deffunc H_{2}( 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 H_{3}( Ordinal, T-Sequence) -> set = (union (rng $2)) /\ (Tarski-Class X);

A1: for A being Ordinal

for x being set holds

( x = H_{1}(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) = H_{2}(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = H_{3}(C,L | C) ) ) )
by Def5;

thus H_{1}( {} ) = {X}
from ORDINAL2:sch 8(A1); :: thesis: ( ( for A being Ordinal holds H_{1}( succ A) = H_{2}(A,H_{1}(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 H_{1}( succ A) = H_{2}(A,H_{1}(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 = 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

end;
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 H

deffunc H

( 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 H

A1: for A being Ordinal

for x being set holds

( x = H

( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = H

L . C = H

thus H

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 H

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 = H_{1}(B)
; :: thesis: Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)

thus H_{1}(A) = H_{3}(A,L)
from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum

end;
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 = H

thus H

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)

end;
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;

theorem :: CLASSES1:8

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;

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 Th9: :: CLASSES1:9

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) ) }

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 Th10: :: CLASSES1:10

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 ) ) ) )

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:11

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 Th10;

for A being Ordinal st Y c= Z & Z in Tarski-Class (X,A) holds

Y in Tarski-Class (X,(succ A)) by Th10;

theorem :: CLASSES1:12

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 Th10;

for A being Ordinal st Y in Tarski-Class (X,A) holds

bool Y in Tarski-Class (X,(succ A)) by Th10;

theorem Th13: :: CLASSES1:13

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) ) )

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:14

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)

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

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

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 :: CLASSES1:20

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 ) )

( 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:21

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)) )

ex A being Ordinal st

( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) )

proof end;

theorem Th22: :: CLASSES1:22

for X being set st X is epsilon-transitive holds

for A being Ordinal st A <> {} holds

Tarski-Class (X,A) is epsilon-transitive

for A being Ordinal st A <> {} holds

Tarski-Class (X,A) is epsilon-transitive

proof end;

theorem Th26: :: CLASSES1:26

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 )

( {x} in Tarski-Class X & {x,y} in Tarski-Class X )

proof end;

definition

let A be Ordinal;

existence

ex b_{1} being set ex L being T-Sequence st

( b_{1} = 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 b_{1}, b_{2} being set st ex L being T-Sequence st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2};

end;
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 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)) ) );

existence

ex b

( b

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 b

( b

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

( b

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

b

proof end;

:: deftheorem Def6 defines Rank CLASSES1:def 6 :

for A being Ordinal

for b_{2} being set holds

( b_{2} = Rank A iff ex L being T-Sequence st

( b_{2} = 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)) ) ) );

for A being Ordinal

for b

( b

( b

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 H

Lm2: now :: thesis: ( H_{1}( {} ) = {} & ( for A being Ordinal holds H_{1}( succ A) = H_{2}(A,H_{1}(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) ) )

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) ) )

deffunc H_{2}( Ordinal, set ) -> Element of bool (bool $2) = bool $2;

deffunc H_{3}( Ordinal, T-Sequence) -> set = union (rng $2);

A1: for A being Ordinal

for x being set holds

( x = H_{1}(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) = H_{2}(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds

L . C = H_{3}(C,L | C) ) ) )
by Def6;

thus H_{1}( {} ) = {}
from ORDINAL2:sch 8(A1); :: thesis: ( ( for A being Ordinal holds H_{1}( succ A) = H_{2}(A,H_{1}(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 H_{1}( succ A) = H_{2}(A,H_{1}(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

end;
deffunc H

A1: for A being Ordinal

for x being set holds

( x = H

( x = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = H

L . C = H

thus H

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 H

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 = H_{1}(B)
; :: thesis: Rank A = union (rng L)

thus H_{1}(A) = H_{3}(A,L)
from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum

end;
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 = H

thus H

theorem Th31: :: CLASSES1:31

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 ) )

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 :: CLASSES1:39

for A being Ordinal

for X being set st X in Rank A holds

( not X, Rank A are_equipotent & card X in card (Rank A) )

for X being set st X in Rank A holds

( not X, Rank A are_equipotent & card X in card (Rank A) )

proof end;

theorem Th44: :: CLASSES1:44

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) )

for A being Ordinal holds

( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )

proof end;

theorem :: CLASSES1:45

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)) )

for A being Ordinal holds

( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )

proof end;

theorem Th46: :: CLASSES1:46

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

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 Th49: :: CLASSES1:49

for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds

X \/ Y is epsilon-transitive

X \/ Y is epsilon-transitive

proof end;

theorem :: CLASSES1:50

for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds

X /\ Y is epsilon-transitive

X /\ Y is epsilon-transitive

proof end;

deffunc H

definition

let X be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being Function ex n being Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being Function ex n being Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being Function ex n being Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) holds

b_{1} = b_{2}

end;
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 Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) );

existence for x being set holds

( x in it iff ex f being Function ex n being Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) );

ex b

for x being set holds

( x in b

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) )

proof end;

uniqueness for b

( x in b

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) & ( for x being set holds

( x in b

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def 7 :

for X, b_{2} being set holds

( b_{2} = the_transitive-closure_of X iff for x being set holds

( x in b_{2} iff ex f being Function ex n being Element of omega st

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) );

for X, b

( b

( x in b

( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) );

theorem Th54: :: CLASSES1:54

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

Y c= Z ) & X c= Y & Y is epsilon-transitive holds

the_transitive-closure_of X = Y

proof end;

theorem :: CLASSES1:59

for X being set holds the_transitive-closure_of (the_transitive-closure_of X) = the_transitive-closure_of X by Th51, Th55;

theorem :: CLASSES1:60

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:61

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;

definition

let X be set ;

ex b_{1} being Ordinal st

( X c= Rank b_{1} & ( for B being Ordinal st X c= Rank B holds

b_{1} c= B ) )

for b_{1}, b_{2} being Ordinal st X c= Rank b_{1} & ( for B being Ordinal st X c= Rank B holds

b_{1} c= B ) & X c= Rank b_{2} & ( for B being Ordinal st X c= Rank B holds

b_{2} c= B ) holds

b_{1} = b_{2}

end;
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 ( X c= Rank it & ( for B being Ordinal st X c= Rank B holds

it c= B ) );

ex b

( X c= Rank b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :

for X being set

for b_{2} being Ordinal holds

( b_{2} = the_rank_of X iff ( X c= Rank b_{2} & ( for B being Ordinal st X c= Rank B holds

b_{2} c= B ) ) );

for X being set

for b

( b

b

theorem Th69: :: CLASSES1:69

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 )

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 Th70: :: CLASSES1:70

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 ) )

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 Th72: :: CLASSES1:72

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 )

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:74

for X being set holds

( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )

( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )

proof end;

begin

:: from RFINSEQ, 2008.10.10, A.T.

definition

let F, G be Relation;

for F being Relation

for x being set holds card (Coim (F,x)) = card (Coim (F,x)) ;

symmetry

for F, G being Relation st ( for x being set holds card (Coim (F,x)) = card (Coim (G,x)) ) holds

for x being set holds card (Coim (G,x)) = card (Coim (F,x)) ;

end;
pred F,G are_fiberwise_equipotent means :Def9: :: CLASSES1:def 9

for x being set holds card (Coim (F,x)) = card (Coim (G,x));

reflexivity for x being set holds card (Coim (F,x)) = card (Coim (G,x));

for F being Relation

for x being set holds card (Coim (F,x)) = card (Coim (F,x)) ;

symmetry

for F, G being Relation st ( for x being set holds card (Coim (F,x)) = card (Coim (G,x)) ) holds

for x being set holds card (Coim (G,x)) = card (Coim (F,x)) ;

:: deftheorem Def9 defines are_fiberwise_equipotent CLASSES1:def 9 :

for F, G being Relation holds

( F,G are_fiberwise_equipotent iff for x being set holds card (Coim (F,x)) = card (Coim (G,x)) );

for F, G being Relation holds

( F,G are_fiberwise_equipotent iff for x being set holds card (Coim (F,x)) = card (Coim (G,x)) );

Lm3: for F being Function

for x being set st not x in rng F holds

Coim (F,x) = {}

proof end;

theorem :: CLASSES1:76

for F, G, H being Function st F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent holds

G,H are_fiberwise_equipotent

G,H are_fiberwise_equipotent

proof end;

theorem Th77: :: CLASSES1:77

for F, G being Function holds

( F,G are_fiberwise_equipotent iff ex H being Function st

( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )

( F,G are_fiberwise_equipotent iff ex H being Function st

( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )

proof end;

theorem Th78: :: CLASSES1:78

for F, G being Function holds

( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )

( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )

proof end;

theorem :: CLASSES1:79

for D being non empty set

for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ) holds

F,G are_fiberwise_equipotent

for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ) holds

F,G are_fiberwise_equipotent

proof end;

theorem Th80: :: CLASSES1:80

for F, G being Function st dom F = dom G holds

( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )

( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )

proof end;

:: from CIRCCOMB, 2009.01.26, A.T.

theorem :: CLASSES1:82

for f being set

for p being Relation

for x being set st x in rng p holds

the_rank_of x in the_rank_of [p,f]

for p being Relation

for x being set st x in rng p holds

the_rank_of x in the_rank_of [p,f]

proof end;

:: from BAGORDER, 2011.07.24, A.T.

theorem :: CLASSES1:83

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

h * f,h * g are_fiberwise_equipotent

proof end;