begin
:: deftheorem defines VAR ZF_LANG:def 1 :
VAR = { k where k is Element of NAT : 5 <= k } ;
:: deftheorem defines x. ZF_LANG:def 2 :
for n being Element of NAT holds x. n = 5 + n;
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: 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;
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
definition
func WFF -> non
empty set means :
Def8:
( ( 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 ) )
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
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 ) ) );
:: 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 );
theorem
canceled;
theorem
:: 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 );
:: 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 );
:: 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 );
:: 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 );
:: 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) );
theorem
canceled;
theorem
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;
:: 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 ) );
:: 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));
:: deftheorem defines <=> ZF_LANG:def 18 :
for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);
:: 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)));
:: 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 );
:: 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 );
:: 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 );
:: 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) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
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
All (
x,
(All (y,H)));
coherence
All (x,(All (y,H))) is ZF-formula
;
func Ex (
x,
y,
H)
-> ZF-formula equals
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
definition
let x,
y,
z be
Variable;
let H be
ZF-formula;
func All (
x,
y,
z,
H)
-> ZF-formula equals
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
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
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 Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
canceled;
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem
theorem
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
:: 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
theorem Th53:
theorem Th54:
:: 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:
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, Def13, Def20;
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 Th47, Th48;
consistency
for b1 being ZF-formula holds verum
;
func the_right_argument_of H -> ZF-formula means :
Def32:
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 ) )
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 Th47, Th48;
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
canceled;
theorem
theorem Th57:
theorem Th58:
theorem
definition
let H be
ZF-formula;
assume A1:
(
H is
universal or
H is
existential )
;
func bound_in H -> Variable means :
Def33:
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, Def14, Def23;
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 Th12, Th51;
consistency
for b1 being Variable holds verum
;
func the_scope_of H -> ZF-formula means :
Def34:
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 ) )
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 Th12, Th51;
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
theorem Th61:
theorem Th62:
theorem
:: 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
theorem
:: 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
theorem
:: 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) ) );
theorem
canceled;
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem
theorem Th75:
theorem Th76:
theorem Th77:
:: 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 ) ) ) );
theorem
canceled;
theorem Th79:
:: 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 ) );
theorem
canceled;
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem
theorem
theorem
theorem
theorem Th97:
theorem Th98:
:: 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
canceled;
theorem Th100:
theorem
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
theorem Th106:
theorem
theorem
theorem
theorem
theorem