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