:: A Model of ZF Set Theory Language
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users


::
:: The Construction of ZF Set Theory Language
::
:: The set and the mode of ZF-language variables
definition
func VAR -> Subset of NAT equals :: ZF_LANG:def 1
 { k where k is Element of NAT : 5 <= k } ;
coherence
{ k where k is Element of NAT : 5 <= k } is Subset of NAT
proof end;
end;

:: deftheorem defines VAR ZF_LANG:def 1 :
VAR = { k where k is Element of NAT : 5 <= k } ;

registration
cluster VAR -> non empty ;
coherence
not VAR is empty
proof end;
end;

definition
mode Variable is Element of VAR ;
end;

definition
let n be Element of NAT ;
func x. n -> Variable equals :: ZF_LANG:def 2
5 + n;
coherence
5 + n is Variable
proof end;
end;

:: deftheorem defines x. ZF_LANG:def 2 :
for n being Element of NAT holds x. n = 5 + n;

:: The operations to make ZF-formulae
registration
cluster -> natural for Element of VAR ;
coherence
for b1 being Variable holds b1 is natural ;
end;

definition
let x, y be Variable;
func x '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3
(<*0*> ^ <*x*>) ^ <*y*>;
coherence
(<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;
func x 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4
(<*1*> ^ <*x*>) ^ <*y*>;
coherence
(<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;
end;

:: deftheorem defines '=' ZF_LANG:def 3 :
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*>;

theorem :: ZF_LANG:1
for x, y, z, t being Variable st x '=' y = z '=' t holds
( x = z & y = t )
proof end;

theorem :: ZF_LANG:2
for x, y, z, t being Variable st x 'in' y = z 'in' t holds
( x = z & y = t )
proof end;

definition
let p be FinSequence of NAT ;
func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5
<*2*> ^ p;
coherence
<*2*> ^ p is FinSequence of NAT ;
let q be FinSequence of NAT ;
func p '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6
(<*3*> ^ p) ^ q;
coherence
(<*3*> ^ p) ^ q is FinSequence of NAT ;
end;

:: deftheorem defines 'not' ZF_LANG:def 5 :
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;

definition
let x be Variable;
let p be FinSequence of NAT ;
func All (x,p) -> FinSequence of NAT equals :: ZF_LANG:def 7
(<*4*> ^ <*x*>) ^ p;
coherence
(<*4*> ^ <*x*>) ^ p is FinSequence of NAT ;
end;

:: deftheorem defines All ZF_LANG:def 7 :
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 )
proof end;

:: The set of all well formed formulae of ZF-language
definition
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
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( 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
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( 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
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b2 & x 'in' y in b2 ) ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for x being Variable
for p being FinSequence of NAT st p in b2 holds
All (x,p) in b2 ) & ( 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
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines WFF ZF_LANG:def 8 :
for b1 being non empty set holds
( b1 = WFF iff ( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( 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
b1 c= D ) ) );

definition
let IT be FinSequence of NAT ;
attr IT is ZF-formula-like means :Def9: :: ZF_LANG:def 9
IT is Element of WFF ;
end;

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

registration
cluster Relation-like omega -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like ZF-formula-like for FinSequence of NAT ;
existence
ex b1 being FinSequence of NAT st b1 is ZF-formula-like
proof end;
end;

definition
mode ZF-formula is ZF-formula-like FinSequence of NAT ;
end;

theorem :: ZF_LANG:4
for a being set holds
( a is ZF-formula iff a in WFF )
proof end;

registration
let x, y be Variable;
cluster x '=' y -> ZF-formula-like ;
coherence
x '=' y is ZF-formula-like by Def8;
cluster x 'in' y -> ZF-formula-like ;
coherence
x 'in' y is ZF-formula-like by Def8;
end;

registration
let H be ZF-formula;
cluster 'not' H -> ZF-formula-like ;
coherence
'not' H is ZF-formula-like
proof end;
let G be ZF-formula;
cluster H '&' G -> ZF-formula-like ;
coherence
H '&' G is ZF-formula-like
proof end;
end;

registration
let x be Variable;
let H be ZF-formula;
cluster All (x,H) -> ZF-formula-like ;
coherence
All (x,H) is ZF-formula-like
proof end;
end;

::
:: The Properties of ZF-formulae
::
definition
let H be ZF-formula;
attr H is being_equality means :: ZF_LANG:def 10
 ex x, y being Variable st H = x '=' y;
attr H is being_membership means :: ZF_LANG:def 11
 ex x, y being Variable st H = x 'in' y;
attr H is negative means :: ZF_LANG:def 12
 ex H1 being ZF-formula st H = 'not' H1;
attr H is conjunctive means :: ZF_LANG:def 13
 ex F, G being ZF-formula st H = F '&' G;
attr H is universal means :: ZF_LANG:def 14
 ex x being Variable ex H1 being ZF-formula st H = All (x,H1);
end;

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

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

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

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

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

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

definition
let H be ZF-formula;
attr H is atomic means :: ZF_LANG:def 15
( H is being_equality or H is being_membership );
end;

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

definition
let F, G be ZF-formula;
func F 'or' G -> ZF-formula equals :: ZF_LANG:def 16
 'not' (('not' F) '&' ('not' G));
coherence
'not' (('not' F) '&' ('not' G)) is ZF-formula ;
func F => G -> ZF-formula equals :: ZF_LANG:def 17
 'not' (F '&' ('not' G));
coherence
'not' (F '&' ('not' G)) is ZF-formula ;
end;

:: deftheorem defines 'or' ZF_LANG:def 16 :
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));

