ZF_LANG: A Model of ZF Set Theory Language

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines WFF ZF_LANG:def 8 :

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 :

registration

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

existence

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

proof end;

cluster x 'in' y -> ZF-formula-like ;

coherence

proof end;

end;

registration

let H be ZF-formula;

cluster 'not' H -> ZF-formula-like ;

coherence

proof end;

let G be ZF-formula;

cluster H '&' G -> ZF-formula-like ;

coherence

proof end;

end;

registration

let x be Variable;
let H be ZF-formula;

cluster All (x,H) -> ZF-formula-like ;

coherence

proof end;

end;

::
:: The Properties of ZF-formulae
::

definition

let H be ZF-formula;

attr H is being_equality means :Def10: :: ZF_LANG:def 10
ex x, y being Variable st H = x '=' y;

attr H is being_membership means :Def11: :: ZF_LANG:def 11
ex x, y being Variable st H = x 'in' y;

attr H is negative means :Def12: :: ZF_LANG:def 12
ex H1 being ZF-formula st H = 'not' H1;

attr H is conjunctive means :Def13: :: ZF_LANG:def 13
ex F, G being ZF-formula st H = F '&' G;

attr H is universal means :Def14: :: ZF_LANG:def 14
ex x being Variable ex H1 being ZF-formula st H = All (x,H1);

end;

:: deftheorem Def10 defines being_equality ZF_LANG:def 10 :

:: deftheorem Def11 defines being_membership ZF_LANG:def 11 :

:: deftheorem Def12 defines negative ZF_LANG:def 12 :

:: deftheorem Def13 defines conjunctive ZF_LANG:def 13 :

:: deftheorem Def14 defines universal ZF_LANG:def 14 :

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;

definition

let H be ZF-formula;

attr H is atomic means :Def15: :: ZF_LANG:def 15
( H is being_equality or H is being_membership );

end;

:: deftheorem Def15 defines atomic ZF_LANG:def 15 :

definition

let F, G be ZF-formula;

func F 'or' G -> ZF-formula equals :: ZF_LANG:def 16
'not' (('not' F) '&' ('not' G));

coherence ;

func F => G -> ZF-formula equals :: ZF_LANG:def 17
'not' (F '&' ('not' G));

coherence ;

end;

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

:: deftheorem defines => ZF_LANG:def 17 :

definition

let F, G be ZF-formula;

func F <=> G -> ZF-formula equals :: ZF_LANG:def 18
(F => G) '&' (G => F);

coherence ;

end;

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

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 ;

end;

:: deftheorem defines Ex ZF_LANG:def 19 :

definition

let H be ZF-formula;

attr H is disjunctive means :Def20: :: ZF_LANG:def 20
ex F, G being ZF-formula st H = F 'or' G;

attr H is conditional means :Def21: :: ZF_LANG:def 21
ex F, G being ZF-formula st H = F => G;

attr H is biconditional means :Def22: :: ZF_LANG:def 22
ex F, G being ZF-formula st H = F <=> G;

attr H is existential means :Def23: :: ZF_LANG:def 23
ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1);

end;

:: deftheorem Def20 defines disjunctive ZF_LANG:def 20 :

:: deftheorem Def21 defines conditional ZF_LANG:def 21 :

:: deftheorem Def22 defines biconditional ZF_LANG:def 22 :

:: deftheorem Def23 defines existential ZF_LANG:def 23 :

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;

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 ;

func Ex (x,y,H) -> ZF-formula equals :: ZF_LANG:def 25
Ex (x,(Ex (y,H)));

coherence ;

end;

:: deftheorem defines All ZF_LANG:def 24 :

:: deftheorem defines Ex ZF_LANG:def 25 :

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 ;

func Ex (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27
Ex (x,(Ex (y,z,H)));

coherence ;

end;

:: deftheorem defines All ZF_LANG:def 26 :

:: deftheorem defines Ex ZF_LANG:def 27 :

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 )

proof end;

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

proof end;

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 H, F being ZF-formula
for sq being FinSequence st H = F ^ sq holds
H = F

proof end;

theorem Th30: :: ZF_LANG:30

for H, G, H1, G1 being ZF-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )

proof end;

theorem Th31: :: ZF_LANG:31

for F, G, F1, 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, G, F1, G1 being ZF-formula st F => G = F1 => G1 holds
( F = F1 & G = G1 )

proof end;

theorem Th33: :: ZF_LANG:33

for F, G, F1, 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 H, G 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

proof end;

func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29
H . 3;

coherence

proof end;

end;

:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :

:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :

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 by A1, Def12;
uniqueness by FINSEQ_1:33;

end;

:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :

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 by A1, Def13, Def20;
uniqueness by Th30, Th31;
consistency ;

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

proof end;

uniqueness by Th30, Th31;
consistency ;

end;

:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def 31 :

:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def 32 :

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;

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

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 by A1, Def14, Def23;
uniqueness by Th3, Th34;
consistency ;

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

proof end;

uniqueness by Th3, Th34;
consistency ;

end;

:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :

:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :

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 by A1, Def21;
uniqueness 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

proof end;

uniqueness by Th32;

end;

:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :

:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :

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;

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 by A1, Def22;
uniqueness 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

proof end;

uniqueness by Th33;

end;

:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :

:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :

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;

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

end;

:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :

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 H, F being ZF-formula st H is atomic holds
not F is_immediate_constituent_of 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 )

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

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 )

proof end;

definition

let H, F be ZF-formula;

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

end;

:: deftheorem Def40 defines is_subformula_of ZF_LANG:def 40 :

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 :Def41: :: ZF_LANG:def 41
( H is_subformula_of F & H <> F );

end;

:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :

theorem Th60: :: ZF_LANG:60

for H, F being ZF-formula st H is_immediate_constituent_of F holds
len H < len F

proof end;

theorem Th61: :: ZF_LANG:61

for H, F 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 H, F being ZF-formula st H is_proper_subformula_of F holds
len H < len F

proof end;

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

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 H, F 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :

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

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

proof end;

::
:: The Structural Induction Schemes
::

scheme :: ZF_LANG:sch 1
ZFInd{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for H being ZF-formula st H is atomic holds
P₁[H] and
A2: for H being ZF-formula st H is negative & P₁[ the_argument_of H] holds
P₁[H] and
A3: for H being ZF-formula st H is conjunctive & P₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H] and
A4: for H being ZF-formula st H is universal & P₁[ the_scope_of H] holds
P₁[H]

proof end;

scheme :: ZF_LANG:sch 2
ZFCompInd{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P₁[F] ) holds
P₁[H]

proof end;