:: ZF_FUND1 semantic presentation

definition

let A, B be set ;
func A (#) B -> set means :Def1: :: ZF_FUND1:def 1
for p being set holds
( p in it iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines (#) ZF_FUND1:def 1 :

definition

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

proof end;

end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines decode ZF_FUND1:def 2 :

definition

let v1 be Element of VAR ;
func x". v1 -> Nat means :Def3: :: ZF_FUND1:def 3
x. it = v1;
existence

proof end;

uniqueness

proof end;

end;

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

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 finite Subset of VAR ;
func code A -> finite Subset of omega equals :: ZF_FUND1:def 4
(decode " ) .: A;
coherence by Lm1, RELAT_1:144;

end;

:: deftheorem defines code ZF_FUND1:def 4 :

definition

let H be ZF-formula;
:: original: Free
redefine func Free H -> finite Subset of VAR ;
coherence by ZF_LANG1:85;

end;

definition

let n be Element of omega ;
:: original: {
redefine func {n} -> finite Subset of omega ;
coherence by ZFMISC_1:37;

end;

definition

let v1 be Element of VAR ;
:: original: {
redefine func {v1} -> finite Subset of VAR ;
coherence by ZFMISC_1:37;
let v2 be Element of VAR ;
:: original: {
redefine func {v1,v2} -> finite Subset of VAR ;
coherence by ZFMISC_1:38;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Diagram ZF_FUND1:def 5 :

definition

let V be Universe;
let X be Subclass of V;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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 :

:: deftheorem Def7 defines closed_wrt_A2 ZF_FUND1:def 7 :

:: deftheorem Def8 defines closed_wrt_A3 ZF_FUND1:def 8 :

:: deftheorem Def9 defines closed_wrt_A4 ZF_FUND1:def 9 :

:: deftheorem Def10 defines closed_wrt_A5 ZF_FUND1:def 10 :

:: deftheorem Def11 defines closed_wrt_A6 ZF_FUND1:def 11 :

:: deftheorem Def12 defines closed_wrt_A7 ZF_FUND1:def 12 :

definition

let V be Universe;
let X be Subclass of V;
attr X 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 :

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

proof end;

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 & rng (f * decode ) c= E )

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 A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) & code (A \ B) = (code A) \ (code B) )
by RELAT_1:153, Lm1, FUNCT_1:123;

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

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

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

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

proof end;

Lm14: 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
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & b in X & b c= Funcs fs,a 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 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 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, 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

proof end;

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

Lm16: 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]}

proof end;

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

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 Lm13, Lm14;

theorem :: ZF_FUND1:24

for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} by Lm15;

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

theorem :: ZF_FUND1:26

canceled;

theorem :: ZF_FUND1:27

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

for o, q being set
for f being Function holds
( dom f = {o,q} iff f = {[o,(f . o)],[q,(f . q)]} ) by Lm17;

theorem :: ZF_FUND1:29

( 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:30

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

theorem :: ZF_FUND1:31

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

theorem :: ZF_FUND1:32

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 & rng (f * decode ) c= E ) by Lm3;

theorem :: ZF_FUND1:33

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

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

for A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) & code (A \ B) = (code A) \ (code B) ) by Lm9;

theorem :: ZF_FUND1:36

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

theorem :: ZF_FUND1:37

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

theorem :: ZF_FUND1:38

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