definition
let F, G be ZF-formula;
func F <=> G -> ZF-formula equals :: ZF_LANG:def 18
(F => G) '&' (G => F);
coherence
(F => G) '&' (G => F) is ZF-formula ;
end;

:: deftheorem defines <=> ZF_LANG:def 18 :
for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);

definition
let x be Variable;
let H be ZF-formula;
func Ex (x,H) -> ZF-formula equals :: ZF_LANG:def 19
 'not' (All (x,('not' H)));
coherence
'not' (All (x,('not' H))) is ZF-formula ;
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)));

definition
let H be ZF-formula;
attr H is disjunctive means :: ZF_LANG:def 20
 ex F, G being ZF-formula st H = F 'or' G;
attr H is conditional means :: ZF_LANG:def 21
 ex F, G being ZF-formula st H = F => G;
attr H is biconditional means :: ZF_LANG:def 22
 ex F, G being ZF-formula st H = F <=> G;
attr H is existential means :: ZF_LANG:def 23
 ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1);
end;

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

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

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

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

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

definition
let x, y be Variable;
let H be ZF-formula;
func All (x,y,H) -> ZF-formula equals :: ZF_LANG:def 24
 All (x,(All (y,H)));
coherence
All (x,(All (y,H))) is ZF-formula ;
func Ex (x,y,H) -> ZF-formula equals :: ZF_LANG:def 25
 Ex (x,(Ex (y,H)));
coherence
Ex (x,(Ex (y,H))) is ZF-formula ;
end;

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

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

theorem :: ZF_LANG:7
for x, y being Variable
for H being ZF-formula holds
( All (x,y,H) = All (x,(All (y,H))) & Ex (x,y,H) = Ex (x,(Ex (y,H))) ) ;

definition
let x, y, z be Variable;
let H be ZF-formula;
func All (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 26
 All (x,(All (y,z,H)));
coherence
All (x,(All (y,z,H))) is ZF-formula ;
func Ex (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27
 Ex (x,(Ex (y,z,H)));
coherence
Ex (x,(Ex (y,z,H))) is ZF-formula ;
end;

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

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

theorem :: ZF_LANG:8
for x, y, z being Variable
for H being ZF-formula holds
( All (x,y,z,H) = All (x,(All (y,z,H))) & Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))) ) ;

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

theorem Th10: :: ZF_LANG:10
for H being ZF-formula holds
( H is atomic or H is negative or H is conjunctive or H is universal ) by Th9;

theorem Th11: :: ZF_LANG:11
for H being ZF-formula st H is atomic holds
len H = 3
proof end;

theorem Th12: :: ZF_LANG:12
for H being ZF-formula holds
( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )
proof end;

theorem Th13: :: ZF_LANG:13
for H being ZF-formula holds 3 <= len H
proof end;

theorem :: ZF_LANG:14
for H being ZF-formula st len H = 3 holds
H is atomic
proof end;

theorem Th15: :: ZF_LANG:15
for x, y being Variable holds
( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )
proof end;

theorem Th16: :: ZF_LANG:16
for F, G being ZF-formula holds (F '&' G) . 1 = 3
proof end;

