:: ZF_LANG semantic presentation

definition

func VAR -> Subset of NAT equals :: ZF_LANG:def 1
{ b₁ where B is Nat : 5 <= b₁ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines VAR ZF_LANG:def 1 :

registration

cluster VAR -> non empty ;
coherence

proof end;

end;

definition

mode Variable is Element of VAR ;

end;

definition

let c₁ be Nat;
func x. c₁ -> Variable equals :: ZF_LANG:def 2
5 + a₁;
coherence

proof end;

end;

:: deftheorem Def2 defines x. ZF_LANG:def 2 :

definition

let c₁ be Variable;
redefine func <* as <*c₁*> -> FinSequence of NAT ;
coherence

proof end;

end;

definition

let c₁, c₂ be Variable;
func c₁ '=' c₂ -> FinSequence of NAT equals :: ZF_LANG:def 3
(<*0*> ^ <*a₁*>) ^ <*a₂*>;
coherence ;
func c₁ 'in' c₂ -> FinSequence of NAT equals :: ZF_LANG:def 4
(<*1*> ^ <*a₁*>) ^ <*a₂*>;
coherence ;

end;

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

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

theorem Th1: :: ZF_LANG:1

canceled;

theorem Th2: :: ZF_LANG:2

canceled;

theorem Th3: :: ZF_LANG:3

canceled;

theorem Th4: :: ZF_LANG:4

canceled;

theorem Th5: :: ZF_LANG:5

canceled;

theorem Th6: :: ZF_LANG:6

for b₁, b₂, b₃, b₄ being Variable st b₁ '=' b₂ = b₃ '=' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th7: :: ZF_LANG:7

for b₁, b₂, b₃, b₄ being Variable st b₁ 'in' b₂ = b₃ 'in' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

definition

let c₁ be FinSequence of NAT ;
func 'not' c₁ -> FinSequence of NAT equals :: ZF_LANG:def 5
<*2*> ^ a₁;
coherence ;
let c₂ be FinSequence of NAT ;
func c₁ '&' c₂ -> FinSequence of NAT equals :: ZF_LANG:def 6
(<*3*> ^ a₁) ^ a₂;
coherence ;

end;

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

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

theorem Th8: :: ZF_LANG:8

canceled;

theorem Th9: :: ZF_LANG:9

canceled;

theorem Th10: :: ZF_LANG:10

for b₁, b₂ being FinSequence of NAT st 'not' b₁ = 'not' b₂ holds
b₁ = b₂ by FINSEQ_1:46;

definition

let c₁ be Variable;
let c₂ be FinSequence of NAT ;
func All c₁,c₂ -> FinSequence of NAT equals :: ZF_LANG:def 7
(<*4*> ^ <*a₁*>) ^ a₂;
coherence ;

end;

:: deftheorem Def7 defines All ZF_LANG:def 7 :

theorem Th11: :: ZF_LANG:11

canceled;

theorem Th12: :: ZF_LANG:12

for b₁, b₂ being FinSequence of NAT
for b₃, b₄ being Variable st All b₃,b₁ = All b₄,b₂ holds
( b₃ = b₄ & b₁ = b₂ )

proof end;

definition

func WFF -> non empty set means :Def8: :: ZF_LANG:def 8
( ( for b₁ being set st b₁ in a₁ holds
b₁ is FinSequence of NAT ) & ( for b₁, b₂ being Variable holds
( b₁ '=' b₂ in a₁ & b₁ 'in' b₂ in a₁ ) ) & ( for b₁ being FinSequence of NAT st b₁ in a₁ holds
'not' b₁ in a₁ ) & ( for b₁, b₂ being FinSequence of NAT st b₁ in a₁ & b₂ in a₁ holds
b₁ '&' b₂ in a₁ ) & ( for b₁ being Variable
for b₂ being FinSequence of NAT st b₂ in a₁ holds
All b₁,b₂ in a₁ ) & ( for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ is FinSequence of NAT ) & ( for b₂, b₃ being Variable holds
( b₂ '=' b₃ in b₁ & b₂ 'in' b₃ in b₁ ) ) & ( for b₂ being FinSequence of NAT st b₂ in b₁ holds
'not' b₂ in b₁ ) & ( for b₂, b₃ being FinSequence of NAT st b₂ in b₁ & b₃ in b₁ holds
b₂ '&' b₃ in b₁ ) & ( for b₂ being Variable
for b₃ being FinSequence of NAT st b₃ in b₁ holds
All b₂,b₃ in b₁ ) holds
a₁ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines WFF ZF_LANG:def 8 :

definition

let c₁ be FinSequence of NAT ;
attr a₁ is ZF-formula-like means :Def9: :: ZF_LANG:def 9
a₁ is Element of WFF ;

end;

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

registration

cluster ZF-formula-like FinSequence of NAT ;
existence

proof end;

end;

definition

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

end;

theorem Th13: :: ZF_LANG:13

canceled;

theorem Th14: :: ZF_LANG:14

for b₁ being set holds
( b₁ is ZF-formula iff b₁ in WFF )

proof end;

registration

let c₁, c₂ be Variable;
cluster a₁ '=' a₂ -> ZF-formula-like ;
coherence

proof end;

cluster a₁ 'in' a₂ -> ZF-formula-like ;
coherence

proof end;

end;

registration

let c₁ be ZF-formula;
cluster 'not' a₁ -> ZF-formula-like ;
coherence

proof end;

let c₂ be ZF-formula;
cluster a₁ '&' a₂ -> ZF-formula-like ;
coherence

proof end;

end;

registration

let c₁ be Variable;
let c₂ be ZF-formula;
cluster All a₁,a₂ -> ZF-formula-like ;
coherence

proof end;

end;

definition

let c₁ be ZF-formula;
attr a₁ is being_equality means :Def10: :: ZF_LANG:def 10
ex b₁, b₂ being Variable st a₁ = b₁ '=' b₂;
attr a₁ is being_membership means :Def11: :: ZF_LANG:def 11
ex b₁, b₂ being Variable st a₁ = b₁ 'in' b₂;
attr a₁ is negative means :Def12: :: ZF_LANG:def 12
ex b₁ being ZF-formula st a₁ = 'not' b₁;
attr a₁ is conjunctive means :Def13: :: ZF_LANG:def 13
ex b₁, b₂ being ZF-formula st a₁ = b₁ '&' b₂;
attr a₁ is universal means :Def14: :: ZF_LANG:def 14
ex b₁ being Variableex b₂ being ZF-formula st a₁ = All b₁,b₂;

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 :

notation

let c₁ be ZF-formula;
synonym c₁ is_equality for being_equality c₁;
synonym c₁ is_membership for being_membership c₁;

end;

theorem Th15: :: ZF_LANG:15

canceled;

theorem Th16: :: ZF_LANG:16

for b₁ being ZF-formula holds
( ( b₁ is_equality implies ex b₂, b₃ being Variable st b₁ = b₂ '=' b₃ ) & ( ex b₂, b₃ being Variable st b₁ = b₂ '=' b₃ implies b₁ is_equality ) & ( b₁ is_membership implies ex b₂, b₃ being Variable st b₁ = b₂ 'in' b₃ ) & ( ex b₂, b₃ being Variable st b₁ = b₂ 'in' b₃ implies b₁ is_membership ) & ( b₁ is negative implies ex b₂ being ZF-formula st b₁ = 'not' b₂ ) & ( ex b₂ being ZF-formula st b₁ = 'not' b₂ implies b₁ is negative ) & ( b₁ is conjunctive implies ex b₂, b₃ being ZF-formula st b₁ = b₂ '&' b₃ ) & ( ex b₂, b₃ being ZF-formula st b₁ = b₂ '&' b₃ implies b₁ is conjunctive ) & ( b₁ is universal implies ex b₂ being Variableex b₃ being ZF-formula st b₁ = All b₂,b₃ ) & ( ex b₂ being Variableex b₃ being ZF-formula st b₁ = All b₂,b₃ implies b₁ is universal ) ) by Def10, Def11, Def12, Def13, Def14;

definition

let c₁ be ZF-formula;
attr a₁ is atomic means :Def15: :: ZF_LANG:def 15
( a₁ is_equality or a₁ is_membership );

end;

:: deftheorem Def15 defines atomic ZF_LANG:def 15 :

definition

let c₁, c₂ be ZF-formula;
func c₁ 'or' c₂ -> ZF-formula equals :: ZF_LANG:def 16
'not' (('not' a₁) '&' ('not' a₂));
coherence ;
func c₁ => c₂ -> ZF-formula equals :: ZF_LANG:def 17
'not' (a₁ '&' ('not' a₂));
coherence ;

end;

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

:: deftheorem Def17 defines => ZF_LANG:def 17 :

definition

let c₁, c₂ be ZF-formula;
func c₁ <=> c₂ -> ZF-formula equals :: ZF_LANG:def 18
(a₁ => a₂) '&' (a₂ => a₁);
coherence ;

end;

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

definition

let c₁ be Variable;
let c₂ be ZF-formula;
func Ex c₁,c₂ -> ZF-formula equals :: ZF_LANG:def 19
'not' (All a₁,('not' a₂));
coherence ;

end;

:: deftheorem Def19 defines Ex ZF_LANG:def 19 :

definition

let c₁ be ZF-formula;
attr a₁ is disjunctive means :Def20: :: ZF_LANG:def 20
ex b₁, b₂ being ZF-formula st a₁ = b₁ 'or' b₂;
attr a₁ is conditional means :Def21: :: ZF_LANG:def 21
ex b₁, b₂ being ZF-formula st a₁ = b₁ => b₂;
attr a₁ is biconditional means :Def22: :: ZF_LANG:def 22
ex b₁, b₂ being ZF-formula st a₁ = b₁ <=> b₂;
attr a₁ is existential means :Def23: :: ZF_LANG:def 23
ex b₁ being Variableex b₂ being ZF-formula st a₁ = Ex b₁,b₂;

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 Th17: :: ZF_LANG:17

canceled;

theorem Th18: :: ZF_LANG:18

canceled;

theorem Th19: :: ZF_LANG:19

canceled;

theorem Th20: :: ZF_LANG:20

canceled;

theorem Th21: :: ZF_LANG:21

canceled;

theorem Th22: :: ZF_LANG:22

for b₁ being ZF-formula holds
( ( b₁ is disjunctive implies ex b₂, b₃ being ZF-formula st b₁ = b₂ 'or' b₃ ) & ( ex b₂, b₃ being ZF-formula st b₁ = b₂ 'or' b₃ implies b₁ is disjunctive ) & ( b₁ is conditional implies ex b₂, b₃ being ZF-formula st b₁ = b₂ => b₃ ) & ( ex b₂, b₃ being ZF-formula st b₁ = b₂ => b₃ implies b₁ is conditional ) & ( b₁ is biconditional implies ex b₂, b₃ being ZF-formula st b₁ = b₂ <=> b₃ ) & ( ex b₂, b₃ being ZF-formula st b₁ = b₂ <=> b₃ implies b₁ is biconditional ) & ( b₁ is existential implies ex b₂ being Variableex b₃ being ZF-formula st b₁ = Ex b₂,b₃ ) & ( ex b₂ being Variableex b₃ being ZF-formula st b₁ = Ex b₂,b₃ implies b₁ is existential ) ) by Def20, Def21, Def22, Def23;

definition

let c₁, c₂ be Variable;
let c₃ be ZF-formula;
func All c₁,c₂,c₃ -> ZF-formula equals :: ZF_LANG:def 24
All a₁,(All a₂,a₃);
coherence ;
func Ex c₁,c₂,c₃ -> ZF-formula equals :: ZF_LANG:def 25
Ex a₁,(Ex a₂,a₃);
coherence ;

end;

:: deftheorem Def24 defines All ZF_LANG:def 24 :

:: deftheorem Def25 defines Ex ZF_LANG:def 25 :

theorem Th23: :: ZF_LANG:23

for b₁, b₂ being Variable
for b₃ being ZF-formula holds
( All b₁,b₂,b₃ = All b₁,(All b₂,b₃) & Ex b₁,b₂,b₃ = Ex b₁,(Ex b₂,b₃) ) ;

definition

let c₁, c₂, c₃ be Variable;
let c₄ be ZF-formula;
func All c₁,c₂,c₃,c₄ -> ZF-formula equals :: ZF_LANG:def 26
All a₁,(All a₂,a₃,a₄);
coherence ;
func Ex c₁,c₂,c₃,c₄ -> ZF-formula equals :: ZF_LANG:def 27
Ex a₁,(Ex a₂,a₃,a₄);
coherence ;

end;

:: deftheorem Def26 defines All ZF_LANG:def 26 :

:: deftheorem Def27 defines Ex ZF_LANG:def 27 :

theorem Th24: :: ZF_LANG:24

for b₁, b₂, b₃ being Variable
for b₄ being ZF-formula holds
( All b₁,b₂,b₃,b₄ = All b₁,(All b₂,b₃,b₄) & Ex b₁,b₂,b₃,b₄ = Ex b₁,(Ex b₂,b₃,b₄) ) ;

theorem Th25: :: ZF_LANG:25

for b₁ being ZF-formula holds
( b₁ is_equality or b₁ is_membership or b₁ is negative or b₁ is conjunctive or b₁ is universal )

proof end;

theorem Th26: :: ZF_LANG:26

for b₁ being ZF-formula holds
( b₁ is atomic or b₁ is negative or b₁ is conjunctive or b₁ is universal )

proof end;

theorem Th27: :: ZF_LANG:27

for b₁ being ZF-formula st b₁ is atomic holds
len b₁ = 3

proof end;

theorem Th28: :: ZF_LANG:28

for b₁ being ZF-formula holds
( b₁ is atomic or ex b₂ being ZF-formula st (len b₂) + 1 <= len b₁ )

proof end;

theorem Th29: :: ZF_LANG:29

for b₁ being ZF-formula holds 3 <= len b₁

proof end;

theorem Th30: :: ZF_LANG:30

for b₁ being ZF-formula st len b₁ = 3 holds
b₁ is atomic

proof end;

theorem Th31: :: ZF_LANG:31

for b₁, b₂ being Variable holds
( (b₁ '=' b₂) . 1 = 0 & (b₁ 'in' b₂) . 1 = 1 )

proof end;

theorem Th32: :: ZF_LANG:32

for b₁ being ZF-formula holds ('not' b₁) . 1 = 2 by FINSEQ_1:58;

theorem Th33: :: ZF_LANG:33

for b₁, b₂ being ZF-formula holds (b₁ '&' b₂) . 1 = 3

proof end;

theorem Th34: :: ZF_LANG:34

for b₁ being Variable
for b₂ being ZF-formula holds (All b₁,b₂) . 1 = 4

proof end;

theorem Th35: :: ZF_LANG:35

for b₁ being ZF-formula st b₁ is_equality holds
b₁ . 1 = 0

proof end;

theorem Th36: :: ZF_LANG:36

for b₁ being ZF-formula st b₁ is_membership holds
b₁ . 1 = 1

proof end;

theorem Th37: :: ZF_LANG:37

for b₁ being ZF-formula st b₁ is negative holds
b₁ . 1 = 2

proof end;

theorem Th38: :: ZF_LANG:38

for b₁ being ZF-formula st b₁ is conjunctive holds
b₁ . 1 = 3

proof end;

theorem Th39: :: ZF_LANG:39

for b₁ being ZF-formula st b₁ is universal holds
b₁ . 1 = 4

proof end;

theorem Th40: :: ZF_LANG:40

for b₁ being ZF-formula holds
( ( b₁ is_equality & b₁ . 1 = 0 ) or ( b₁ is_membership & b₁ . 1 = 1 ) or ( b₁ is negative & b₁ . 1 = 2 ) or ( b₁ is conjunctive & b₁ . 1 = 3 ) or ( b₁ is universal & b₁ . 1 = 4 ) )

proof end;

theorem Th41: :: ZF_LANG:41

for b₁ being ZF-formula st b₁ . 1 = 0 holds
b₁ is_equality by Th40;

theorem Th42: :: ZF_LANG:42

for b₁ being ZF-formula st b₁ . 1 = 1 holds
b₁ is_membership by Th40;

theorem Th43: :: ZF_LANG:43

for b₁ being ZF-formula st b₁ . 1 = 2 holds
b₁ is negative by Th40;

theorem Th44: :: ZF_LANG:44

for b₁ being ZF-formula st b₁ . 1 = 3 holds
b₁ is conjunctive by Th40;

theorem Th45: :: ZF_LANG:45

for b₁ being ZF-formula st b₁ . 1 = 4 holds
b₁ is universal by Th40;

theorem Th46: :: ZF_LANG:46

for b₁, b₂ being ZF-formula
for b₃ being FinSequence st b₁ = b₂ ^ b₃ holds
b₁ = b₂

proof end;

theorem Th47: :: ZF_LANG:47

for b₁, b₂, b₃, b₄ being ZF-formula st b₁ '&' b₂ = b₃ '&' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th48: :: ZF_LANG:48

for b₁, b₂, b₃, b₄ being ZF-formula st b₁ 'or' b₂ = b₃ 'or' b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th49: :: ZF_LANG:49

for b₁, b₂, b₃, b₄ being ZF-formula st b₁ => b₂ = b₃ => b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th50: :: ZF_LANG:50

for b₁, b₂, b₃, b₄ being ZF-formula st b₁ <=> b₂ = b₃ <=> b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th51: :: ZF_LANG:51

for b₁, b₂ being Variable
for b₃, b₄ being ZF-formula st Ex b₁,b₃ = Ex b₂,b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

definition

let c₁ be ZF-formula;
assume E36: c₁ is atomic ;
func Var1 c₁ -> Variable equals :Def28: :: ZF_LANG:def 28
a₁ . 2;
coherence

proof end;

func Var2 c₁ -> Variable equals :Def29: :: ZF_LANG:def 29
a₁ . 3;
coherence

proof end;

end;

:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :

:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :

theorem Th52: :: ZF_LANG:52

for b₁ being ZF-formula st b₁ is atomic holds
( Var1 b₁ = b₁ . 2 & Var2 b₁ = b₁ . 3 ) by Def28, Def29;

theorem Th53: :: ZF_LANG:53

for b₁ being ZF-formula st b₁ is_equality holds
b₁ = (Var1 b₁) '=' (Var2 b₁)

proof end;

theorem Th54: :: ZF_LANG:54

for b₁ being ZF-formula st b₁ is_membership holds
b₁ = (Var1 b₁) 'in' (Var2 b₁)

proof end;

definition

let c₁ be ZF-formula;
assume E40: c₁ is negative ;
func the_argument_of c₁ -> ZF-formula means :Def30: :: ZF_LANG:def 30
'not' a₂ = a₁;
existence by E40, Def12;
uniqueness by Th10;

end;

:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :

definition

let c₁ be ZF-formula;
assume E41: ( c₁ is conjunctive or c₁ is disjunctive ) ;
func the_left_argument_of c₁ -> ZF-formula means :Def31: :: ZF_LANG:def 31
ex b₁ being ZF-formula st a₂ '&' b₁ = a₁ if a₁ is conjunctive
otherwise ex b₁ being ZF-formula st a₂ 'or' b₁ = a₁;
existence by E41, Def13, Def20;
uniqueness by Th47, Th48;
consistency ;
func the_right_argument_of c₁ -> ZF-formula means :Def32: :: ZF_LANG:def 32
ex b₁ being ZF-formula st b₁ '&' a₂ = a₁ if a₁ is conjunctive
otherwise ex b₁ being ZF-formula st b₁ 'or' a₂ = a₁;
existence

proof end;

uniqueness by Th47, Th48;
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 Th55: :: ZF_LANG:55

canceled;

theorem Th56: :: ZF_LANG:56

for b₁, b₂ being ZF-formula st b₁ is conjunctive holds
( ( b₂ = the_left_argument_of b₁ implies ex b₃ being ZF-formula st b₂ '&' b₃ = b₁ ) & ( ex b₃ being ZF-formula st b₂ '&' b₃ = b₁ implies b₂ = the_left_argument_of b₁ ) & ( b₂ = the_right_argument_of b₁ implies ex b₃ being ZF-formula st b₃ '&' b₂ = b₁ ) & ( ex b₃ being ZF-formula st b₃ '&' b₂ = b₁ implies b₂ = the_right_argument_of b₁ ) ) by Def31, Def32;

theorem Th57: :: ZF_LANG:57

for b₁, b₂ being ZF-formula st b₁ is disjunctive holds
( ( b₂ = the_left_argument_of b₁ implies ex b₃ being ZF-formula st b₂ 'or' b₃ = b₁ ) & ( ex b₃ being ZF-formula st b₂ 'or' b₃ = b₁ implies b₂ = the_left_argument_of b₁ ) & ( b₂ = the_right_argument_of b₁ implies ex b₃ being ZF-formula st b₃ 'or' b₂ = b₁ ) & ( ex b₃ being ZF-formula st b₃ 'or' b₂ = b₁ implies b₂ = the_right_argument_of b₁ ) )

proof end;

theorem Th58: :: ZF_LANG:58

for b₁ being ZF-formula st b₁ is conjunctive holds
b₁ = (the_left_argument_of b₁) '&' (the_right_argument_of b₁)

proof end;

theorem Th59: :: ZF_LANG:59

for b₁ being ZF-formula st b₁ is disjunctive holds
b₁ = (the_left_argument_of b₁) 'or' (the_right_argument_of b₁)

proof end;

definition

let c₁ be ZF-formula;
assume E45: ( c₁ is universal or c₁ is existential ) ;
func bound_in c₁ -> Variable means :Def33: :: ZF_LANG:def 33
ex b₁ being ZF-formula st All a₂,b₁ = a₁ if a₁ is universal
otherwise ex b₁ being ZF-formula st Ex a₂,b₁ = a₁;
existence by E45, Def14, Def23;
uniqueness by Th12, Th51;
consistency ;
func the_scope_of c₁ -> ZF-formula means :Def34: :: ZF_LANG:def 34
ex b₁ being Variable st All b₁,a₂ = a₁ if a₁ is universal
otherwise ex b₁ being Variable st Ex b₁,a₂ = a₁;
existence

proof end;

uniqueness by Th12, Th51;
consistency ;

end;

:: deftheorem Def33 defines bound_in ZF_LANG:def 33 :

:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :

theorem Th60: :: ZF_LANG:60

for b₁ being Variable
for b₂, b₃ being ZF-formula st b₂ is universal holds
( ( b₁ = bound_in b₂ implies ex b₄ being ZF-formula st All b₁,b₄ = b₂ ) & ( ex b₄ being ZF-formula st All b₁,b₄ = b₂ implies b₁ = bound_in b₂ ) & ( b₃ = the_scope_of b₂ implies ex b₄ being Variable st All b₄,b₃ = b₂ ) & ( ex b₄ being Variable st All b₄,b₃ = b₂ implies b₃ = the_scope_of b₂ ) ) by Def33, Def34;

theorem Th61: :: ZF_LANG:61

for b₁ being Variable
for b₂, b₃ being ZF-formula st b₂ is existential holds
( ( b₁ = bound_in b₂ implies ex b₄ being ZF-formula st Ex b₁,b₄ = b₂ ) & ( ex b₄ being ZF-formula st Ex b₁,b₄ = b₂ implies b₁ = bound_in b₂ ) & ( b₃ = the_scope_of b₂ implies ex b₄ being Variable st Ex b₄,b₃ = b₂ ) & ( ex b₄ being Variable st Ex b₄,b₃ = b₂ implies b₃ = the_scope_of b₂ ) )

proof end;

theorem Th62: :: ZF_LANG:62

for b₁ being ZF-formula st b₁ is universal holds
b₁ = All (bound_in b₁),(the_scope_of b₁)

proof end;

theorem Th63: :: ZF_LANG:63

for b₁ being ZF-formula st b₁ is existential holds
b₁ = Ex (bound_in b₁),(the_scope_of b₁)

proof end;

definition

let c₁ be ZF-formula;
assume E49: c₁ is conditional ;
func the_antecedent_of c₁ -> ZF-formula means :Def35: :: ZF_LANG:def 35
ex b₁ being ZF-formula st a₁ = a₂ => b₁;
existence by E49, Def21;
uniqueness by Th49;
func the_consequent_of c₁ -> ZF-formula means :Def36: :: ZF_LANG:def 36
ex b₁ being ZF-formula st a₁ = b₁ => a₂;
existence

proof end;

uniqueness by Th49;

end;

:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :

:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :

theorem Th64: :: ZF_LANG:64

for b₁, b₂ being ZF-formula st b₁ is conditional holds
( ( b₂ = the_antecedent_of b₁ implies ex b₃ being ZF-formula st b₁ = b₂ => b₃ ) & ( ex b₃ being ZF-formula st b₁ = b₂ => b₃ implies b₂ = the_antecedent_of b₁ ) & ( b₂ = the_consequent_of b₁ implies ex b₃ being ZF-formula st b₁ = b₃ => b₂ ) & ( ex b₃ being ZF-formula st b₁ = b₃ => b₂ implies b₂ = the_consequent_of b₁ ) ) by Def35, Def36;

theorem Th65: :: ZF_LANG:65

for b₁ being ZF-formula st b₁ is conditional holds
b₁ = (the_antecedent_of b₁) => (the_consequent_of b₁)

proof end;

definition

let c₁ be ZF-formula;
assume E51: c₁ is biconditional ;
func the_left_side_of c₁ -> ZF-formula means :Def37: :: ZF_LANG:def 37
ex b₁ being ZF-formula st a₁ = a₂ <=> b₁;
existence by E51, Def22;
uniqueness by Th50;
func the_right_side_of c₁ -> ZF-formula means :Def38: :: ZF_LANG:def 38
ex b₁ being ZF-formula st a₁ = b₁ <=> a₂;
existence

proof end;

uniqueness by Th50;

end;

:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :

:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :

theorem Th66: :: ZF_LANG:66

for b₁, b₂ being ZF-formula st b₁ is biconditional holds
( ( b₂ = the_left_side_of b₁ implies ex b₃ being ZF-formula st b₁ = b₂ <=> b₃ ) & ( ex b₃ being ZF-formula st b₁ = b₂ <=> b₃ implies b₂ = the_left_side_of b₁ ) & ( b₂ = the_right_side_of b₁ implies ex b₃ being ZF-formula st b₁ = b₃ <=> b₂ ) & ( ex b₃ being ZF-formula st b₁ = b₃ <=> b₂ implies b₂ = the_right_side_of b₁ ) ) by Def37, Def38;

theorem Th67: :: ZF_LANG:67

for b₁ being ZF-formula st b₁ is biconditional holds
b₁ = (the_left_side_of b₁) <=> (the_right_side_of b₁)

proof end;

definition

let c₁, c₂ be ZF-formula;
pred c₁ is_immediate_constituent_of c₂ means :Def39: :: ZF_LANG:def 39
( a₂ = 'not' a₁ or ex b₁ being ZF-formula st
( a₂ = a₁ '&' b₁ or a₂ = b₁ '&' a₁ ) or ex b₁ being Variable st a₂ = All b₁,a₁ );

end;

:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :

theorem Th68: :: ZF_LANG:68

canceled;

theorem Th69: :: ZF_LANG:69

for b₁, b₂ being Variable
for b₃ being ZF-formula holds not b₃ is_immediate_constituent_of b₁ '=' b₂

proof end;

theorem Th70: :: ZF_LANG:70

for b₁, b₂ being Variable
for b₃ being ZF-formula holds not b₃ is_immediate_constituent_of b₁ 'in' b₂

proof end;

theorem Th71: :: ZF_LANG:71

for b₁, b₂ being ZF-formula holds
( b₁ is_immediate_constituent_of 'not' b₂ iff b₁ = b₂ )

proof end;

theorem Th72: :: ZF_LANG:72

for b₁, b₂, b₃ being ZF-formula holds
( b₁ is_immediate_constituent_of b₂ '&' b₃ iff ( b₁ = b₂ or b₁ = b₃ ) )

proof end;

theorem Th73: :: ZF_LANG:73

for b₁ being Variable
for b₂, b₃ being ZF-formula holds
( b₂ is_immediate_constituent_of All b₁,b₃ iff b₂ = b₃ )

proof end;

theorem Th74: :: ZF_LANG:74

for b₁, b₂ being ZF-formula st b₁ is atomic holds
not b₂ is_immediate_constituent_of b₁

proof end;

theorem Th75: :: ZF_LANG:75

for b₁, b₂ being ZF-formula st b₁ is negative holds
( b₂ is_immediate_constituent_of b₁ iff b₂ = the_argument_of b₁ )

proof end;

theorem Th76: :: ZF_LANG:76

for b₁, b₂ being ZF-formula st b₁ is conjunctive holds
( b₂ is_immediate_constituent_of b₁ iff ( b₂ = the_left_argument_of b₁ or b₂ = the_right_argument_of b₁ ) )

proof end;

theorem Th77: :: ZF_LANG:77

for b₁, b₂ being ZF-formula st b₁ is universal holds
( b₂ is_immediate_constituent_of b₁ iff b₂ = the_scope_of b₁ )

proof end;

definition

let c₁, c₂ be ZF-formula;
pred c₁ is_subformula_of c₂ means :Def40: :: ZF_LANG:def 40
ex b₁ being Natex b₂ being FinSequence st
( 1 <= b₁ & len b₂ = b₁ & b₂ . 1 = a₁ & b₂ . b₁ = a₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ < b₁ holds
ex b₄, b₅ being ZF-formula st
( b₂ . b₃ = b₄ & b₂ . (b₃ + 1) = b₅ & b₄ is_immediate_constituent_of b₅ ) ) );

end;

:: deftheorem Def40 defines is_subformula_of ZF_LANG:def 40 :

theorem Th78: :: ZF_LANG:78

canceled;

theorem Th79: :: ZF_LANG:79

for b₁ being ZF-formula holds b₁ is_subformula_of b₁

proof end;

definition

let c₁, c₂ be ZF-formula;
pred c₁ is_proper_subformula_of c₂ means :Def41: :: ZF_LANG:def 41
( a₁ is_subformula_of a₂ & a₁ <> a₂ );

end;

:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :

theorem Th80: :: ZF_LANG:80

canceled;

theorem Th81: :: ZF_LANG:81

for b₁, b₂ being ZF-formula st b₁ is_immediate_constituent_of b₂ holds
len b₁ < len b₂

proof end;

theorem Th82: :: ZF_LANG:82

for b₁, b₂ being ZF-formula st b₁ is_immediate_constituent_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th83: :: ZF_LANG:83

for b₁, b₂ being ZF-formula st b₁ is_proper_subformula_of b₂ holds
len b₁ < len b₂

proof end;

theorem Th84: :: ZF_LANG:84

for b₁, b₂ being ZF-formula st b₁ is_proper_subformula_of b₂ holds
ex b₃ being ZF-formula st b₃ is_immediate_constituent_of b₂

proof end;

theorem Th85: :: ZF_LANG:85

for b₁, b₂, b₃ being ZF-formula st b₁ is_proper_subformula_of b₂ & b₂ is_proper_subformula_of b₃ holds
b₁ is_proper_subformula_of b₃

proof end;

theorem Th86: :: ZF_LANG:86

for b₁, b₂, b₃ being ZF-formula st b₁ is_subformula_of b₂ & b₂ is_subformula_of b₃ holds
b₁ is_subformula_of b₃

proof end;

theorem Th87: :: ZF_LANG:87

for b₁, b₂ being ZF-formula st b₁ is_subformula_of b₂ & b₂ is_subformula_of b₁ holds
b₁ = b₂

proof end;

theorem Th88: :: ZF_LANG:88

for b₁, b₂ being Variable
for b₃ being ZF-formula holds not b₃ is_proper_subformula_of b₁ '=' b₂

proof end;

theorem Th89: :: ZF_LANG:89

for b₁, b₂ being Variable
for b₃ being ZF-formula holds not b₃ is_proper_subformula_of b₁ 'in' b₂

proof end;

theorem Th90: :: ZF_LANG:90

for b₁, b₂ being ZF-formula st b₁ is_proper_subformula_of 'not' b₂ holds
b₁ is_subformula_of b₂

proof end;

theorem Th91: :: ZF_LANG:91

for b₁, b₂, b₃ being ZF-formula holds
( not b₁ is_proper_subformula_of b₂ '&' b₃ or b₁ is_subformula_of b₂ or b₁ is_subformula_of b₃ )

proof end;

theorem Th92: :: ZF_LANG:92

for b₁ being Variable
for b₂, b₃ being ZF-formula st b₂ is_proper_subformula_of All b₁,b₃ holds
b₂ is_subformula_of b₃

proof end;

theorem Th93: :: ZF_LANG:93

for b₁, b₂ being ZF-formula st b₁ is atomic holds
not b₂ is_proper_subformula_of b₁

proof end;

theorem Th94: :: ZF_LANG:94

for b₁ being ZF-formula st b₁ is negative holds
the_argument_of b₁ is_proper_subformula_of b₁

proof end;

theorem Th95: :: ZF_LANG:95

for b₁ being ZF-formula st b₁ is conjunctive holds
( the_left_argument_of b₁ is_proper_subformula_of b₁ & the_right_argument_of b₁ is_proper_subformula_of b₁ )

proof end;

theorem Th96: :: ZF_LANG:96

for b₁ being ZF-formula st b₁ is universal holds
the_scope_of b₁ is_proper_subformula_of b₁

proof end;

theorem Th97: :: ZF_LANG:97

for b₁, b₂ being Variable
for b₃ being ZF-formula holds
( b₃ is_subformula_of b₁ '=' b₂ iff b₃ = b₁ '=' b₂ )

proof end;

theorem Th98: :: ZF_LANG:98

for b₁, b₂ being Variable
for b₃ being ZF-formula holds
( b₃ is_subformula_of b₁ 'in' b₂ iff b₃ = b₁ 'in' b₂ )

proof end;

definition

let c₁ be ZF-formula;
func Subformulae c₁ -> set means :Def42: :: ZF_LANG:def 42
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being ZF-formula st
( b₂ = b₁ & b₂ is_subformula_of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :

theorem Th99: :: ZF_LANG:99

canceled;

theorem Th100: :: ZF_LANG:100

for b₁, b₂ being ZF-formula st b₁ in Subformulae b₂ holds
b₁ is_subformula_of b₂

proof end;

theorem Th101: :: ZF_LANG:101

for b₁, b₂ being ZF-formula st b₁ is_subformula_of b₂ holds
Subformulae b₁ c= Subformulae b₂

proof end;

theorem Th102: :: ZF_LANG:102

for b₁, b₂ being Variable holds Subformulae (b₁ '=' b₂) = {(b₁ '=' b₂)}

proof end;

theorem Th103: :: ZF_LANG:103

for b₁, b₂ being Variable holds Subformulae (b₁ 'in' b₂) = {(b₁ 'in' b₂)}

proof end;

theorem Th104: :: ZF_LANG:104

for b₁ being ZF-formula holds Subformulae ('not' b₁) = (Subformulae b₁) \/ {('not' b₁)}

proof end;

theorem Th105: :: ZF_LANG:105

for b₁, b₂ being ZF-formula holds Subformulae (b₁ '&' b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {(b₁ '&' b₂)}

proof end;

theorem Th106: :: ZF_LANG:106

for b₁ being Variable
for b₂ being ZF-formula holds Subformulae (All b₁,b₂) = (Subformulae b₂) \/ {(All b₁,b₂)}

proof end;

theorem Th107: :: ZF_LANG:107

for b₁ being ZF-formula holds
( b₁ is atomic iff Subformulae b₁ = {b₁} )

proof end;

theorem Th108: :: ZF_LANG:108

for b₁ being ZF-formula st b₁ is negative holds
Subformulae b₁ = (Subformulae (the_argument_of b₁)) \/ {b₁}

proof end;

theorem Th109: :: ZF_LANG:109

for b₁ being ZF-formula st b₁ is conjunctive holds
Subformulae b₁ = ((Subformulae (the_left_argument_of b₁)) \/ (Subformulae (the_right_argument_of b₁))) \/ {b₁}

proof end;

theorem Th110: :: ZF_LANG:110

for b₁ being ZF-formula st b₁ is universal holds
Subformulae b₁ = (Subformulae (the_scope_of b₁)) \/ {b₁}

proof end;

theorem Th111: :: ZF_LANG:111

for b₁, b₂, b₃ being ZF-formula st ( b₁ is_immediate_constituent_of b₂ or b₁ is_proper_subformula_of b₂ or b₁ is_subformula_of b₂ ) & b₂ in Subformulae b₃ holds
b₁ in Subformulae b₃

proof end;

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

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

provided

E85: for b₁ being ZF-formula st b₁ is atomic holds
P₁[b₁] and
E86: for b₁ being ZF-formula st b₁ is negative & P₁[ the_argument_of b₁] holds
P₁[b₁] and
E87: for b₁ being ZF-formula st b₁ is conjunctive & P₁[ the_left_argument_of b₁] & P₁[ the_right_argument_of b₁] holds
P₁[b₁] and
E88: for b₁ being ZF-formula st b₁ is universal & P₁[ the_scope_of b₁] holds
P₁[b₁]

proof end;

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

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

provided

E85: for b₁ being ZF-formula st ( for b₂ being ZF-formula st b₂ is_proper_subformula_of b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;