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