theorem Th17: :: ZF_LANG:17
for x being Variable
for H being ZF-formula holds (All (x,H)) . 1 = 4
proof end;

theorem Th18: :: ZF_LANG:18
for H being ZF-formula st H is being_equality holds
H . 1 = 0
proof end;

theorem Th19: :: ZF_LANG:19
for H being ZF-formula st H is being_membership holds
H . 1 = 1
proof end;

theorem Th20: :: ZF_LANG:20
for H being ZF-formula st H is negative holds
H . 1 = 2 by FINSEQ_1:41;

theorem Th21: :: ZF_LANG:21
for H being ZF-formula st H is conjunctive holds
H . 1 = 3
proof end;

theorem Th22: :: ZF_LANG:22
for H being ZF-formula st H is universal holds
H . 1 = 4
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 ) )
proof end;

theorem :: ZF_LANG:24
for H being ZF-formula st H . 1 = 0 holds
H is being_equality by Th23;

theorem :: ZF_LANG:25
for H being ZF-formula st H . 1 = 1 holds
H is being_membership by Th23;

theorem :: ZF_LANG:26
for H being ZF-formula st H . 1 = 2 holds
H is negative by Th23;

theorem :: ZF_LANG:27
for H being ZF-formula st H . 1 = 3 holds
H is conjunctive by Th23;

theorem :: ZF_LANG:28
for H being ZF-formula st H . 1 = 4 holds
H is universal by Th23;

theorem Th29: :: ZF_LANG:29
for F, H being ZF-formula
for sq being FinSequence st H = F ^ sq holds
H = F
proof end;

theorem Th30: :: ZF_LANG:30
for G, G1, H, H1 being ZF-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )
proof end;

theorem Th31: :: ZF_LANG:31
for F, F1, G, G1 being ZF-formula st F 'or' G = F1 'or' G1 holds
( F = F1 & G = G1 )
proof end;

theorem Th32: :: ZF_LANG:32
for F, F1, G, G1 being ZF-formula st F => G = F1 => G1 holds
( F = F1 & G = G1 )
proof end;

theorem Th33: :: ZF_LANG:33
for F, F1, G, G1 being ZF-formula st F <=> G = F1 <=> G1 holds
( F = F1 & G = G1 )
proof end;

theorem Th34: :: ZF_LANG:34
for x, y being Variable
for G, H being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )
proof end;

::
:: The Select Function of ZF-fomrulae
::
definition
let H be ZF-formula;
assume A1: H is atomic ;
func Var1 H -> Variable equals :Def28: :: ZF_LANG:def 28
H . 2;
coherence
H . 2 is Variable
proof end;
func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29
H . 3;
coherence
H . 3 is Variable
proof end;
end;

:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :
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;

theorem :: ZF_LANG:35
for H being ZF-formula st H is atomic holds
( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29;

theorem Th36: :: ZF_LANG:36
for H being ZF-formula st H is being_equality holds
H = (Var1 H) '=' (Var2 H)
proof end;

theorem Th37: :: ZF_LANG:37
for H being ZF-formula st H is being_membership holds
H = (Var1 H) 'in' (Var2 H)
proof end;

definition
let H be ZF-formula;
assume A1: H is negative ;
func the_argument_of H -> ZF-formula means :Def30: :: ZF_LANG:def 30
 'not' it = H;
existence
ex b1 being ZF-formula st 'not' b1 = H by A1;
uniqueness
for b1, b2 being ZF-formula st 'not' b1 = H & 'not' b2 = H holds
b1 = b2 by FINSEQ_1:33;
end;

:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :
for H being ZF-formula st H is negative holds
for b2 being ZF-formula holds
( b2 = the_argument_of H iff 'not' b2 = H );

definition
let H be ZF-formula;
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
( ( H is conjunctive implies ex b1, H1 being ZF-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st b1 'or' H1 = H ) ) by A1;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st b1 '&' H1 = H & ex H1 being ZF-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st b1 'or' H1 = H & ex H1 being ZF-formula st b2 'or' H1 = H implies b1 = b2 ) ) by Th30, Th31;
consistency
for b1 being ZF-formula holds verum ;
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
( ( H is conjunctive implies ex b1, H1 being ZF-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) ) by A1;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b1 = H & ex H1 being ZF-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b1 = H & ex H1 being ZF-formula st H1 'or' b2 = H implies b1 = b2 ) ) by Th30, Th31;
consistency
for b1 being ZF-formula holds verum ;
end;

