:: by Bogdan Nowak and Grzegorz Bancerek

::

:: Received April 10, 1990

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

Lm1: for X being set holds Tarski-Class X is Tarski

proof end;

registration
end;

theorem Th1: :: CLASSES2:1

for X, W being set st W is subset-closed & X in W holds

( not X,W are_equipotent & card X in card W )

( not X,W are_equipotent & card X in card W )

proof end;

theorem :: CLASSES2:6

for A being Ordinal

for W being set st A in Tarski-Class W holds

( succ A in Tarski-Class W & A c= Tarski-Class W ) by Th5;

for W being set st A in Tarski-Class W holds

( succ A in Tarski-Class W & A c= Tarski-Class W ) by Th5;

theorem :: CLASSES2:8

for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds

X c= Tarski-Class W by Th7;

X c= Tarski-Class W by Th7;

theorem :: CLASSES2:12

theorem :: CLASSES2:14

theorem :: CLASSES2:17

theorem :: CLASSES2:18

theorem :: CLASSES2:20

theorem Th21: :: CLASSES2:21

for W being set holds

( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )

( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )

proof end;

theorem Th22: :: CLASSES2:22

for X, W being set st W is Tarski & ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) holds

Funcs (X,W) c= W

Funcs (X,W) c= W

proof end;

theorem :: CLASSES2:23

for X, W being set st ( ( X in Tarski-Class W & W is epsilon-transitive ) or ( X in Tarski-Class W & X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) & X c= Tarski-Class W ) ) holds

Funcs (X,(Tarski-Class W)) c= Tarski-Class W

Funcs (X,(Tarski-Class W)) c= Tarski-Class W

proof end;

theorem Th24: :: CLASSES2:24

for L being Sequence st dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds

L . A = Rank A ) holds

Rank (dom L) = Union L

L . A = Rank A ) holds

Rank (dom L) = Union L

proof end;

defpred S

( card (Rank $1) in card W & Rank $1 in W );

Lm2: S

by Th9, CLASSES1:29, ORDINAL1:def 9;

Lm3: for A being Ordinal st S

S

proof end;

Lm4: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds

S

S

proof end;

theorem Th25: :: CLASSES2:25

for A being Ordinal

for W being set st W is Tarski & A in On W holds

( card (Rank A) in card W & Rank A in W )

for W being set st W is Tarski & A in On W holds

( card (Rank A) in card W & Rank A in W )

proof end;

theorem :: CLASSES2:26

for A being Ordinal

for W being set st A in On (Tarski-Class W) holds

( card (Rank A) in card (Tarski-Class W) & Rank A in Tarski-Class W ) by Th25;

for W being set st A in On (Tarski-Class W) holds

( card (Rank A) in card (Tarski-Class W) & Rank A in Tarski-Class W ) by Th25;

deffunc H

deffunc H

theorem :: CLASSES2:33

for A being Ordinal

for W being set st A in On (Tarski-Class W) holds

card (Rank A) c= card (Tarski-Class W)

for W being set st A in On (Tarski-Class W) holds

card (Rank A) c= card (Tarski-Class W)

proof end;

theorem :: CLASSES2:35

theorem Th36: :: CLASSES2:36

for X, W being set st W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent holds

X in Rank (card W)

X in Rank (card W)

proof end;

theorem :: CLASSES2:37

for X, W being set holds

( not X c= Rank (card (Tarski-Class W)) or X, Rank (card (Tarski-Class W)) are_equipotent or X in Rank (card (Tarski-Class W)) ) by Th36;

( not X c= Rank (card (Tarski-Class W)) or X, Rank (card (Tarski-Class W)) are_equipotent or X in Rank (card (Tarski-Class W)) ) by Th36;

theorem Th40: :: CLASSES2:40

for A being Ordinal

for X being set st X is epsilon-transitive & A in the_rank_of X holds

ex Y being set st

( Y in X & the_rank_of Y = A )

for X being set st X is epsilon-transitive & A in the_rank_of X holds

ex Y being set st

( Y in X & the_rank_of Y = A )

proof end;

theorem :: CLASSES2:43

for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds

X in Rank (card (Tarski-Class W)) by Th42;

X in Rank (card (Tarski-Class W)) by Th42;

theorem Th44: :: CLASSES2:44

for W being set st W is epsilon-transitive holds

