:: Tarski's Classes and Ranks
:: by Grzegorz Bancerek
::
:: Received March 23, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines subset-closed CLASSES1:def 1 :
:: deftheorem Def2 defines Tarski CLASSES1:def 2 :
:: deftheorem Def3 defines is_Tarski-Class_of CLASSES1:def 3 :
:: deftheorem Def4 defines Tarski-Class CLASSES1:def 4 :
theorem :: CLASSES1:1
canceled;
theorem :: CLASSES1:2
theorem :: CLASSES1:3
canceled;
theorem :: CLASSES1:4
canceled;
theorem Th5: :: CLASSES1:5
theorem Th6: :: CLASSES1:6
theorem Th7: :: CLASSES1:7
theorem Th8: :: CLASSES1:8
theorem :: CLASSES1:9
:: deftheorem Def5 defines Tarski-Class CLASSES1:def 5 :
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(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(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;
theorem :: CLASSES1:10
theorem :: CLASSES1:11
theorem Th12: :: CLASSES1:12
theorem Th13: :: CLASSES1:13
theorem :: CLASSES1:14
theorem :: CLASSES1:15
theorem Th16: :: CLASSES1:16
theorem :: CLASSES1:17
theorem Th18: :: CLASSES1:18
theorem Th19: :: CLASSES1:19
theorem Th20: :: CLASSES1:20
theorem Th21: :: CLASSES1:21
theorem Th22: :: CLASSES1:22
theorem :: CLASSES1:23
theorem :: CLASSES1:24
theorem Th25: :: CLASSES1:25
theorem :: CLASSES1:26
theorem Th27: :: CLASSES1:27
theorem Th28: :: CLASSES1:28
theorem Th29: :: CLASSES1:29
theorem Th30: :: CLASSES1:30
theorem Th31: :: CLASSES1:31
theorem :: CLASSES1:32
:: deftheorem Def6 defines Rank CLASSES1:def 6 :
deffunc H1( Ordinal) -> set = Rank $1;
theorem :: CLASSES1:33
theorem :: CLASSES1:34
theorem Th35: :: CLASSES1:35
theorem Th36: :: CLASSES1:36
theorem :: CLASSES1:37
canceled;
theorem :: CLASSES1:38
canceled;
theorem :: CLASSES1:39
theorem Th40: :: CLASSES1:40
theorem :: CLASSES1:41
theorem Th42: :: CLASSES1:42
theorem Th43: :: CLASSES1:43
theorem Th44: :: CLASSES1:44
theorem :: CLASSES1:45
theorem :: CLASSES1:46
theorem Th47: :: CLASSES1:47
theorem Th48: :: CLASSES1:48
theorem Th49: :: CLASSES1:49
theorem Th50: :: CLASSES1:50
theorem :: CLASSES1:51
theorem Th52: :: CLASSES1:52
theorem Th53: :: CLASSES1:53
theorem Th54: :: CLASSES1:54
theorem Th55: :: CLASSES1:55
theorem :: CLASSES1:56
deffunc H2( set , set ) -> set = union $2;
:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def 7 :
theorem :: CLASSES1:57
canceled;
theorem Th58: :: CLASSES1:58
theorem Th59: :: CLASSES1:59
theorem Th60: :: CLASSES1:60
theorem Th61: :: CLASSES1:61
theorem Th62: :: CLASSES1:62
theorem :: CLASSES1:63
theorem :: CLASSES1:64
theorem Th65: :: CLASSES1:65
theorem :: CLASSES1:66
theorem :: CLASSES1:67
theorem :: CLASSES1:68
theorem Th69: :: CLASSES1:69
:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :
theorem :: CLASSES1:70
canceled;
theorem Th71: :: CLASSES1:71
theorem :: CLASSES1:72
theorem Th73: :: CLASSES1:73
theorem Th74: :: CLASSES1:74
theorem :: CLASSES1:75
theorem Th76: :: CLASSES1:76
theorem Th77: :: CLASSES1:77
theorem Th78: :: CLASSES1:78
theorem :: CLASSES1:79
theorem Th80: :: CLASSES1:80
theorem :: CLASSES1:81
theorem :: CLASSES1:82
definition
let F,
G be
Relation;
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 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;
:: deftheorem Def9 defines are_fiberwise_equipotent CLASSES1:def 9 :
Lm3:
for F being Function
for x being set st not x in rng F holds
Coim F,x = {}
theorem Th83: :: CLASSES1:83
theorem :: CLASSES1:84
theorem Th85: :: CLASSES1:85
theorem Th86: :: CLASSES1:86
theorem :: CLASSES1:87
theorem :: CLASSES1:88
theorem :: CLASSES1:89
theorem :: CLASSES1:90