:: 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 b2 being ZF-formula holds
( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 'or' H1 = H ) ) );

:: 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 b2 being ZF-formula holds
( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 'or' b2 = H ) ) );

theorem :: ZF_LANG:38
for F, H 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;

theorem Th39: :: ZF_LANG:39
for F, H 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 ) )
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)
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)
proof end;

definition
let H be ZF-formula;
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
( ( H is universal implies ex b1 being Variable ex H1 being ZF-formula st All (b1,H1) = H ) & ( not H is universal implies ex b1 being Variable ex H1 being ZF-formula st Ex (b1,H1) = H ) ) by A1;
uniqueness
for b1, b2 being Variable holds
( ( H is universal & ex H1 being ZF-formula st All (b1,H1) = H & ex H1 being ZF-formula st All (b2,H1) = H implies b1 = b2 ) & ( not H is universal & ex H1 being ZF-formula st Ex (b1,H1) = H & ex H1 being ZF-formula st Ex (b2,H1) = H implies b1 = b2 ) ) by Th3, Th34;
consistency
for b1 being Variable holds verum ;
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
( ( H is universal implies ex b1 being ZF-formula ex x being Variable st All (x,b1) = H ) & ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H ) ) by A1;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is universal & ex x being Variable st All (x,b1) = H & ex x being Variable st All (x,b2) = H implies b1 = b2 ) & ( not H is universal & ex x being Variable st Ex (x,b1) = H & ex x being Variable st Ex (x,b2) = H implies b1 = b2 ) ) by Th3, Th34;
consistency
for b1 being ZF-formula holds verum ;
end;

:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :
for H being ZF-formula st ( H is universal or H is existential ) holds
for b2 being Variable holds
( ( H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st All (b2,H1) = H ) ) & ( not H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st Ex (b2,H1) = H ) ) );

:: 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 b2 being ZF-formula holds
( ( H is universal implies ( b2 = the_scope_of H iff ex x being Variable st All (x,b2) = H ) ) & ( not H is universal implies ( b2 = the_scope_of H iff ex x being Variable st Ex (x,b2) = H ) ) );

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;

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

theorem Th44: :: ZF_LANG:44
for H being ZF-formula st H is universal holds
H = All ((bound_in H),(the_scope_of H))
proof end;

theorem :: ZF_LANG:45
for H being ZF-formula st H is existential holds
H = Ex ((bound_in H),(the_scope_of H))
proof end;

definition
let H be ZF-formula;
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 b1, H1 being ZF-formula st H = b1 => H1 by A1;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 => H1 & ex H1 being ZF-formula st H = b2 => H1 holds
b1 = b2 by Th32;
func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36
 ex H1 being ZF-formula st H = H1 => it;
existence
ex b1, H1 being ZF-formula st H = H1 => b1 by A1;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 => b1 & ex H1 being ZF-formula st H = H1 => b2 holds
b1 = b2 by Th32;
end;

:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :
for H being ZF-formula st H is conditional holds
for b2 being ZF-formula holds
( b2 = the_antecedent_of H iff ex H1 being ZF-formula st H = b2 => H1 );

:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :
for H being ZF-formula st H is conditional holds
for b2 being ZF-formula holds
( b2 = the_consequent_of H iff ex H1 being ZF-formula st H = H1 => b2 );

theorem :: ZF_LANG:46
for F, H 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;

theorem :: ZF_LANG:47
for H being ZF-formula st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
proof end;

definition
let H be ZF-formula;
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 b1, H1 being ZF-formula st H = b1 <=> H1 by A1;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 <=> H1 & ex H1 being ZF-formula st H = b2 <=> H1 holds
b1 = b2 by Th33;
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 b1, H1 being ZF-formula st H = H1 <=> b1 by A1;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 <=> b1 & ex H1 being ZF-formula st H = H1 <=> b2 holds
b1 = b2 by Th33;
end;

:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :
for H being ZF-formula st H is biconditional holds
for b2 being ZF-formula holds
( b2 = the_left_side_of H iff ex H1 being ZF-formula st H = b2 <=> H1 );

:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :
for H being ZF-formula st H is biconditional holds
for b2 being ZF-formula holds
( b2 = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b2 );

