:: Mostowski's Fundamental Operations - Part I
:: by Andrzej Kondracki
::
:: Received December 17, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

registration
let V be Universe;
cluster Relation-like for Element of V;
existence
 ex b1 being Element of V st b1 is Relation-like
proofend;
end;

definition
canceled;
let V be Universe;
let x, y be Element of V;
:: original:(#)
redefine funcx (#) y ->  Relation-like Element of V;
coherence
 x (#) y is Relation-like Element of V
proofend;
end;

:: deftheorem  ZF_FUND1:def_1_:_
canceled;

definition
func decode  ->  Function of omega,VAR means :Def2: :: ZF_FUND1:def 2
 for p being Element of omega holds it . p = x. (card p);
existence
 ex b1 being Function of omega,VAR st
for p being Element of omega holds b1 . p = x. (card p)
proofend;
uniqueness
 for b1, b2 being Function of omega,VAR st ( for p being Element of omega holds b1 . p = x. (card p) ) & ( for p being Element of omega holds b2 . p = x. (card p) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines decode ZF_FUND1:def_2_:_
 for b1 being Function of omega,VAR holds
( b1 = decode iff for p being Element of omega holds b1 . p = x. (card p) );

definition
let v1 be Element of VAR ;
func x". v1 ->  Element of NAT  means :Def3: :: ZF_FUND1:def 3
 x. it = v1;
existence
 ex b1 being Element of NAT st x. b1 = v1
proofend;
uniqueness
 for b1, b2 being Element of NAT st x. b1 = v1 & x. b2 = v1 holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines x". ZF_FUND1:def_3_:_
 for v1 being Element of VAR
for b2 being Element of NAT holds
( b2 = x". v1 iff x. b2 = v1 );

Lm1:  ( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega )
proofend;

definition
let A be Subset of VAR;
func code A ->  Subset of omega equals :: ZF_FUND1:def 4
(decode ") .: A;
coherence
 (decode ") .: A is Subset of omega by Lm1, RELAT_1:111;
end;

:: deftheorem  defines code ZF_FUND1:def_4_:_
 for A being Subset of VAR holds code A = (decode ") .: A;

registration
let A be finite Subset of VAR;
cluster code A ->  finite ;
coherence
 code A is finite ;
end;

definition
let H be ZF-formula;
let E be non empty set ;
func Diagram (H,E) ->  set  means :Def5: :: ZF_FUND1:def 5
 for p being set holds
( p in it iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) );
existence
 ex b1 being set st
for p being set holds
( p in b1 iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for p being set holds
( p in b1 iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) & ( for p being set holds
( p in b2 iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Diagram ZF_FUND1:def_5_:_
 for H being ZF-formula
for E being non empty set
for b3 being set holds
( b3 = Diagram (H,E) iff for p being set holds
( p in b3 iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) );

definition
let V be Universe;
let X be Subclass of V;
attrX is closed_wrt_A1  means :Def6: :: ZF_FUND1:def 6
 for a being Element of V st a in X holds
{  {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a )  }  in X;
attrX is closed_wrt_A2  means :Def7: :: ZF_FUND1:def 7
 for a, b being Element of V st a in X & b in X holds
{a,b} in X;
attrX is closed_wrt_A3  means :Def8: :: ZF_FUND1:def 8
 for a being Element of V st a in X holds
union a in X;
attrX is closed_wrt_A4  means :Def9: :: ZF_FUND1:def 9
 for a, b being Element of V st a in X & b in X holds
{  {[x,y]} where x, y is Element of V : ( x in a & y in b )  }  in X;
attrX is closed_wrt_A5  means :Def10: :: ZF_FUND1:def 10
 for a, b being Element of V st a in X & b in X holds
{  (x \/ y) where x, y is Element of V : ( x in a & y in b )  }  in X;
attrX is closed_wrt_A6  means :Def11: :: ZF_FUND1:def 11
 for a, b being Element of V st a in X & b in X holds
{  (x \ y) where x, y is Element of V : ( x in a & y in b )  }  in X;
attrX is closed_wrt_A7  means :Def12: :: ZF_FUND1:def 12
 for a, b being Element of V st a in X & b in X holds
{  (x (#) y) where x, y is Element of V : ( x in a & y in b )  }  in X;
end;

:: deftheorem Def6 defines closed_wrt_A1 ZF_FUND1:def_6_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1 iff for a being Element of V st a in X holds
{  {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a )  }  in X );

:: deftheorem Def7 defines closed_wrt_A2 ZF_FUND1:def_7_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A2 iff for a, b being Element of V st a in X & b in X holds
{a,b} in X );

:: deftheorem Def8 defines closed_wrt_A3 ZF_FUND1:def_8_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A3 iff for a being Element of V st a in X holds
union a in X );

:: deftheorem Def9 defines closed_wrt_A4 ZF_FUND1:def_9_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A4 iff for a, b being Element of V st a in X & b in X holds
{  {[x,y]} where x, y is Element of V : ( x in a & y in b )  }  in X );

:: deftheorem Def10 defines closed_wrt_A5 ZF_FUND1:def_10_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A5 iff for a, b being Element of V st a in X & b in X holds
{  (x \/ y) where x, y is Element of V : ( x in a & y in b )  }  in X );

:: deftheorem Def11 defines closed_wrt_A6 ZF_FUND1:def_11_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A6 iff for a, b being Element of V st a in X & b in X holds
{  (x \ y) where x, y is Element of V : ( x in a & y in b )  }  in X );

:: deftheorem Def12 defines closed_wrt_A7 ZF_FUND1:def_12_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A7 iff for a, b being Element of V st a in X & b in X holds
{  (x (#) y) where x, y is Element of V : ( x in a & y in b )  }  in X );

definition
let V be Universe;
let X be Subclass of V;
attrX is closed_wrt_A1-A7  means :Def13: :: ZF_FUND1:def 13
( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 );
end;

:: deftheorem Def13 defines closed_wrt_A1-A7 ZF_FUND1:def_13_:_
 for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1-A7 iff ( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 ) );

Lm2:  for A being Element of omega holds A = x". (x. (card A))
proofend;

Lm3:  for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR,E holds
( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega )
proofend;

Lm4:  for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 )
proofend;

Lm5:  for p being set
for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) )
proofend;

Lm6:  for v1 being Element of VAR holds code {v1} = {(x". v1)}
proofend;

Lm7:  for v1, v2 being Element of VAR holds code {v1,v2} = {(x". v1),(x". v2)}
proofend;

Lm8:  for A being finite Subset of VAR holds A, code A are_equipotent
proofend;

Lm9:  for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode) | (code (Free H))) . (x". v1) = f . v1
proofend;

Lm10:  for E being non empty set
for H being ZF-formula
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)
proofend;

Lm11:  for p being set
for fs being finite Subset of omega
for E being non empty set st p in Funcs (fs,E) holds
ex f being Function of VAR,E st p = (f * decode) | fs
proofend;

theorem Th1: :: ZF_FUND1:1
for V being Universe
for X being Subclass of V
for o, A being set holds
( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) )
proofend;

theorem Th2: :: ZF_FUND1:2
for V being Universe
for X being Subclass of V
for o, A being set st X is closed_wrt_A1-A7 holds
( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) )
proofend;

theorem Th3: :: ZF_FUND1:3
for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X
proofend;

theorem Th4: :: ZF_FUND1:4
for V being Universe
for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
proofend;

theorem Th5: :: ZF_FUND1:5
for V being Universe
for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
A /\ B in X
proofend;

theorem Th6: :: ZF_FUND1:6
for V being Universe
for X being Subclass of V
for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds
( {o,p} in X & [o,p] in X )
proofend;

theorem Th7: :: ZF_FUND1:7
for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
omega c= X
proofend;

theorem Th8: :: ZF_FUND1:8
for V being Universe
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds
Funcs (fs,omega) c= X
proofend;

theorem Th9: :: ZF_FUND1:9
for V being Universe
for a being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs (fs,a) in X
proofend;

theorem Th10: :: ZF_FUND1:10
for V being Universe
for a, b being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds
{  (a (#) x) where x is Element of V : x in b  }  in X
proofend;

Lm12:  for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
n in X
proofend;

Lm13:  for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
( 0-element_of V in X & 1-element_of V in X )
proofend;

theorem Th11: :: ZF_FUND1:11
for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds
{  x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b )  }  in X
proofend;

theorem Th12: :: ZF_FUND1:12
for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds
{  ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b )  }  in X
proofend;

theorem Th13: :: ZF_FUND1:13
for V being Universe
for X being Subclass of V
for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) holds
B in X
proofend;

theorem Th14: :: ZF_FUND1:14
for V being Universe
for y being Element of V
for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds
y in X
proofend;

theorem Th15: :: ZF_FUND1:15
for V being Universe
for a, y being Element of V
for X being Subclass of V
for fs being finite Subset of omega
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{  ({[n,x]} \/ y) where x is Element of V : x in a  }  in X
proofend;

theorem :: ZF_FUND1:16
for V being Universe
for a, y, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st 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 holds
{  x where x is Element of V : ( x in a & {[n,x]} \/ y in b )  }  in X
proofend;

Lm14:  for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]}
proofend;

theorem Th17: :: ZF_FUND1:17
for V being Universe
for a being Element of V
for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds
{  {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a  }  in X
proofend;

Lm15:  for p, r, o, q, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]}
proofend;

Lm16:  for o, q being set
for g being Function holds
( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} )
proofend;

