:: Mostowski's Fundamental Operations - Part I :: by Andrzej Kondracki :: :: Received December 17, 1990 :: Copyright (c) 1990-2021 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 CLASSES2, SUBSET_1, ZF_REFLE, ORDINAL1, FINSET_1, FUNCT_1, XBOOLE_0, ZF_LANG, NUMBERS, VALUED_1, RELAT_1, TARSKI, ZFMISC_1, MCART_1, CARD_1, XXREAL_0, NAT_1, ARYTM_3, ZF_MODEL, FUNCT_2, ORDINAL4, FUNCOP_1, XBOOLEAN, BVFUNC_2, ZF_FUND1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, ORDINAL4, CARD_1, FINSET_1, RELAT_1, CLASSES2, ZF_REFLE, ZF_LANG, ZF_MODEL, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MCART_1, FUNCOP_1, XXREAL_0; constructors PARTFUN1, WELLORD2, DOMAIN_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, CLASSES1, ORDINAL4, ZF_MODEL, RELSET_1, NUMBERS; registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, CARD_1, CLASSES2, ZF_LANG, ZF_LANG1, RELAT_1, XTUPLE_0; requirements NUMERALS, SUBSET, BOOLE; begin reserve V for Universe, a,b,x,y,z,x9,y9 for Element of V, X for Subclass of V, o,p,q,r,s,t,u,a1,a2,a3,A,B,C,D for set, K,L,M for Ordinal, n for Element of omega, fs for finite Subset of omega, e,g,h for Function, E for non empty set, f for Function of VAR,E, k,k1 for Element of NAT, v1,v2,v3 for Element of VAR, H,H9 for ZF-formula; registration let V; cluster Relation-like for Element of V; end; definition ::$CD let V,x,y; redefine func x(#)y -> Relation-like Element of V; end; definition func decode -> Function of omega,VAR means :: ZF_FUND1:def 2 for p being Element of omega holds it.p = x.card p; end; definition let v1; func x".v1 -> Element of NAT means :: ZF_FUND1:def 3 x.it=v1; end; definition let A be Subset of VAR; func code A -> Subset of omega equals :: ZF_FUND1:def 4 (decode").:A; end; registration let A be finite Subset of VAR; cluster code A -> finite; end; definition let H,E; func Diagram(H,E) -> set means :: ZF_FUND1:def 5 p in it iff ex f st p=(f*decode)|code Free(H) & f in St(H,E); end; definition let V,X; attr X is closed_wrt_A1 means :: ZF_FUND1:def 6 for a st a in X holds {{[0-element_of(V ),x],[1-element_of(V),y]}: x in y & x in a & y in a} in X; attr X is closed_wrt_A2 means :: ZF_FUND1:def 7 for a,b st a in X & b in X holds {a,b} in X; attr X is closed_wrt_A3 means :: ZF_FUND1:def 8 for a st a in X holds union a in X; attr X is closed_wrt_A4 means :: ZF_FUND1:def 9 for a,b st a in X & b in X holds {{[x,y ]}: x in a & y in b} in X; attr X is closed_wrt_A5 means :: ZF_FUND1:def 10 for a,b st a in X & b in X holds {x \/ y: x in a & y in b} in X; attr X is closed_wrt_A6 means :: ZF_FUND1:def 11 for a,b st a in X & b in X holds {x\y: x in a & y in b} in X; attr X is closed_wrt_A7 means :: ZF_FUND1:def 12 for a,b st a in X & b in X holds {x(#) y: x in a & y in b} in X; end; definition let V,X; attr X is closed_wrt_A1-A7 means :: ZF_FUND1:def 13 X is closed_wrt_A1 closed_wrt_A2 closed_wrt_A3 closed_wrt_A4 closed_wrt_A5 closed_wrt_A6 closed_wrt_A7; end; theorem :: ZF_FUND1:1 X c= V & (o in X implies o is Element of V) & (o in A & A in X implies o is Element of V); theorem :: ZF_FUND1:2 X is closed_wrt_A1-A7 implies (o in X iff {o} in X) & (A in X implies union A in X); theorem :: ZF_FUND1:3 X is closed_wrt_A1-A7 implies {} in X; theorem :: ZF_FUND1:4 X is closed_wrt_A1-A7 & A in X & B in X implies A \/ B in X & A\B in X & A(#)B in X; theorem :: ZF_FUND1:5 X is closed_wrt_A1-A7 & A in X & B in X implies A/\B in X; theorem :: ZF_FUND1:6 X is closed_wrt_A1-A7 & o in X & p in X implies {o,p} in X & [o,p ] in X; theorem :: ZF_FUND1:7 X is closed_wrt_A1-A7 implies omega c= X; theorem :: ZF_FUND1:8 X is closed_wrt_A1-A7 implies Funcs(fs,omega) c= X; theorem :: ZF_FUND1:9 X is closed_wrt_A1-A7 & a in X implies Funcs(fs,a) in X; theorem :: ZF_FUND1:10 X is closed_wrt_A1-A7 & a in Funcs(fs,omega) & b in X implies {a(#)x: x in b} in X; theorem :: ZF_FUND1:11 X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs( fs,a) implies {x: x in Funcs(fs\{n},a) & ex u st {[n,u]} \/ x in b} in X; theorem :: ZF_FUND1:12 for n st X is closed_wrt_A1-A7 & a in X & b in X holds {{[n,x]} \/ y: x in a & y in b} in X; theorem :: ZF_FUND1:13 (X is closed_wrt_A1-A7 & B is finite & for o st o in B holds o in X) implies B in X; theorem :: ZF_FUND1:14 X is closed_wrt_A1-A7 & A c= X & y in Funcs(fs,A) implies y in X; theorem :: ZF_FUND1:15 for n st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs(fs ,a) holds {{[n,x]} \/ y: x in a} in X; theorem :: ZF_FUND1:16 X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs(fs, a) & b c= Funcs(fs \/ {n},a) & b in X implies {x: x in a & {[n,x]} \/ y in b} in X; theorem :: ZF_FUND1:17 X is closed_wrt_A1-A7 & a in X implies {{[0-element_of(V),x], [ 1-element_of(V),x]} : x in a} in X; theorem :: ZF_FUND1:18 X is closed_wrt_A1-A7 & E in X implies for v1,v2 holds Diagram( v1 '=' v2,E) in X & Diagram(v1 'in' v2,E) in X; theorem :: ZF_FUND1:19 X is closed_wrt_A1-A7 & E in X implies for H st Diagram(H,E) in X holds Diagram('not' H,E) in X; theorem :: ZF_FUND1:20 X is closed_wrt_A1-A7 & E in X implies for H,H9 st Diagram(H,E) in X & Diagram(H9,E) in X holds Diagram(H '&' H9,E) in X; theorem :: ZF_FUND1:21 X is closed_wrt_A1-A7 & E in X implies for H,v1 st Diagram(H,E) in X holds Diagram(All(v1,H),E) in X; theorem :: ZF_FUND1:22 X is closed_wrt_A1-A7 & E in X implies Diagram(H,E) in X; :: Auxiliary theorems theorem :: ZF_FUND1:23 X is closed_wrt_A1-A7 implies n in X & 0-element_of(V) in X & 1-element_of(V) in X; theorem :: ZF_FUND1:24 {[o,p],[p,p]}(#){[p,q]}={[o,q],[p,q]}; theorem :: ZF_FUND1:25 p<>r implies {[o,p],[q,r]}(#){[p,s],[r,t]}={[o,s],[q,t]}; theorem :: ZF_FUND1:26 code {v1} = { x".v1} & code {v1,v2} = { x".v1, x".v2}; theorem :: ZF_FUND1:27 for f being Function holds dom f={o,q} iff f={[o,f.o],[q,f.q]}; theorem :: ZF_FUND1:28 dom decode = omega & rng decode = VAR & decode is one-to-one & decode" is one-to-one & dom(decode") = VAR & rng(decode") = omega; theorem :: ZF_FUND1:29 for A being finite Subset of VAR holds A,code A are_equipotent; theorem :: ZF_FUND1:30 for A being Element of omega holds A = x".x.card A; theorem :: ZF_FUND1:31 dom((f*decode)|fs)=fs & rng((f*decode)|fs) c= E & (f*decode)|fs in Funcs(fs,E) & dom(f*decode)=omega; theorem :: ZF_FUND1:32 decode.(x".v1)=v1 & (decode").v1= x".v1 & (f*decode).(x".v1)=f.v1; theorem :: ZF_FUND1:33 for A being finite Subset of VAR holds p in code A iff ex v1 st v1 in A & p= x".v1; theorem :: ZF_FUND1:34 for A,B being finite Subset of VAR holds code(A \/ B)=code A \/ code B & code(A\B)=(code A)\(code B); theorem :: ZF_FUND1:35 v1 in Free H implies ((f*decode)|code Free H).( x".v1)=f.v1; theorem :: ZF_FUND1:36 for f,g being Function of VAR,E st (f*decode)|code Free H=(g*decode)| code Free H & f in St(H,E) holds g in St(H,E); theorem :: ZF_FUND1:37 p in Funcs(fs,E) implies ex f st p=(f*decode)|fs;