theorem :: ZF_LANG:48
for F, H 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;

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

::
:: The Immediate Constituents of ZF-formulae
::
definition
let H, F be ZF-formula;
pred H is_immediate_constituent_of F means :: 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) );
end;

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

theorem Th50: :: ZF_LANG:50
for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x '=' y
proof end;

theorem Th51: :: ZF_LANG:51
for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y
proof end;

theorem Th52: :: ZF_LANG:52
for F, H being ZF-formula holds
( F is_immediate_constituent_of 'not' H iff F = H )
proof end;

theorem Th53: :: ZF_LANG:53
for F, G, H being ZF-formula holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
proof end;

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

theorem :: ZF_LANG:55
for F, H being ZF-formula st H is atomic holds
not F is_immediate_constituent_of H
proof end;

theorem Th56: :: ZF_LANG:56
for F, H being ZF-formula st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
proof end;

theorem Th57: :: ZF_LANG:57
for F, H 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 ) )
proof end;

theorem Th58: :: ZF_LANG:58
for F, H being ZF-formula st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
proof end;

definition
let H, F be ZF-formula;
pred H is_subformula_of F means :: 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 ) ) );
end;

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

theorem Th59: :: ZF_LANG:59
for H being ZF-formula holds H is_subformula_of H
proof end;

definition
let H, F be ZF-formula;
pred H is_proper_subformula_of F means :: ZF_LANG:def 41
( H is_subformula_of F & H <> F );
end;

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

theorem Th60: :: ZF_LANG:60
for F, H being ZF-formula st H is_immediate_constituent_of F holds
len H < len F
proof end;

theorem Th61: :: ZF_LANG:61
for F, H being ZF-formula st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proof end;

theorem Th62: :: ZF_LANG:62
for F, H being ZF-formula st H is_proper_subformula_of F holds
len H < len F
proof end;

theorem Th63: :: ZF_LANG:63
for F, H being ZF-formula st H is_proper_subformula_of F holds
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
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
proof end;

theorem :: ZF_LANG:66
for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds
G = H
proof end;

theorem Th67: :: ZF_LANG:67
for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x '=' y
proof end;

theorem Th68: :: ZF_LANG:68
for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x 'in' y
proof end;

theorem Th69: :: ZF_LANG:69
for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds
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 )
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
proof end;

theorem :: ZF_LANG:72
for F, H being ZF-formula st H is atomic holds
not F is_proper_subformula_of H
proof end;

theorem :: ZF_LANG:73
for H being ZF-formula st H is negative holds
the_argument_of H is_proper_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 )
proof end;

theorem :: ZF_LANG:75
for H being ZF-formula st H is universal holds
the_scope_of H is_proper_subformula_of H
proof end;

theorem Th76: :: ZF_LANG:76
for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )
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 )
proof end;

::
:: The Set of Subformulae of ZF-formulae
::
definition
let H be ZF-formula;
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
ex b1 being set st
for a being set holds
( a in b1 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in b2 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :
for H being ZF-formula
for b2 being set holds
( b2 = Subformulae H iff for a being set holds
( a in b2 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) );

theorem Th78: :: ZF_LANG:78
for G, H being ZF-formula st G in Subformulae H holds
G is_subformula_of H
proof end;

theorem :: ZF_LANG:79
for F, H being ZF-formula st F is_subformula_of H holds
Subformulae F c= Subformulae H
proof end;

theorem Th80: :: ZF_LANG:80
for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)}
proof end;

theorem Th81: :: ZF_LANG:81
for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)}
proof end;

theorem Th82: :: ZF_LANG:82
for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
proof end;

theorem Th83: :: ZF_LANG:83
for F, H 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))}
proof end;

theorem :: ZF_LANG:85
for H being ZF-formula holds
( H is atomic iff Subformulae H = {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}
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}
proof end;

theorem :: ZF_LANG:88
for H being ZF-formula st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
proof end;

theorem :: ZF_LANG:89
for F, G, H 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
proof end;

::
:: The Structural Induction Schemes
::
scheme :: ZF_LANG:sch 1
ZFInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st H is atomic holds
P1[H] and
A2: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds
P1[H] and
A3: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H] and
A4: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds
P1[H]
proof end;

scheme :: ZF_LANG:sch 2
ZFCompInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P1[F] ) holds
P1[H]
proof end;