theorem Th18: :: ZF_FUND1:18
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 &amp; E in X holds
for v1, v2 being Element of VAR holds
( Diagram ((v1 '=' v2),E) in X &amp; Diagram ((v1 'in' v2),E) in X )
proofend;

theorem Th19: :: ZF_FUND1:19
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 &amp; E in X holds
for H being ZF-formula st Diagram (H,E) in X holds
Diagram (('not' H),E) in X
proofend;

theorem Th20: :: ZF_FUND1:20
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 &amp; E in X holds
for H, H9 being ZF-formula st Diagram (H,E) in X &amp; Diagram (H9,E) in X holds
Diagram ((H '&amp;' H9),E) in X
proofend;

theorem Th21: :: ZF_FUND1:21
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 &amp; E in X holds
for H being ZF-formula
for v1 being Element of VAR st Diagram (H,E) in X holds
Diagram ((All (v1,H)),E) in X
proofend;

theorem :: ZF_FUND1:22
for V being Universe
for X being Subclass of V
for E being non empty set
for H being ZF-formula st X is closed_wrt_A1-A7 &amp; E in X holds
Diagram (H,E) in X
proofend;

:: Auxiliary theorems
theorem :: ZF_FUND1:23
for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
( n in X &amp; 0-element_of V in X &amp; 1-element_of V in X ) by Lm12, Lm13;

