begin
:: deftheorem defines VAR ZF_LANG:def 1 :
:: deftheorem defines x. ZF_LANG:def 2 :
:: deftheorem defines '=' ZF_LANG:def 3 :
:: deftheorem defines 'in' ZF_LANG:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem defines 'not' ZF_LANG:def 5 :
:: deftheorem defines '&' ZF_LANG:def 6 :
:: deftheorem defines All ZF_LANG:def 7 :
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 :
:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def 9 :
theorem
canceled;
theorem
:: 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
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 :
:: deftheorem defines 'or' ZF_LANG:def 16 :
:: deftheorem defines => ZF_LANG:def 17 :
:: deftheorem defines <=> ZF_LANG:def 18 :
:: deftheorem defines Ex ZF_LANG:def 19 :
:: 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
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 :
:: deftheorem defines Ex ZF_LANG:def 25 :
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 :
:: deftheorem defines Ex ZF_LANG:def 27 :
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 :
:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :
theorem
theorem Th53:
theorem Th54:
:: 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:
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 :
:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def 32 :
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 :
:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :
theorem
theorem Th61:
theorem Th62:
theorem
:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def 35 :
:: deftheorem Def36 defines the_consequent_of ZF_LANG:def 36 :
theorem
theorem
:: deftheorem Def37 defines the_left_side_of ZF_LANG:def 37 :
:: deftheorem Def38 defines the_right_side_of ZF_LANG:def 38 :
theorem
theorem
:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def 39 :
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 :
theorem
canceled;
theorem Th79:
:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def 41 :
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 :
theorem
canceled;
theorem Th100:
theorem
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
theorem Th106:
theorem
theorem
theorem
theorem
theorem