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

registration

let V be Universe;

cluster Relation-like for Element of V;

existence
ex b₁ being Element of V st b₁ is Relation-like

proof end;

end;

definition

let V be Universe;
let x, y be Element of V;
:: original: (#)
redefine func x (#) y -> Relation-like Element of V;
coherence
x (#) y is Relation-like Element of V

proof end;

end;

:: deftheorem ZF_FUND1:def 1 :
canceled;

definition

func decode -> Function of omega,VAR means :Def1: :: ZF_FUND1:def 2
for p being Element of omega holds it . p = x. (card p);

existence
ex b₁ being Function of omega,VAR st
for p being Element of omega holds b₁ . p = x. (card p)

proof end;

uniqueness
for b₁, b₂ being Function of omega,VAR st ( for p being Element of omega holds b₁ . p = x. (card p) ) & ( for p being Element of omega holds b₂ . p = x. (card p) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines decode ZF_FUND1:def 2 :
for b₁ being Function of omega,VAR holds
( b₁ = decode iff for p being Element of omega holds b₁ . p = x. (card p) );

definition

let v1 be Element of VAR ;

func x". v1 -> Element of NAT means :Def2: :: ZF_FUND1:def 3
x. it = v1;

existence
ex b₁ being Element of NAT st x. b₁ = v1

proof end;

uniqueness
for b₁, b₂ being Element of NAT st x. b₁ = v1 & x. b₂ = v1 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines x". ZF_FUND1:def 3 :
for v1 being Element of VAR
for b₂ being Element of NAT holds
( b₂ = x". v1 iff x. b₂ = v1 );

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

proof end;

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 :Def4: :: 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 b₁ being set st
for p being set holds
( p in b₁ iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for p being set holds
( p in b₁ 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 b₂ iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Diagram ZF_FUND1:def 5 :
for H being ZF-formula
for E being non empty set
for b₃ being set holds
( b₃ = Diagram (H,E) iff for p being set holds
( p in b₃ 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;

attr X is closed_wrt_A1 means :: 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;

attr X is closed_wrt_A2 means :: ZF_FUND1:def 7
for a, b being Element of V 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 being Element of V st a in X holds
union a in X;

attr X is closed_wrt_A4 means :: 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;

attr X is closed_wrt_A5 means :: 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;

attr X is closed_wrt_A6 means :: 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;

attr X is closed_wrt_A7 means :: 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 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 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 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 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 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 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 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;

attr X is closed_wrt_A1-A7 means :: 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 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))
by Def2;

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 )

proof end;

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 )

proof end;

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 ) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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 ) )

proof end;

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 ) )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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
by Th7, TARSKI:def 3;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem :: ZF_FUND1:16

for V being Universe
for a, b, y 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 & E in X holds
for v1, v2 being Element of VAR holds
( Diagram ((v1 '=' v2),E) in X & Diagram ((v1 'in' v2),E) in X )

proof end;

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 & E in X holds
for H being ZF-formula st Diagram (H,E) in X holds
Diagram (('not' H),E) in X

proof end;

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 & E in X holds
for H, H9 being ZF-formula st Diagram (H,E) in X & Diagram (H9,E) in X holds
Diagram ((H '&' H9),E) in X

proof end;

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 & 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

proof end;

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 & E in X holds
Diagram (H,E) in X

proof end;

:: 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 & 0-element_of V in X & 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 o, p, q, r, 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)} & 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 & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & 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 & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & 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 & (decode ") . v1 = x". v1 & (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 & 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) & 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)) & 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;