theorem :: ZF_FUND1:24
for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} by Lm14;

theorem :: ZF_FUND1:25
for p, r, o, q, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} by Lm15;

theorem :: ZF_FUND1:26
for v1, v2 being Element of VAR holds
( code {v1} = {(x". v1)} &amp; code {v1,v2} = {(x". v1),(x". v2)} ) by Lm6, Lm7;

theorem :: ZF_FUND1:27
for o, q being set
for f being Function holds
( dom f = {o,q} iff f = {[o,(f . o)],[q,(f . q)]} ) by Lm16;

theorem :: ZF_FUND1:28
( dom decode = omega &amp; rng decode = VAR &amp; decode is one-to-one &amp; decode " is one-to-one &amp; dom (decode ") = VAR &amp; rng (decode ") = omega ) by Lm1;

theorem :: ZF_FUND1:29
for A being finite Subset of VAR holds A, code A are_equipotent by Lm8;

theorem :: ZF_FUND1:30
for A being Element of omega holds A = x". (x. (card A)) by Lm2;

theorem :: ZF_FUND1:31
for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR,E holds
( dom ((f * decode) | fs) = fs &amp; rng ((f * decode) | fs) c= E &amp; (f * decode) | fs in Funcs (fs,E) &amp; dom (f * decode) = omega ) by Lm3;

theorem :: ZF_FUND1:32
for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 &amp; (decode ") . v1 = x". v1 &amp; (f * decode) . (x". v1) = f . v1 ) by Lm4;

theorem :: ZF_FUND1:33
for p being set
for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A &amp; p = x". v1 ) ) by Lm5;

theorem :: ZF_FUND1:34
for A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) &amp; code (A \ B) = (code A) \ (code B) ) by Lm1, FUNCT_1:64, RELAT_1:120;

theorem :: ZF_FUND1:35
for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode) | (code (Free H))) . (x". v1) = f . v1 by Lm9;

theorem :: ZF_FUND1:36
for E being non empty set
for H being ZF-formula
for f, g being Function of VAR,E st (f * decode) | (code (Free H)) = (g * decode) | (code (Free H)) &amp; f in St (H,E) holds
g in St (H,E) by Lm10;

theorem :: ZF_FUND1:37
for p being set
for fs being finite Subset of omega
for E being non empty set st p in Funcs (fs,E) holds
ex f being Function of VAR,E st p = (f * decode) | fs by Lm11;