:: by Grzegorz Bancerek

::

:: Received April 4, 1989

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

begin

:: The operations to make ZF-formulae

definition

let x be Variable;

:: original: <*

redefine func <*x*> -> FinSequence of NAT ;

coherence

<*x*> is FinSequence of NAT

end;
:: original: <*

redefine func <*x*> -> FinSequence of NAT ;

coherence

<*x*> is FinSequence of NAT

proof end;

definition

let x, y be Variable;

coherence

(<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;

coherence

(<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;

end;
coherence

(<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;

coherence

(<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;

:: deftheorem defines '=' ZF_LANG:def 3 :

for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>;

for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>;

:: deftheorem defines 'in' ZF_LANG:def 4 :

for x, y being Variable holds x 'in' y = (<*1*> ^ <*x*>) ^ <*y*>;

for x, y being Variable holds x 'in' y = (<*1*> ^ <*x*>) ^ <*y*>;

definition

let p be FinSequence of NAT ;

coherence

<*2*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*3*> ^ p) ^ q is FinSequence of NAT ;

end;
coherence

<*2*> ^ p is FinSequence of NAT ;

let q be FinSequence of NAT ;

coherence

(<*3*> ^ p) ^ q is FinSequence of NAT ;

:: deftheorem defines 'not' ZF_LANG:def 5 :

for p being FinSequence of NAT holds 'not' p = <*2*> ^ p;

for p being FinSequence of NAT holds 'not' p = <*2*> ^ p;

:: deftheorem defines '&' ZF_LANG:def 6 :

for p, q being FinSequence of NAT holds p '&' q = (<*3*> ^ p) ^ q;

for p, q being FinSequence of NAT holds p '&' q = (<*3*> ^ p) ^ q;

definition

let x be Variable;

let p be FinSequence of NAT ;

coherence

(<*4*> ^ <*x*>) ^ p is FinSequence of NAT ;

end;
let p be FinSequence of NAT ;

coherence

(<*4*> ^ <*x*>) ^ p is FinSequence of NAT ;

:: deftheorem defines All ZF_LANG:def 7 :

for x being Variable

for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p;

for x being Variable

for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p;

theorem Th3: :: ZF_LANG:3

for p, q being FinSequence of NAT

for x, y being Variable st All (x,p) = All (y,q) holds

( x = y & p = q )

for x, y being Variable st All (x,p) = All (y,q) holds

( x = y & p = q )

proof end;

:: The set of all well formed formulae of ZF-language

definition

ex b_{1} being non empty set st

( ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b_{1} & x 'in' y in b_{1} ) ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for x being Variable

for p being FinSequence of NAT st p in b_{1} holds

All (x,p) in b_{1} ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b_{1} c= D ) )

for b_{1}, b_{2} being non empty set st ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b_{1} & x 'in' y in b_{1} ) ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for x being Variable

for p being FinSequence of NAT st p in b_{1} holds

