:: Tarski's Classes and Ranks
:: by Grzegorz Bancerek
::
:: Received March 23, 1990
:: Copyright (c) 1990-2016 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 FUNCT_1, TARSKI, ZFMISC_1, SETFAM_1, XBOOLE_0, CARD_1, SUBSET_1,
ORDINAL1, ORDINAL2, RELAT_1, FUNCT_2, CLASSES1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, CARD_1, ORDINAL1, MCART_1, ORDINAL2;
constructors SETFAM_1, MCART_1, WELLORD2, ORDINAL2, CARD_1, FUNCT_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, RELSET_1,
RELAT_1;
requirements SUBSET, BOOLE, NUMERALS;
begin
reserve W,X,Y,Z for set,
f,g for Function,
a,x,y,z for set;
definition
let B be set;
attr B is subset-closed means
:: CLASSES1:def 1
for X,Y holds X in B & Y c= X implies Y in B;
end;
definition
let B be set;
attr B is Tarski means
:: CLASSES1:def 2
B is subset-closed & (for X holds X in B implies bool X in B) &
for X holds X c= B implies X,B are_equipotent or X in B;
end;
definition
let A,B be set;
pred B is_Tarski-Class_of A means
:: CLASSES1:def 3
A in B & B is Tarski;
end;
definition
let A be set;
func Tarski-Class A -> set means
:: CLASSES1:def 4
it is_Tarski-Class_of A &
for D being set st D is_Tarski-Class_of A holds it c= D;
end;
registration
let A be set;
cluster Tarski-Class A -> non empty;
end;
theorem :: CLASSES1:1
W is Tarski iff W is subset-closed & (for X st X in W holds bool X in W) &
for X st X c= W & card X in card W holds X in W;
theorem :: CLASSES1:2
X in Tarski-Class X;
theorem :: CLASSES1:3
Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X;
theorem :: CLASSES1:4
Y in Tarski-Class X implies bool Y in Tarski-Class X;
theorem :: CLASSES1:5
Y c= Tarski-Class X implies
Y,Tarski-Class X are_equipotent or Y in Tarski-Class X;
theorem :: CLASSES1:6
Y c= Tarski-Class X & card Y in card Tarski-Class X implies
Y in Tarski-Class X;
reserve u,v for Element of Tarski-Class(X),
A,B,C for Ordinal,
L for Sequence;
definition
let X,A;
func Tarski-Class(X,A) -> set means
:: CLASSES1:def 5
ex L st it = last L & dom L = succ A & L.0 = { X } &
(for C st succ C in succ A holds
L.succ C = { u : ex v st v in L.C & u c= v } \/ { bool v : v in L.C } \/
bool(L.C) /\ Tarski-Class X) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = (union rng(L|C)) /\ Tarski-Class X;
end;
definition
let X,A;
redefine func Tarski-Class(X,A) -> Subset of Tarski-Class X;
end;
theorem :: CLASSES1:7
Tarski-Class(X,{}) = { X };
theorem :: CLASSES1:8
Tarski-Class(X,succ A) = { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X;
theorem :: CLASSES1:9
A <> {} & A is limit_ordinal implies
Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) };
theorem :: CLASSES1:10
Y in Tarski-Class(X,succ A) iff
Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
theorem :: CLASSES1:11
Y c= Z & Z in Tarski-Class(X,A) implies Y in Tarski-Class(X,succ A);
theorem :: CLASSES1:12
Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,succ A);
theorem :: CLASSES1:13
A <> {} & A is limit_ordinal implies
(x in Tarski-Class(X,A) iff ex B st B in A & x in Tarski-Class(X,B));
theorem :: CLASSES1:14
A <> {} & A is limit_ordinal & Y in Tarski-Class(X,A) &
(Z c= Y or Z = bool Y) implies Z in Tarski-Class(X,A);
theorem :: CLASSES1:15
Tarski-Class(X,A) c= Tarski-Class(X,succ A);
theorem :: CLASSES1:16
A c= B implies Tarski-Class(X,A) c= Tarski-Class(X,B);
theorem :: CLASSES1:17
ex A st Tarski-Class(X,A) = Tarski-Class(X,succ A);
theorem :: CLASSES1:18
Tarski-Class(X,A) = Tarski-Class(X,succ A) implies
Tarski-Class(X,A) = Tarski-Class X;
theorem :: CLASSES1:19
ex A st Tarski-Class(X,A) = Tarski-Class X;
theorem :: CLASSES1:20
ex A st Tarski-Class(X,A) = Tarski-Class X &
for B st B in A holds Tarski-Class(X,B) <> Tarski-Class X;
theorem :: CLASSES1:21
Y <> X & Y in Tarski-Class X implies
ex A st not Y in Tarski-Class(X,A) & Y in Tarski-Class(X,succ A);
theorem :: CLASSES1:22
X is epsilon-transitive implies
for A st A <> {} holds Tarski-Class(X,A) is epsilon-transitive;
theorem :: CLASSES1:23
X is epsilon-transitive implies Tarski-Class X is epsilon-transitive;
theorem :: CLASSES1:24
Y in Tarski-Class X implies card Y in card Tarski-Class X;
theorem :: CLASSES1:25
Y in Tarski-Class X implies not Y,Tarski-Class X are_equipotent;
theorem :: CLASSES1:26
(x in Tarski-Class X implies {x} in Tarski-Class X) &
(x in Tarski-Class X & y in Tarski-Class X implies
{x,y} in Tarski-Class X);
theorem :: CLASSES1:27
x in Tarski-Class X & y in Tarski-Class X implies [x,y] in Tarski-Class X;
theorem :: CLASSES1:28
Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X;
definition
let A;
func Rank(A) -> set means
:: CLASSES1:def 6
ex L st it = last L & dom L = succ A & L.0 = {} &
(for C st succ C in succ A holds L.succ C = bool(L.C)) &
for C st C in succ A & C <> 0 & C is limit_ordinal
holds L.C = union rng(L|C);
end;
theorem :: CLASSES1:29
Rank {} = {};
theorem :: CLASSES1:30
Rank succ A = bool Rank A;
theorem :: CLASSES1:31
A <> {} & A is limit_ordinal implies
for x holds x in Rank A iff ex B st B in A & x in Rank B;
theorem :: CLASSES1:32
X c= Rank A iff X in Rank succ A;
registration
let A;
cluster Rank A -> epsilon-transitive;
end;
theorem :: CLASSES1:33
Rank A c= Rank succ A;
theorem :: CLASSES1:34
union Rank A c= Rank A;
theorem :: CLASSES1:35
X in Rank A implies union X in Rank A;
theorem :: CLASSES1:36
A in B iff Rank A in Rank B;
theorem :: CLASSES1:37
A c= B iff Rank A c= Rank B;
theorem :: CLASSES1:38
A c= Rank A;
theorem :: CLASSES1:39
for A,X st X in Rank A holds
not X,Rank A are_equipotent & card X in card Rank A;
theorem :: CLASSES1:40
X c= Rank A iff bool X c= Rank succ A;
theorem :: CLASSES1:41
X c= Y & Y in Rank A implies X in Rank A;
theorem :: CLASSES1:42
X in Rank A iff bool X in Rank succ A;
theorem :: CLASSES1:43
x in Rank A iff {x} in Rank succ A;
theorem :: CLASSES1:44
x in Rank A & y in Rank A iff {x,y} in Rank succ A;
theorem :: CLASSES1:45
x in Rank A & y in Rank A iff [x,y] in Rank succ succ A;
theorem :: CLASSES1:46
X is epsilon-transitive &
Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X implies
Tarski-Class X c= Rank A;
theorem :: CLASSES1:47
X is epsilon-transitive implies ex A st Tarski-Class X c= Rank A;
theorem :: CLASSES1:48
X is epsilon-transitive implies union X c= X;
theorem :: CLASSES1:49
X is epsilon-transitive & Y is epsilon-transitive implies
X \/ Y is epsilon-transitive;
theorem :: CLASSES1:50
X is epsilon-transitive & Y is epsilon-transitive implies
X /\ Y is epsilon-transitive;
reserve n for Element of omega;
definition
let X;
func the_transitive-closure_of X -> set means
:: CLASSES1:def 7
for x being object
holds x in it iff ex f,n st x in f.n & dom f = omega & f.0 = X &
for k being Nat holds f.(succ k) = union(f.k);
end;
registration let X;
cluster the_transitive-closure_of X -> epsilon-transitive;
end;
theorem :: CLASSES1:51
the_transitive-closure_of X is epsilon-transitive;
theorem :: CLASSES1:52
X c= the_transitive-closure_of X;
theorem :: CLASSES1:53
X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y;
theorem :: CLASSES1:54
(for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y &
Y is epsilon-transitive implies the_transitive-closure_of X = Y;
theorem :: CLASSES1:55
X is epsilon-transitive implies the_transitive-closure_of X = X;
theorem :: CLASSES1:56
the_transitive-closure_of {} = {};
theorem :: CLASSES1:57
the_transitive-closure_of A = A;
theorem :: CLASSES1:58
X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y;
theorem :: CLASSES1:59
the_transitive-closure_of the_transitive-closure_of X =
the_transitive-closure_of X;
theorem :: CLASSES1:60
the_transitive-closure_of (X \/ Y) =
the_transitive-closure_of X \/ the_transitive-closure_of Y;
theorem :: CLASSES1:61
the_transitive-closure_of (X /\ Y) c=
the_transitive-closure_of X /\ the_transitive-closure_of Y;
theorem :: CLASSES1:62
ex A st X c= Rank A;
definition
let x be object;
func the_rank_of x -> Ordinal means
:: CLASSES1:def 8
x in Rank succ it & for B st x in Rank succ B holds it c= B;
end;
definition
let X;
redefine func the_rank_of X means
:: CLASSES1:def 9
X c= Rank it & for B st X c= Rank B holds it c= B;
end;
theorem :: CLASSES1:63
the_rank_of bool X = succ the_rank_of X;
theorem :: CLASSES1:64
the_rank_of Rank A = A;
theorem :: CLASSES1:65
X c= Rank A iff the_rank_of X c= A;
theorem :: CLASSES1:66
X in Rank A iff the_rank_of X in A;
theorem :: CLASSES1:67
X c= Y implies the_rank_of X c= the_rank_of Y;
theorem :: CLASSES1:68
X in Y implies the_rank_of X in the_rank_of Y;
theorem :: CLASSES1:69
the_rank_of X c= A iff for Y st Y in X holds the_rank_of Y in A;
theorem :: CLASSES1:70
A c= the_rank_of X iff for B st B in A ex Y st Y in X & B c= the_rank_of Y;
theorem :: CLASSES1:71
the_rank_of X = {} iff X = {};
theorem :: CLASSES1:72
the_rank_of X = succ A implies ex Y st Y in X & the_rank_of Y = A;
theorem :: CLASSES1:73
the_rank_of A = A;
theorem :: CLASSES1:74
the_rank_of Tarski-Class X <> {} &
the_rank_of Tarski-Class X is limit_ordinal;
begin :: Addenda
:: from ZFREFLE1, 2007.03, A.T.
reserve e,u for set;
scheme :: CLASSES1:sch 1
NonUniqFuncEx { X() -> set, P[object,object] }:
ex f being Function st dom f = X() &
for e being object st e in X() holds P[e,f.e]
provided
for e being object st e in X() ex u being object st P[e,u];
:: from RFINSEQ, 2008.10.10, A.T.
definition
let F,G be Relation;
pred F,G are_fiberwise_equipotent means
:: CLASSES1:def 10
for x be object holds card Coim(F,x) = card Coim(G,x);
reflexivity;
symmetry;
end;
theorem :: CLASSES1:75
for F,G be Function st F,G are_fiberwise_equipotent holds rng F = rng G;
theorem :: CLASSES1:76
for F,G,H be Function
st F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent holds
G,H are_fiberwise_equipotent;
theorem :: CLASSES1:77
for F,G be Function holds F,G are_fiberwise_equipotent iff
ex H be Function st dom H = dom F & rng H = dom G & H is one-to-one & F = G*H
;
theorem :: CLASSES1:78
for F,G be Function holds
F,G are_fiberwise_equipotent iff for X be set holds card (F"X) = card (G"X);
theorem :: CLASSES1:79
for D be non empty set, F,G be Function st rng F c= D & rng G c= D &
for d be Element of D holds card Coim(F,d) = card Coim(G,d)
holds F,G are_fiberwise_equipotent;
theorem :: CLASSES1:80
for F,G be Function st dom F = dom G holds
F,G are_fiberwise_equipotent iff ex P be Permutation of dom F st F = G*P;
theorem :: CLASSES1:81
for F,G be Function
st F,G are_fiberwise_equipotent holds card dom F = card dom G;
:: from CIRCCOMB, 2009.01.26, A.T.
theorem :: CLASSES1:82
for f being set, p being Relation
for x being set st x in rng p holds the_rank_of x in the_rank_of [p,f];
:: 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;
scheme :: CLASSES1:sch 2
LambdaAB { A, B()->set, F(Element of B())->set } :
ex f being Function st
dom f = A() & for x being Element of B() st x in A() holds f.x = F(x);
theorem :: CLASSES1:84
for x,y being set holds the_rank_of x in the_rank_of [x,y] &
the_rank_of y in the_rank_of [x,y];