:: by Andrzej Kondracki

::

:: Received December 17, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

registration
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

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

definition

ex b_{1} being Function of omega,VAR st

for p being Element of omega holds b_{1} . p = x. (card p)

for b_{1}, b_{2} being Function of omega,VAR st ( for p being Element of omega holds b_{1} . p = x. (card p) ) & ( for p being Element of omega holds b_{2} . p = x. (card p) ) holds

b_{1} = b_{2}
end;

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 for p being Element of omega holds it . p = x. (card p);

ex b

for p being Element of omega holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines decode ZF_FUND1:def 2 :

for b_{1} being Function of omega,VAR holds

( b_{1} = decode iff for p being Element of omega holds b_{1} . p = x. (card p) );

for b

( b

definition

let v1 be Element of VAR ;

existence

ex b_{1} being Element of NAT st x. b_{1} = v1

for b_{1}, b_{2} being Element of NAT st x. b_{1} = v1 & x. b_{2} = v1 holds

b_{1} = b_{2}

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines x". ZF_FUND1:def 3 :

for v1 being Element of VAR

for b_{2} being Element of NAT holds

( b_{2} = x". v1 iff x. b_{2} = v1 );

for v1 being Element of VAR

for b

( b

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

:: deftheorem defines code ZF_FUND1:def 4 :

for A being Subset of VAR holds code A = (decode ") .: A;

for A being Subset of VAR holds code A = (decode ") .: A;

registration
end;

definition

let H be ZF-formula;

let E be non empty set ;

ex b_{1} being set st

for p being set holds

( p in b_{1} iff ex f being Function of VAR,E st

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )

for b_{1}, b_{2} being set st ( for p being set holds

( p in b_{1} 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_{2} iff ex f being Function of VAR,E st

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) holds

b_{1} = b_{2}

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

ex b

for p being set holds

( p in b

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )

proof end;

uniqueness for b

( p in b

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) & ( for p being set holds

( p in b

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Diagram ZF_FUND1:def 5 :

for H being ZF-formula

for E being non empty set

for b_{3} being set holds

( b_{3} = Diagram (H,E) iff for p being set holds

( p in b_{3} iff ex f being Function of VAR,E st

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) );

for H being ZF-formula

for E being non empty set

for b

( b

( p in b

( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) );

definition

let V be Universe;

let X be Subclass of V;

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

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;

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;

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;

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;

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

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

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

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

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

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

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

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;

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

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

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

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

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

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

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

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 )

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

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

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

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

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

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

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

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

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

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

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 )

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

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

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

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

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;

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

theorem :: ZF_FUND1:25

theorem :: ZF_FUND1:26

theorem :: ZF_FUND1:27

theorem :: ZF_FUND1:28

theorem :: ZF_FUND1:31

theorem :: ZF_FUND1:32

theorem :: ZF_FUND1:33

theorem :: ZF_FUND1:34

theorem :: ZF_FUND1:35

theorem :: ZF_FUND1:36

theorem :: ZF_FUND1:37