All (x,p) in b_{1} ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b_{1} c= D ) & ( for a being set st a in b_{2} holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b_{2} & x 'in' y in b_{2} ) ) & ( for p being FinSequence of NAT st p in b_{2} holds

'not' p in b_{2} ) & ( for p, q being FinSequence of NAT st p in b_{2} & q in b_{2} holds

p '&' q in b_{2} ) & ( for x being Variable

for p being FinSequence of NAT st p in b_{2} holds

All (x,p) in b_{2} ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func WFF -> non empty set means :Def8: :: ZF_LANG:def 8

( ( for a being set st a in it holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds

'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p '&' q in it ) & ( for x being Variable

for p being FinSequence of NAT st p in it holds

All (x,p) in it ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

it c= D ) );

existence ( ( for a being set st a in it holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds

'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds

p '&' q in it ) & ( for x being Variable

for p being FinSequence of NAT st p in it holds

All (x,p) in it ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

it c= D ) );

ex b

( ( for a being set st a in b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b

'not' p in b

p '&' q in b

for p being FinSequence of NAT st p in b

All (x,p) in b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b

proof end;

uniqueness for b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b

'not' p in b

p '&' q in b

for p being FinSequence of NAT st p in b

All (x,p) in b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b

'not' p in b

p '&' q in b

for p being FinSequence of NAT st p in b

All (x,p) in b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b

b

proof end;

:: deftheorem Def8 defines WFF ZF_LANG:def 8 :

for b_{1} being non empty set holds

( b_{1} = WFF iff ( ( for a being set st a in b_{1} holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b_{1} & x 'in' y in b_{1} ) ) & ( for p being FinSequence of NAT st p in b_{1} holds

'not' p in b_{1} ) & ( for p, q being FinSequence of NAT st p in b_{1} & q in b_{1} holds

p '&' q in b_{1} ) & ( for x being Variable

for p being FinSequence of NAT st p in b_{1} holds

All (x,p) in b_{1} ) & ( for D being non empty set st ( for a being set st a in D holds

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b_{1} c= D ) ) );

for b

( b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in b

'not' p in b

p '&' q in b

for p being FinSequence of NAT st p in b

All (x,p) in b

a is FinSequence of NAT ) & ( for x, y being Variable holds

( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds

'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds

p '&' q in D ) & ( for x being Variable

for p being FinSequence of NAT st p in D holds

All (x,p) in D ) holds

b

:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def 9 :

for IT being FinSequence of NAT holds

( IT is ZF-formula-like iff IT is Element of WFF );

for IT being FinSequence of NAT holds

( IT is ZF-formula-like iff IT is Element of WFF );

registration

ex b_{1} being FinSequence of NAT st b_{1} is ZF-formula-like
end;

cluster Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like ZF-formula-like for FinSequence of NAT ;

existence ex b

proof end;

registration

let x, y be Variable;

coherence

x '=' y is ZF-formula-like

x 'in' y is ZF-formula-like

end;
coherence

x '=' y is ZF-formula-like

proof end;

coherence x 'in' y is ZF-formula-like

proof end;

registration

let H be ZF-formula;

coherence

'not' H is ZF-formula-like

coherence

H '&' G is ZF-formula-like

end;
coherence

'not' H is ZF-formula-like

proof end;

let G be ZF-formula;coherence

H '&' G is ZF-formula-like

proof end;

registration
end;

::

:: The Properties of ZF-formulae

::

:: The Properties of ZF-formulae

::

definition

let H be ZF-formula;

end;
attr H is universal means :Def14: :: ZF_LANG:def 14

ex x being Variable ex H1 being ZF-formula st H = All (x,H1);

ex x being Variable ex H1 being ZF-formula st H = All (x,H1);

:: deftheorem Def10 defines being_equality ZF_LANG:def 10 :

for H being ZF-formula holds

( H is being_equality iff ex x, y being Variable st H = x '=' y );

for H being ZF-formula holds

( H is being_equality iff ex x, y being Variable st H = x '=' y );

:: deftheorem Def11 defines being_membership ZF_LANG:def 11 :

for H being ZF-formula holds

( H is being_membership iff ex x, y being Variable st H = x 'in' y );

for H being ZF-formula holds

( H is being_membership iff ex x, y being Variable st H = x 'in' y );

:: deftheorem Def12 defines negative ZF_LANG:def 12 :

for H being ZF-formula holds

( H is negative iff ex H1 being ZF-formula st H = 'not' H1 );

for H being ZF-formula holds

( H is negative iff ex H1 being ZF-formula st H = 'not' H1 );

:: deftheorem Def13 defines conjunctive ZF_LANG:def 13 :

for H being ZF-formula holds

( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G );

for H being ZF-formula holds

( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G );

:: deftheorem Def14 defines universal ZF_LANG:def 14 :

for H being ZF-formula holds

( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) );

for H being ZF-formula holds

( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) );

theorem :: ZF_LANG:5

for H being ZF-formula holds

( ( H is being_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is being_equality ) & ( H is being_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is being_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = All (x,H1) implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14;

( ( H is being_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is being_equality ) & ( H is being_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is being_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = All (x,H1) implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14;

:: deftheorem Def15 defines atomic ZF_LANG:def 15 :

for H being ZF-formula holds

( H is atomic iff ( H is being_equality or H is being_membership ) );

for H being ZF-formula holds

( H is atomic iff ( H is being_equality or H is being_membership ) );

definition

let F, G be ZF-formula;

coherence

'not' (('not' F) '&' ('not' G)) is ZF-formula ;

coherence

'not' (F '&' ('not' G)) is ZF-formula ;

end;
coherence

'not' (('not' F) '&' ('not' G)) is ZF-formula ;

coherence

'not' (F '&' ('not' G)) is ZF-formula ;

:: deftheorem defines 'or' ZF_LANG:def 16 :

for F, G being ZF-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));

for F, G being ZF-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));

:: deftheorem defines => ZF_LANG:def 17 :

for F, G being ZF-formula holds F => G = 'not' (F '&' ('not' G));

for F, G being ZF-formula holds F => G = 'not' (F '&' ('not' G));

:: deftheorem defines <=> ZF_LANG:def 18 :

for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);

for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);