Rank (card (Tarski-Class W)) is_Tarski-Class_of W by CLASSES1:2, Th38, Th42;

Rank (card (Tarski-Class W)) is_Tarski-Class_of W by CLASSES1:2, Th38, Th42;

:: deftheorem defines universal CLASSES2:def 1 :

for IT being set holds

( IT is universal iff ( IT is epsilon-transitive & IT is Tarski ) );

for IT being set holds

( IT is universal iff ( IT is epsilon-transitive & IT is Tarski ) );

registration

coherence

for b_{1} being set st b_{1} is universal holds

( b_{1} is epsilon-transitive & b_{1} is Tarski )
;

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is Tarski holds

b_{1} is universal
;

end;
for b

( b

coherence

for b

b

registration
end;

registration

let U be Universe;

coherence

On U is ordinal by Th46;

coherence

Tarski-Class U is universal by Th47;

end;
coherence

On U is ordinal by Th46;

coherence

Tarski-Class U is universal by Th47;

theorem :: CLASSES2:58

theorem Th60: :: CLASSES2:60

for X, Y being set

for U being Universe st X in U & Y in U holds

( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )

for U being Universe st X in U & Y in U holds

( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )

proof end;

theorem Th61: :: CLASSES2:61

for X, Y being set

for U being Universe st X in U & Y in U holds

( [:X,Y:] in U & Funcs (X,Y) in U )

for U being Universe st X in U & Y in U holds

( [:X,Y:] in U & Funcs (X,Y) in U )

proof end;

registration
end;

definition

let U be Universe;

let u be Element of U;

:: original: {

redefine func {u} -> Element of U;

coherence

{u} is Element of U by Th2;

:: original: bool

redefine func bool u -> Element of U;

coherence

bool u is Element of U by Th59;

:: original: union

redefine func union u -> Element of U;

coherence

union u is Element of U by Th59;

:: original: meet

redefine func meet u -> Element of U;

coherence

meet u is Element of U by Th59;

let v be Element of U;

:: original: {

redefine func {u,v} -> Element of U;

coherence

{u,v} is Element of U by Th2;

:: original: [

redefine func [u,v] -> Element of U;

coherence

[u,v] is Element of U by Th3;

:: original: \/

redefine func u \/ v -> Element of U;

coherence

u \/ v is Element of U by Th60;

:: original: /\

redefine func u /\ v -> Element of U;

coherence

u /\ v is Element of U by Th60;

:: original: \

redefine func u \ v -> Element of U;

coherence

u \ v is Element of U by Th60;

:: original: \+\

redefine func u \+\ v -> Element of U;

coherence

u \+\ v is Element of U by Th60;

:: original: [:

redefine func [:u,v:] -> Element of U;

coherence

[:u,v:] is Element of U by Th61;

:: original: Funcs

redefine func Funcs (u,v) -> Element of U;

coherence

Funcs (u,v) is Element of U by Th61;

end;
let u be Element of U;

:: original: {

redefine func {u} -> Element of U;

coherence

{u} is Element of U by Th2;

:: original: bool

redefine func bool u -> Element of U;

coherence

bool u is Element of U by Th59;

:: original: union

redefine func union u -> Element of U;

coherence

union u is Element of U by Th59;

:: original: meet

redefine func meet u -> Element of U;

coherence

meet u is Element of U by Th59;

let v be Element of U;

:: original: {

redefine func {u,v} -> Element of U;

coherence

{u,v} is Element of U by Th2;

:: original: [

redefine func [u,v] -> Element of U;

coherence

[u,v] is Element of U by Th3;

:: original: \/

redefine func u \/ v -> Element of U;

coherence

u \/ v is Element of U by Th60;

:: original: /\

redefine func u /\ v -> Element of U;

coherence

u /\ v is Element of U by Th60;

:: original: \

redefine func u \ v -> Element of U;

coherence

u \ v is Element of U by Th60;

:: original: \+\

redefine func u \+\ v -> Element of U;

coherence

u \+\ v is Element of U by Th60;

:: original: [:

redefine func [:u,v:] -> Element of U;

coherence

[:u,v:] is Element of U by Th61;

:: original: Funcs

redefine func Funcs (u,v) -> Element of U;

coherence

Funcs (u,v) is Element of U by Th61;

Lm5: omega is limit_ordinal

by ORDINAL1:def 11;

registration
end;

definition

let X be set ;

for b_{1}, b_{2} being Universe st X c= b_{1} & ( for Y being Universe st X c= Y holds

b_{1} c= Y ) & X c= b_{2} & ( for Y being Universe st X c= Y holds

b_{2} c= Y ) holds

b_{1} = b_{2}
;

existence

ex b_{1} being Universe st

( X c= b_{1} & ( for Y being Universe st X c= Y holds

b_{1} c= Y ) )

end;
func Universe_closure X -> Universe means :Def4: :: CLASSES2:def 4

( X c= it & ( for Y being Universe st X c= Y holds

it c= Y ) );

uniqueness ( X c= it & ( for Y being Universe st X c= Y holds

it c= Y ) );

for b

b

b

b

existence

ex b

( X c= b

b

proof end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def 4 :

for X being set

for b_{2} being Universe holds

( b_{2} = Universe_closure X iff ( X c= b_{2} & ( for Y being Universe st X c= Y holds

b_{2} c= Y ) ) );

for X being set

for b

( b

b

deffunc H

deffunc H

definition

mode FinSet is Element of FinSETS ;

mode Set is Element of SETS ;

let A be Ordinal;

existence

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

( b_{1} = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) );

uniqueness

for b_{1}, b_{2} being set st ex L being Sequence st

( b_{1} = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) & ex L being Sequence st

( b_{2} = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) holds

b_{1} = b_{2};

end;
mode Set is Element of SETS ;

let A be Ordinal;

func UNIVERSE A -> set means :Def5: :: CLASSES2:def 5

ex L being Sequence st

( it = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) );

correctness ex L being Sequence st

( it = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) );

existence

ex b

( b

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) );

uniqueness

for b

( b

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) & ex L being Sequence st

( b

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) holds

b

proof end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 :

for A being Ordinal

for b_{2} being set holds

( b_{2} = UNIVERSE A iff ex L being Sequence st

( b_{2} = last L & dom L = succ A & L . 0 = FinSETS & ( for C being Ordinal st succ C in succ A holds

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) );

for A being Ordinal

for b

( b

( b

L . (succ C) = Tarski-Class (L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

L . C = Universe_closure (Union (L | C)) ) ) );

deffunc H

Lm6: now :: thesis: ( H_{5}( 0 ) = FinSETS & ( for A being Ordinal holds H_{5}( succ A) = H_{3}(A,H_{5}(A)) ) & ( for A being Ordinal

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H_{5}(B) ) holds

H_{5}(A) = H_{4}(A,L) ) )

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H

H

A1:
for A being Ordinal

for x being object holds

( x = H_{5}(A) iff ex L being Sequence st

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

L . (succ C) = H_{3}(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds

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

thus H_{5}( 0 ) = FinSETS
from ORDINAL2:sch 8(A1); :: thesis: ( ( for A being Ordinal holds H_{5}( succ A) = H_{3}(A,H_{5}(A)) ) & ( for A being Ordinal

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H_{5}(B) ) holds

H_{5}(A) = H_{4}(A,L) ) )

thus for A being Ordinal holds H_{5}( succ A) = H_{3}(A,H_{5}(A))
from ORDINAL2:sch 9(A1); :: thesis: for A being Ordinal

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H_{5}(B) ) holds

H_{5}(A) = H_{4}(A,L)

let A be Ordinal; :: thesis: for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H_{5}(B) ) holds

H_{5}(A) = H_{4}(A,L)

let L be Sequence; :: thesis: ( A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H_{5}(B) ) implies H_{5}(A) = H_{4}(A,L) )

assume that

A2: ( A <> 0 & A is limit_ordinal ) and

A3: dom L = A and

A4: for B being Ordinal st B in A holds

L . B = H_{5}(B)
; :: thesis: H_{5}(A) = H_{4}(A,L)

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

end;
for x being object holds

( x = H

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

L . (succ C) = H

L . C = H

thus H

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H

H

thus for A being Ordinal holds H

for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H

H

let A be Ordinal; :: thesis: for L being Sequence st A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H

H

let L be Sequence; :: thesis: ( A <> 0 & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds

L . B = H

assume that

A2: ( A <> 0 & 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

registration
end;

theorem :: CLASSES2:66

Lm7: 1 = succ 0

;

theorem :: CLASSES2:68

theorem :: CLASSES2:73

for X being set holds

( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )

( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )

proof end;