:: Universal Classes
:: by Bogdan Nowak and Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2017 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 CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, ZFMISC_1, XBOOLE_0,
RELAT_1, CARD_3, FUNCT_2, SUBSET_1, SETFAM_1, FINSET_1, ORDINAL2,
CLASSES2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL2, CLASSES1,
CARD_3;
constructors SETFAM_1, WELLORD2, ORDINAL2, CLASSES1, CARD_3, NUMBERS, FUNCT_2,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, CARD_1, CLASSES1;
requirements SUBSET, BOOLE, NUMERALS;
begin
reserve m for Cardinal,
A,B,C for Ordinal,
x,y,z,X,Y,Z,W for set,
f for Function;
registration
cluster Tarski -> subset-closed for set;
end;
registration
let X be set;
cluster Tarski-Class X -> Tarski;
end;
theorem :: CLASSES2:1
W is subset-closed & X in W implies not X,W are_equipotent & card X in card W
;
theorem :: CLASSES2:2
W is Tarski & x in W & y in W implies {x} in W & {x,y} in W;
theorem :: CLASSES2:3
W is Tarski & x in W & y in W implies [x,y] in W;
theorem :: CLASSES2:4
W is Tarski & X in W implies Tarski-Class X c= W;
theorem :: CLASSES2:5
W is Tarski & A in W implies succ A in W & A c= W;
theorem :: CLASSES2:6
A in Tarski-Class W implies succ A in Tarski-Class W & A c=
Tarski-Class W;
theorem :: CLASSES2:7
W is subset-closed & X is epsilon-transitive & X in W implies X c= W;
theorem :: CLASSES2:8
X is epsilon-transitive & X in Tarski-Class W implies X c=
Tarski-Class W;
theorem :: CLASSES2:9
W is Tarski implies On W = card W;
theorem :: CLASSES2:10
On Tarski-Class W = card Tarski-Class W;
theorem :: CLASSES2:11
W is Tarski & X in W implies card X in W;
theorem :: CLASSES2:12
X in Tarski-Class W implies card X in Tarski-Class W;
theorem :: CLASSES2:13
W is Tarski & x in card W implies x in W;
theorem :: CLASSES2:14
x in card Tarski-Class W implies x in Tarski-Class W;
theorem :: CLASSES2:15
W is Tarski & m in card W implies m in W;
theorem :: CLASSES2:16
m in card Tarski-Class W implies m in Tarski-Class W;
theorem :: CLASSES2:17
W is Tarski & m in W implies m c= W;
theorem :: CLASSES2:18
m in Tarski-Class W implies m c= Tarski-Class W;
theorem :: CLASSES2:19
W is Tarski implies card W is limit_ordinal;
theorem :: CLASSES2:20
W is Tarski & W <> {} implies card W <> 0 & card W <> {} & card W is
limit_ordinal;
theorem :: CLASSES2:21
card Tarski-Class W <> 0 & card Tarski-Class W <> {} & card
Tarski-Class W is limit_ordinal;
reserve f,g for Function,
L for Sequence,
F for Cardinal-Function;
theorem :: CLASSES2:22
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) implies Funcs(X,W) c= W;
theorem :: CLASSES2:23
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
implies Funcs(X,Tarski-Class W) c= Tarski-Class W;
theorem :: CLASSES2:24
dom L is limit_ordinal & (for A st A in dom L holds L.A = Rank A
) implies Rank dom L = Union L;
theorem :: CLASSES2:25
W is Tarski & A in On W implies card Rank A in card W & Rank A in W;
theorem :: CLASSES2:26
A in On Tarski-Class W implies card Rank A in card Tarski-Class W &
Rank A in Tarski-Class W;
theorem :: CLASSES2:27
W is Tarski implies Rank card W c= W;
theorem :: CLASSES2:28
Rank card Tarski-Class W c= Tarski-Class W;
theorem :: CLASSES2:29
W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W;
theorem :: CLASSES2:30
W is Tarski & W is epsilon-transitive implies W c= Rank card W;
theorem :: CLASSES2:31
W is Tarski & W is epsilon-transitive implies Rank card W = W;
theorem :: CLASSES2:32
W is Tarski & A in On W implies card Rank A c= card W;
theorem :: CLASSES2:33
A in On Tarski-Class W implies card Rank A c= card Tarski-Class W;
theorem :: CLASSES2:34
W is Tarski implies card W = card Rank card W;
theorem :: CLASSES2:35
card Tarski-Class W = card Rank card Tarski-Class W;
theorem :: CLASSES2:36
W is Tarski & X c= Rank card W implies X,Rank card W
are_equipotent or X in Rank card W;
theorem :: CLASSES2:37
X c= Rank card Tarski-Class W implies X,Rank card Tarski-Class W
are_equipotent or X in Rank card Tarski-Class W;
theorem :: CLASSES2:38
W is Tarski implies Rank card W is Tarski;
theorem :: CLASSES2:39
Rank card Tarski-Class W is Tarski;
theorem :: CLASSES2:40
X is epsilon-transitive & A in the_rank_of X implies ex Y st Y
in X & the_rank_of Y = A;
theorem :: CLASSES2:41
X is epsilon-transitive implies card the_rank_of X c= card X;
theorem :: CLASSES2:42
W is Tarski & X is epsilon-transitive & X in W implies X in Rank card W;
theorem :: CLASSES2:43
X is epsilon-transitive & X in Tarski-Class W implies X in Rank card
Tarski-Class W;
theorem :: CLASSES2:44
W is epsilon-transitive implies Rank card Tarski-Class W is_Tarski-Class_of W
;
theorem :: CLASSES2:45
W is epsilon-transitive implies Rank card Tarski-Class W = Tarski-Class W;
definition
let IT be set;
attr IT is universal means
:: CLASSES2:def 1
IT is epsilon-transitive & IT is Tarski;
end;
registration
cluster universal -> epsilon-transitive Tarski for set;
cluster epsilon-transitive Tarski -> universal for set;
end;
registration
cluster universal non empty for set;
end;
definition
mode Universe is universal non empty set;
end;
reserve U1,U2,U for Universe;
theorem :: CLASSES2:46
On U is Ordinal;
theorem :: CLASSES2:47
X is epsilon-transitive implies Tarski-Class X is universal;
theorem :: CLASSES2:48
Tarski-Class U is Universe;
registration
let U;
cluster On U -> ordinal;
cluster Tarski-Class U -> universal;
end;
theorem :: CLASSES2:49
Tarski-Class A is universal;
registration
let A;
cluster Tarski-Class A -> universal;
end;
theorem :: CLASSES2:50
U = Rank On U;
theorem :: CLASSES2:51
On U <> {} & On U is limit_ordinal;
theorem :: CLASSES2:52
U1 in U2 or U1 = U2 or U2 in U1;
theorem :: CLASSES2:53
U1 c= U2 or U2 in U1;
theorem :: CLASSES2:54
U1,U2 are_c=-comparable;
theorem :: CLASSES2:55
U1 \/ U2 is Universe & U1 /\ U2 is Universe;
theorem :: CLASSES2:56
{} in U;
theorem :: CLASSES2:57
x in U implies {x} in U;
theorem :: CLASSES2:58
x in U & y in U implies {x,y} in U & [x,y] in U;
theorem :: CLASSES2:59
X in U implies bool X in U & union X in U & meet X in U;
theorem :: CLASSES2:60
X in U & Y in U implies X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U
;
theorem :: CLASSES2:61
X in U & Y in U implies [:X,Y:] in U & Funcs(X,Y) in U;
reserve u,v for Element of U;
registration
let U1;
cluster non empty for Element of U1;
end;
definition
let U,u;
redefine func {u} -> Element of U;
redefine func bool u -> Element of U;
redefine func union u -> Element of U;
redefine func meet u -> Element of U;
let v;
redefine func {u,v} -> Element of U;
redefine func [u,v] -> Element of U;
redefine func u \/ v -> Element of U;
redefine func u /\ v -> Element of U;
redefine func u \ v -> Element of U;
redefine func u \+\ v -> Element of U;
redefine func [:u,v:] -> Element of U;
redefine func Funcs(u,v) -> Element of U;
end;
definition
func FinSETS -> Universe equals
:: CLASSES2:def 2
Tarski-Class {};
end;
theorem :: CLASSES2:62
card Rank omega = card omega;
theorem :: CLASSES2:63
Rank omega is Tarski;
theorem :: CLASSES2:64
FinSETS = Rank omega;
definition
func SETS -> Universe equals
:: CLASSES2:def 3
Tarski-Class FinSETS;
end;
registration
let X be set;
cluster the_transitive-closure_of X -> epsilon-transitive;
end;
registration
let X be epsilon-transitive set;
cluster Tarski-Class X -> epsilon-transitive;
end;
definition
let X be set;
func Universe_closure X -> Universe means
:: CLASSES2:def 4
X c= it & for Y being Universe st X c= Y holds it c= Y;
end;
definition
mode FinSet is Element of FinSETS;
mode Set is Element of SETS;
let A;
func UNIVERSE A -> set means
:: CLASSES2:def 5
ex L st it = last L & dom L = succ A & L.0 =
FinSETS & (for C st succ C in succ A holds L.succ C = Tarski-Class(L.C)) & for
C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = Universe_closure
Union(L|C);
end;
registration
let A;
cluster UNIVERSE A -> universal non empty;
end;
theorem :: CLASSES2:65
UNIVERSE {} = FinSETS;
theorem :: CLASSES2:66
UNIVERSE succ A = Tarski-Class UNIVERSE A;
theorem :: CLASSES2:67
UNIVERSE 1 = SETS;
theorem :: CLASSES2:68
A <> {} & A is limit_ordinal & dom L = A & (for B st B in A holds L.B
= UNIVERSE B) implies UNIVERSE A = Universe_closure Union L;
theorem :: CLASSES2:69
FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U;
theorem :: CLASSES2:70
A in B iff UNIVERSE A in UNIVERSE B;
theorem :: CLASSES2:71
UNIVERSE A = UNIVERSE B implies A = B;
theorem :: CLASSES2:72
A c= B iff UNIVERSE A c= UNIVERSE B;
reserve u,v for Element of Tarski-Class(X);
theorem :: CLASSES2:73
Tarski-Class(X,{}) in Tarski-Class(X,1) &
Tarski-Class(X,{}) <> Tarski-Class(X,1);