definition
end;

:: deftheorem defines Ex ZF_LANG:def 19 :

for x being Variable

for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H)));

for x being Variable

for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H)));

definition

let H be ZF-formula;

end;
attr H is existential means :Def23: :: ZF_LANG:def 23

ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1);

ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1);

:: deftheorem Def20 defines disjunctive ZF_LANG:def 20 :

for H being ZF-formula holds

( H is disjunctive iff ex F, G being ZF-formula st H = F 'or' G );

for H being ZF-formula holds

( H is disjunctive iff ex F, G being ZF-formula st H = F 'or' G );

:: deftheorem Def21 defines conditional ZF_LANG:def 21 :

for H being ZF-formula holds

( H is conditional iff ex F, G being ZF-formula st H = F => G );

for H being ZF-formula holds

( H is conditional iff ex F, G being ZF-formula st H = F => G );

:: deftheorem Def22 defines biconditional ZF_LANG:def 22 :

for H being ZF-formula holds

( H is biconditional iff ex F, G being ZF-formula st H = F <=> G );

for H being ZF-formula holds

( H is biconditional iff ex F, G being ZF-formula st H = F <=> G );

:: deftheorem Def23 defines existential ZF_LANG:def 23 :

for H being ZF-formula holds

( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) );

for H being ZF-formula holds

( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) );

theorem :: ZF_LANG:6

for H being ZF-formula holds

( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) implies H is existential ) ) by Def20, Def21, Def22, Def23;

( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) implies H is existential ) ) by Def20, Def21, Def22, Def23;

definition

let x, y be Variable;

let H be ZF-formula;

coherence

All (x,(All (y,H))) is ZF-formula ;

coherence

Ex (x,(Ex (y,H))) is ZF-formula ;

end;
let H be ZF-formula;

coherence

All (x,(All (y,H))) is ZF-formula ;

coherence

Ex (x,(Ex (y,H))) is ZF-formula ;

:: deftheorem defines All ZF_LANG:def 24 :

for x, y being Variable

for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H)));

for x, y being Variable

for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H)));

:: deftheorem defines Ex ZF_LANG:def 25 :

for x, y being Variable

for H being ZF-formula holds Ex (x,y,H) = Ex (x,(Ex (y,H)));

for x, y being Variable

for H being ZF-formula holds Ex (x,y,H) = Ex (x,(Ex (y,H)));

theorem :: ZF_LANG:7

definition

let x, y, z be Variable;

let H be ZF-formula;

coherence

All (x,(All (y,z,H))) is ZF-formula ;

coherence

Ex (x,(Ex (y,z,H))) is ZF-formula ;

end;
let H be ZF-formula;

coherence

All (x,(All (y,z,H))) is ZF-formula ;

coherence

Ex (x,(Ex (y,z,H))) is ZF-formula ;

:: deftheorem defines All ZF_LANG:def 26 :

for x, y, z being Variable

for H being ZF-formula holds All (x,y,z,H) = All (x,(All (y,z,H)));

for x, y, z being Variable

for H being ZF-formula holds All (x,y,z,H) = All (x,(All (y,z,H)));

:: deftheorem defines Ex ZF_LANG:def 27 :

for x, y, z being Variable

for H being ZF-formula holds Ex (x,y,z,H) = Ex (x,(Ex (y,z,H)));

for x, y, z being Variable

for H being ZF-formula holds Ex (x,y,z,H) = Ex (x,(Ex (y,z,H)));

theorem :: ZF_LANG:8

theorem Th9: :: ZF_LANG:9

for H being ZF-formula holds

( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )

( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )

proof end;

theorem Th23: :: ZF_LANG:23

for H being ZF-formula holds

( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) )

( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) )

proof end;

::

:: The Select Function of ZF-fomrulae

::

:: The Select Function of ZF-fomrulae

::

definition

let H be ZF-formula;

assume A1: H is atomic ;

coherence

H . 2 is Variable

H . 3 is Variable

end;
assume A1: H is atomic ;

coherence

H . 2 is Variable

proof end;

coherence H . 3 is Variable

proof end;

:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :

for H being ZF-formula st H is atomic holds

Var1 H = H . 2;

for H being ZF-formula st H is atomic holds

Var1 H = H . 2;

:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :

for H being ZF-formula st H is atomic holds

Var2 H = H . 3;

for H being ZF-formula st H is atomic holds

Var2 H = H . 3;

theorem :: ZF_LANG:35

definition

let H be ZF-formula;

assume A1: H is negative ;

existence

ex b_{1} being ZF-formula st 'not' b_{1} = H
by A1, Def12;

uniqueness

for b_{1}, b_{2} being ZF-formula st 'not' b_{1} = H & 'not' b_{2} = H holds

b_{1} = b_{2}
by FINSEQ_1:33;

end;
assume A1: H is negative ;

existence

ex b

uniqueness

for b

b

:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :

for H being ZF-formula st H is negative holds

for b_{2} being ZF-formula holds

( b_{2} = the_argument_of H iff 'not' b_{2} = H );

for H being ZF-formula st H is negative holds

for b

( b

definition

let H be ZF-formula;

assume A1: ( H is conjunctive or H is disjunctive ) ;

( ( H is conjunctive implies ex b_{1}, H1 being ZF-formula st b_{1} '&' H1 = H ) & ( not H is conjunctive implies ex b_{1}, H1 being ZF-formula st b_{1} 'or' H1 = H ) )
by A1, Def13, Def20;

uniqueness

for b_{1}, b_{2} being ZF-formula holds

( ( H is conjunctive & ex H1 being ZF-formula st b_{1} '&' H1 = H & ex H1 being ZF-formula st b_{2} '&' H1 = H implies b_{1} = b_{2} ) & ( not H is conjunctive & ex H1 being ZF-formula st b_{1} 'or' H1 = H & ex H1 being ZF-formula st b_{2} 'or' H1 = H implies b_{1} = b_{2} ) )
by Th30, Th31;

consistency

for b_{1} being ZF-formula holds verum
;

( ( H is conjunctive implies ex b_{1}, H1 being ZF-formula st H1 '&' b_{1} = H ) & ( not H is conjunctive implies ex b_{1}, H1 being ZF-formula st H1 'or' b_{1} = H ) )

for b_{1}, b_{2} being ZF-formula holds

( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b_{1} = H & ex H1 being ZF-formula st H1 '&' b_{2} = H implies b_{1} = b_{2} ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b_{1} = H & ex H1 being ZF-formula st H1 'or' b_{2} = H implies b_{1} = b_{2} ) )
by Th30, Th31;

consistency

for b_{1} being ZF-formula holds verum
;

end;
assume A1: ( H is conjunctive or H is disjunctive ) ;

func the_left_argument_of H -> ZF-formula means :Def31: :: ZF_LANG:def 31

ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive

otherwise ex H1 being ZF-formula st it 'or' H1 = H;

existence ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive

otherwise ex H1 being ZF-formula st it 'or' H1 = H;

( ( H is conjunctive implies ex b

uniqueness

for b

( ( H is conjunctive & ex H1 being ZF-formula st b

consistency

for b

func the_right_argument_of H -> ZF-formula means :Def32: :: ZF_LANG:def 32

ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive

otherwise ex H1 being ZF-formula st H1 'or' it = H;

existence ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive

otherwise ex H1 being ZF-formula st H1 'or' it = H;

( ( H is conjunctive implies ex b

proof end;

uniqueness for b

( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b

consistency

for b

:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def 31 :

for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds

for b_{2} being ZF-formula holds

( ( H is conjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being ZF-formula st b_{2} '&' H1 = H ) ) & ( not H is conjunctive implies ( b_{2} = the_left_argument_of H iff ex H1 being ZF-formula st b_{2} 'or' H1 = H ) ) );

for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds

for b

( ( H is conjunctive implies ( b

:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def 32 :

for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds

for b_{2} being ZF-formula holds

( ( H is conjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being ZF-formula st H1 '&' b_{2} = H ) ) & ( not H is conjunctive implies ( b_{2} = the_right_argument_of H iff ex H1 being ZF-formula st H1 'or' b_{2} = H ) ) );

for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds

for b

( ( H is conjunctive implies ( b

theorem :: ZF_LANG:38

for H, F being ZF-formula st H is conjunctive holds

( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32;

( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32;

theorem Th39: :: ZF_LANG:39

for H, F being ZF-formula st H is disjunctive holds

( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )

( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )

proof end;

theorem Th40: :: ZF_LANG:40

for H being ZF-formula st H is conjunctive holds

H = (the_left_argument_of H) '&' (the_right_argument_of H)

H = (the_left_argument_of H) '&' (the_right_argument_of H)

proof end;

theorem :: ZF_LANG:41

for H being ZF-formula st H is disjunctive holds

H = (the_left_argument_of H) 'or' (the_right_argument_of H)

H = (the_left_argument_of H) 'or' (the_right_argument_of H)

proof end;

definition

let H be ZF-formula;

assume A1: ( H is universal or H is existential ) ;

( ( H is universal implies ex b_{1} being Variable ex H1 being ZF-formula st All (b_{1},H1) = H ) & ( not H is universal implies ex b_{1} being Variable ex H1 being ZF-formula st Ex (b_{1},H1) = H ) )
by A1, Def14, Def23;

uniqueness

for b_{1}, b_{2} being Variable holds

( ( H is universal & ex H1 being ZF-formula st All (b_{1},H1) = H & ex H1 being ZF-formula st All (b_{2},H1) = H implies b_{1} = b_{2} ) & ( not H is universal & ex H1 being ZF-formula st Ex (b_{1},H1) = H & ex H1 being ZF-formula st Ex (b_{2},H1) = H implies b_{1} = b_{2} ) )
by Th3, Th34;

consistency

for b_{1} being Variable holds verum
;

( ( H is universal implies ex b_{1} being ZF-formula ex x being Variable st All (x,b_{1}) = H ) & ( not H is universal implies ex b_{1} being ZF-formula ex x being Variable st Ex (x,b_{1}) = H ) )

for b_{1}, b_{2} being ZF-formula holds

( ( H is universal & ex x being Variable st All (x,b_{1}) = H & ex x being Variable st All (x,b_{2}) = H implies b_{1} = b_{2} ) & ( not H is universal & ex x being Variable st Ex (x,b_{1}) = H & ex x being Variable st Ex (x,b_{2}) = H implies b_{1} = b_{2} ) )
by Th3, Th34;

consistency

for b_{1} being ZF-formula holds verum
;

end;
assume A1: ( H is universal or H is existential ) ;

func bound_in H -> Variable means :Def33: :: ZF_LANG:def 33

ex H1 being ZF-formula st All (it,H1) = H if H is universal

otherwise ex H1 being ZF-formula st Ex (it,H1) = H;

existence ex H1 being ZF-formula st All (it,H1) = H if H is universal

otherwise ex H1 being ZF-formula st Ex (it,H1) = H;

( ( H is universal implies ex b

uniqueness

for b

( ( H is universal & ex H1 being ZF-formula st All (b

consistency

for b

func the_scope_of H -> ZF-formula means :Def34: :: ZF_LANG:def 34

ex x being Variable st All (x,it) = H if H is universal

otherwise ex x being Variable st Ex (x,it) = H;

existence ex x being Variable st All (x,it) = H if H is universal

otherwise ex x being Variable st Ex (x,it) = H;

( ( H is universal implies ex b

proof end;

uniqueness for b

( ( H is universal & ex x being Variable st All (x,b

consistency

for b

:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :

for H being ZF-formula st ( H is universal or H is existential ) holds

for b_{2} being Variable holds

( ( H is universal implies ( b_{2} = bound_in H iff ex H1 being ZF-formula st All (b_{2},H1) = H ) ) & ( not H is universal implies ( b_{2} = bound_in H iff ex H1 being ZF-formula st Ex (b_{2},H1) = H ) ) );

for H being ZF-formula st ( H is universal or H is existential ) holds

for b

( ( H is universal implies ( b

:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :

for H being ZF-formula st ( H is universal or H is existential ) holds

for b_{2} being ZF-formula holds

( ( H is universal implies ( b_{2} = the_scope_of H iff ex x being Variable st All (x,b_{2}) = H ) ) & ( not H is universal implies ( b_{2} = the_scope_of H iff ex x being Variable st Ex (x,b_{2}) = H ) ) );

for H being ZF-formula st ( H is universal or H is existential ) holds

for b

( ( H is universal implies ( b

theorem :: ZF_LANG:42

for x being Variable

for H, H1 being ZF-formula st H is universal holds

( ( x = bound_in H implies ex H1 being ZF-formula st All (x,H1) = H ) & ( ex H1 being ZF-formula st All (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All (x,H1) = H ) & ( ex x being Variable st All (x,H1) = H implies H1 = the_scope_of H ) ) by Def33, Def34;

for H, H1 being ZF-formula st H is universal holds

( ( x = bound_in H implies ex H1 being ZF-formula st All (x,H1) = H ) & ( ex H1 being ZF-formula st All (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All (x,H1) = H ) & ( ex x being Variable st All (x,H1) = H implies H1 = the_scope_of H ) ) by Def33, Def34;

theorem Th43: :: ZF_LANG:43

for x being Variable

for H, H1 being ZF-formula st H is existential holds

( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) )

for H, H1 being ZF-formula st H is existential holds

( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) )

proof end;

definition

let H be ZF-formula;

assume A1: H is conditional ;

ex b_{1}, H1 being ZF-formula st H = b_{1} => H1
by A1, Def21;

uniqueness

for b_{1}, b_{2} being ZF-formula st ex H1 being ZF-formula st H = b_{1} => H1 & ex H1 being ZF-formula st H = b_{2} => H1 holds

b_{1} = b_{2}
by Th32;

ex b_{1}, H1 being ZF-formula st H = H1 => b_{1}

for b_{1}, b_{2} being ZF-formula st ex H1 being ZF-formula st H = H1 => b_{1} & ex H1 being ZF-formula st H = H1 => b_{2} holds

b_{1} = b_{2}
by Th32;

end;
assume A1: H is conditional ;

func the_antecedent_of H -> ZF-formula means :Def35: :: ZF_LANG:def 35

ex H1 being ZF-formula st H = it => H1;

existence ex H1 being ZF-formula st H = it => H1;

ex b

uniqueness

for b

b

func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36

ex H1 being ZF-formula st H = H1 => it;

existence ex H1 being ZF-formula st H = H1 => it;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :

for H being ZF-formula st H is conditional holds

for b_{2} being ZF-formula holds

( b_{2} = the_antecedent_of H iff ex H1 being ZF-formula st H = b_{2} => H1 );

for H being ZF-formula st H is conditional holds

for b

( b

:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :

for H being ZF-formula st H is conditional holds

for b_{2} being ZF-formula holds

( b_{2} = the_consequent_of H iff ex H1 being ZF-formula st H = H1 => b_{2} );

for H being ZF-formula st H is conditional holds

for b

( b

theorem :: ZF_LANG:46

for H, F being ZF-formula st H is conditional holds

( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36;

( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36;

definition

let H be ZF-formula;

assume A1: H is biconditional ;

ex b_{1}, H1 being ZF-formula st H = b_{1} <=> H1
by A1, Def22;

uniqueness

for b_{1}, b_{2} being ZF-formula st ex H1 being ZF-formula st H = b_{1} <=> H1 & ex H1 being ZF-formula st H = b_{2} <=> H1 holds

b_{1} = b_{2}
by Th33;

ex b_{1}, H1 being ZF-formula st H = H1 <=> b_{1}

for b_{1}, b_{2} being ZF-formula st ex H1 being ZF-formula st H = H1 <=> b_{1} & ex H1 being ZF-formula st H = H1 <=> b_{2} holds

b_{1} = b_{2}
by Th33;

end;
assume A1: H is biconditional ;

func the_left_side_of H -> ZF-formula means :Def37: :: ZF_LANG:def 37

ex H1 being ZF-formula st H = it <=> H1;

existence ex H1 being ZF-formula st H = it <=> H1;

ex b

uniqueness

for b

b

func the_right_side_of H -> ZF-formula means :Def38: :: ZF_LANG:def 38

ex H1 being ZF-formula st H = H1 <=> it;

existence ex H1 being ZF-formula st H = H1 <=> it;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :

for H being ZF-formula st H is biconditional holds

for b_{2} being ZF-formula holds

( b_{2} = the_left_side_of H iff ex H1 being ZF-formula st H = b_{2} <=> H1 );

for H being ZF-formula st H is biconditional holds

for b

( b

:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :

for H being ZF-formula st H is biconditional holds

for b_{2} being ZF-formula holds

( b_{2} = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b_{2} );

for H being ZF-formula st H is biconditional holds

for b

( b

theorem :: ZF_LANG:48

for H, F being ZF-formula st H is biconditional holds

( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38;

( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38;

theorem :: ZF_LANG:49

for H being ZF-formula st H is biconditional holds

H = (the_left_side_of H) <=> (the_right_side_of H)

H = (the_left_side_of H) <=> (the_right_side_of H)

proof end;

::

:: The Immediate Constituents of ZF-formulae

::

:: The Immediate Constituents of ZF-formulae

::

definition

let H, F be ZF-formula;

end;
pred H is_immediate_constituent_of F means :Def39: :: ZF_LANG:def 39

( F = 'not' H or ex H1 being ZF-formula st

( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) );

( F = 'not' H or ex H1 being ZF-formula st

( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) );

:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :

for H, F being ZF-formula holds

( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st

( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) );

for H, F being ZF-formula holds

( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st

( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) );

theorem Th54: :: ZF_LANG:54

for x being Variable

for F, H being ZF-formula holds

( F is_immediate_constituent_of All (x,H) iff F = H )

for F, H being ZF-formula holds

( F is_immediate_constituent_of All (x,H) iff F = H )

proof end;

theorem Th56: :: ZF_LANG:56

for H, F being ZF-formula st H is negative holds

( F is_immediate_constituent_of H iff F = the_argument_of H )

( F is_immediate_constituent_of H iff F = the_argument_of H )

proof end;

theorem Th57: :: ZF_LANG:57

for H, F being ZF-formula st H is conjunctive holds

( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )

( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )

proof end;

theorem Th58: :: ZF_LANG:58

for H, F being ZF-formula st H is universal holds

( F is_immediate_constituent_of H iff F = the_scope_of H )

( F is_immediate_constituent_of H iff F = the_scope_of H )

proof end;

definition

let H, F be ZF-formula;

end;
pred H is_subformula_of F means :Def40: :: ZF_LANG:def 40

ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds

ex H1, F1 being ZF-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );

ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds

ex H1, F1 being ZF-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );

:: deftheorem Def40 defines is_subformula_of ZF_LANG:def 40 :

for H, F being ZF-formula holds

( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds

ex H1, F1 being ZF-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );

for H, F being ZF-formula holds

( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds

ex H1, F1 being ZF-formula st

( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );

:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :

for H, F being ZF-formula holds

( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );

for H, F being ZF-formula holds

( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );

theorem Th63: :: ZF_LANG:63

for H, F being ZF-formula st H is_proper_subformula_of F holds

ex G being ZF-formula st G is_immediate_constituent_of F

ex G being ZF-formula st G is_immediate_constituent_of F

proof end;

theorem Th64: :: ZF_LANG:64

for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds

F is_proper_subformula_of H

F is_proper_subformula_of H

proof end;

theorem Th65: :: ZF_LANG:65

for F, G, H being ZF-formula st F is_subformula_of G & G is_subformula_of H holds

F is_subformula_of H

F is_subformula_of H

proof end;

theorem Th70: :: ZF_LANG:70

for F, G, H being ZF-formula holds

( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )

( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )

proof end;

theorem Th71: :: ZF_LANG:71

for x being Variable

for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds

F is_subformula_of H

for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds

F is_subformula_of H

proof end;

theorem :: ZF_LANG:74

for H being ZF-formula st H is conjunctive holds

( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )

( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )

proof end;

theorem Th77: :: ZF_LANG:77

for x, y being Variable

for H being ZF-formula holds

( H is_subformula_of x 'in' y iff H = x 'in' y )

for H being ZF-formula holds

( H is_subformula_of x 'in' y iff H = x 'in' y )

proof end;

::

:: The Set of Subformulae of ZF-formulae

::

:: The Set of Subformulae of ZF-formulae

::

definition

let H be ZF-formula;

ex b_{1} being set st

for a being set holds

( a in b_{1} iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) )

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

( a in b_{1} iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b_{2} iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) ) ) holds

b_{1} = b_{2}

end;
func Subformulae H -> set means :Def42: :: ZF_LANG:def 42

for a being set holds

( a in it iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) );

existence for a being set holds

( a in it iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) );

ex b

for a being set holds

( a in b

( F = a & F is_subformula_of H ) )

proof end;

uniqueness for b

( a in b

( F = a & F is_subformula_of H ) ) ) & ( for a being set holds

( a in b

( F = a & F is_subformula_of H ) ) ) holds

b

proof end;

:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :

for H being ZF-formula

for b_{2} being set holds

( b_{2} = Subformulae H iff for a being set holds

( a in b_{2} iff ex F being ZF-formula st

( F = a & F is_subformula_of H ) ) );

for H being ZF-formula

for b

( b

( a in b

( F = a & F is_subformula_of H ) ) );

theorem Th83: :: ZF_LANG:83

for H, F being ZF-formula holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}

proof end;

theorem Th84: :: ZF_LANG:84

for x being Variable

for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}

for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}

proof end;

theorem :: ZF_LANG:86

for H being ZF-formula st H is negative holds

Subformulae H = (Subformulae (the_argument_of H)) \/ {H}

Subformulae H = (Subformulae (the_argument_of H)) \/ {H}

proof end;

theorem :: ZF_LANG:87

for H being ZF-formula st H is conjunctive holds

Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

proof end;

theorem :: ZF_LANG:88

for H being ZF-formula st H is universal holds

Subformulae H = (Subformulae (the_scope_of H)) \/ {H}

Subformulae H = (Subformulae (the_scope_of H)) \/ {H}

proof end;

theorem :: ZF_LANG:89

for H, G, F being ZF-formula st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds

H in Subformulae F

H in Subformulae F

proof end;

::

:: The Structural Induction Schemes

::

:: The Structural Induction Schemes

::

scheme :: ZF_LANG:sch 1

ZFInd{ P_{1}[ ZF-formula] } :

provided

ZFInd{ P

provided

A1:
for H being ZF-formula st H is atomic holds

P_{1}[H]
and

A2: for H being ZF-formula st H is negative & P_{1}[ the_argument_of H] holds

P_{1}[H]
and

A3: for H being ZF-formula st H is conjunctive & P_{1}[ the_left_argument_of H] & P_{1}[ the_right_argument_of H] holds

P_{1}[H]
and

A4: for H being ZF-formula st H is universal & P_{1}[ the_scope_of H] holds

P_{1}[H]

P

A2: for H being ZF-formula st H is negative & P

P

A3: for H being ZF-formula st H is conjunctive & P

P

A4: for H being ZF-formula st H is universal & P

P

proof end;

scheme :: ZF_LANG:sch 2

ZFCompInd{ P_{1}[ ZF-formula] } :

provided

ZFCompInd{ P

provided

A1:
for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds

P_{1}[F] ) holds

P_{1}[H]

P

P

proof end;

:: The Construction of ZF Set Theory Language

::

:: The set and the mode of ZF-language variables