:: Replacing of Variables in Formulas of ZF Theory
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZF_LANG, XBOOLEAN, XXREAL_0, BVFUNC_2, CLASSES2,
FUNCT_1, CARD_1, FINSEQ_1, ARYTM_3, TARSKI, XBOOLE_0, ZF_MODEL, SUBSET_1,
REALSET1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, ZFMISC_1, ORDINAL4,
ZF_LANG1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG,
ZF_MODEL, XXREAL_0, FUNCT_7, TREES_3;
constructors ENUMSET1, XXREAL_0, XREAL_0, NAT_1, ZF_MODEL, FUNCT_7, RELSET_1,
NUMBERS, TREES_3;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
NAT_1, FINSEQ_1, ZF_LANG, XCMPLX_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ZF_LANG, ZF_MODEL, XBOOLE_0;
equalities ZF_LANG;
expansions TARSKI, ZF_LANG, ZF_MODEL;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, FINSEQ_1, FINSEQ_3, FUNCT_1,
FUNCT_2, ZF_LANG, ZF_MODEL, ZFMODEL1, RELSET_1, XBOOLE_0, XBOOLE_1,
XXREAL_0, ORDINAL1, FUNCT_7, RELAT_1;
schemes PARTFUN1, ZF_LANG;
begin
reserve p,p1,p2,q,r,F,G,G1,G2,H,H1,H2 for ZF-formula,
x,x1,x2,y,y1,y2,z,z1,z2,s,t for Variable,
a,X for set;
theorem Th1:
Var1 (x '=' y) = x & Var2 (x '=' y) = y
proof
x '=' y is being_equality;
then x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:36;
hence thesis by ZF_LANG:1;
end;
theorem Th2:
Var1 (x 'in' y) = x & Var2 (x 'in' y) = y
proof
x 'in' y is being_membership;
then x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:37;
hence thesis by ZF_LANG:2;
end;
theorem Th3:
the_argument_of 'not' p = p
proof
'not' p is negative;
hence thesis by ZF_LANG:def 30;
end;
theorem Th4:
the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q
proof
p '&' q is conjunctive;
then
p '&' q = (the_left_argument_of (p '&' q)) '&' (the_right_argument_of (p
'&' q)) by ZF_LANG:40;
hence thesis by ZF_LANG:30;
end;
theorem
the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q
proof
p 'or' q is disjunctive;
then
p 'or' q = (the_left_argument_of (p 'or' q)) 'or' (the_right_argument_of
(p 'or' q)) by ZF_LANG:41;
hence thesis by ZF_LANG:31;
end;
theorem Th6:
the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q
proof
p => q is conditional;
then
p => q = (the_antecedent_of (p => q)) => (the_consequent_of (p => q)) by
ZF_LANG:47;
hence thesis by ZF_LANG:32;
end;
theorem
the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q
proof
p <=> q is biconditional;
then
p <=> q = (the_left_side_of (p <=> q)) <=> (the_right_side_of (p <=> q))
by ZF_LANG:49;
hence thesis by ZF_LANG:33;
end;
theorem Th8:
bound_in All(x,p) = x & the_scope_of All(x,p) = p
proof
All(x,p) is universal;
then All(x,p) = All(bound_in All(x,p), the_scope_of All(x,p)) by ZF_LANG:44;
hence thesis by ZF_LANG:3;
end;
theorem Th9:
bound_in Ex(x,p) = x & the_scope_of Ex(x,p) = p
proof
Ex(x,p) is existential;
then Ex(x,p) = Ex(bound_in Ex(x,p), the_scope_of Ex(x,p)) by ZF_LANG:45;
hence thesis by ZF_LANG:34;
end;
theorem
p 'or' q = 'not' p => q;
theorem
All(x,y,p) is universal & bound_in All(x,y,p) = x & the_scope_of All(x
,y,p) = All(y,p) by Th8;
theorem
Ex(x,y,p) is existential & bound_in Ex(x,y,p) = x & the_scope_of Ex(x,
y,p) = Ex(y,p) by Th9;
theorem
All(x,y,z,p) = All(x,All(y,All(z,p))) & All(x,y,z,p) = All(x,y,All(z,p ));
theorem Th14:
All(x1,y1,p1) = All(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2
proof
assume
A1: All(x1,y1,p1) = All(x2,y2,p2);
then All(y1,p1) = All(y2,p2) by ZF_LANG:3;
hence thesis by A1,ZF_LANG:3;
end;
theorem
All(x1,y1,z1,p1) = All(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 =
z2 & p1 = p2
proof
assume
A1: All(x1,y1,z1,p1) = All(x2,y2,z2,p2);
then All(y1,z1,p1) = All(y2,z2,p2) by ZF_LANG:3;
hence thesis by A1,Th14,ZF_LANG:3;
end;
theorem
All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q
proof
All(x,y,z,p) = All(x,y,All(z,p));
hence thesis by Th14;
end;
theorem Th17:
Ex(x1,y1,p1) = Ex(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2
proof
assume
A1: Ex(x1,y1,p1) = Ex(x2,y2,p2);
then Ex(y1,p1) = Ex(y2,p2) by ZF_LANG:34;
hence thesis by A1,ZF_LANG:34;
end;
theorem
Ex(x,y,z,p) = Ex(x,Ex(y,Ex(z,p))) & Ex(x,y,z,p) = Ex(x,y,Ex(z,p));
theorem
Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 = z2
& p1 = p2
proof
assume
A1: Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2);
then Ex(y1,z1,p1) = Ex(y2,z2,p2) by ZF_LANG:34;
hence thesis by A1,Th17,ZF_LANG:34;
end;
theorem
Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q
proof
Ex(x,y,z,p) = Ex(x,y,Ex(z,p));
hence thesis by Th17;
end;
theorem
All(x,y,z,p) is universal & bound_in All(x,y,z,p) = x & the_scope_of
All(x,y,z,p) = All(y,z,p) by Th8;
theorem
Ex(x,y,z,p) is existential & bound_in Ex(x,y,z,p) = x & the_scope_of
Ex(x,y,z,p) = Ex(y,z,p) by Th9;
theorem
H is disjunctive implies the_left_argument_of H = the_argument_of
the_left_argument_of the_argument_of H
proof
assume H is disjunctive;
then H = (the_left_argument_of H) 'or' (the_right_argument_of H) by
ZF_LANG:41;
then the_argument_of H = 'not'(the_left_argument_of H) '&' 'not' (
the_right_argument_of H) by Th3;
then the_left_argument_of the_argument_of H = 'not'(the_left_argument_of H)
by Th4;
hence thesis by Th3;
end;
theorem
H is disjunctive implies the_right_argument_of H = the_argument_of
the_right_argument_of the_argument_of H
proof
assume H is disjunctive;
then H = (the_left_argument_of H) 'or' (the_right_argument_of H) by
ZF_LANG:41;
then the_argument_of H = 'not'(the_left_argument_of H) '&' 'not' (
the_right_argument_of H) by Th3;
then
the_right_argument_of the_argument_of H = 'not'(the_right_argument_of H)
by Th4;
hence thesis by Th3;
end;
theorem
H is conditional implies the_antecedent_of H = the_left_argument_of
the_argument_of H
proof
assume H is conditional;
then H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
then
the_argument_of H = (the_antecedent_of H) '&' 'not'(the_consequent_of H)
by Th3;
hence thesis by Th4;
end;
theorem
H is conditional implies the_consequent_of H = the_argument_of
the_right_argument_of the_argument_of H
proof
assume H is conditional;
then H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
then
the_argument_of H = (the_antecedent_of H) '&' 'not'(the_consequent_of H)
by Th3;
then
the_right_argument_of the_argument_of H = 'not' (the_consequent_of H) by Th4;
hence thesis by Th3;
end;
theorem
H is biconditional implies the_left_side_of H = the_antecedent_of
the_left_argument_of H & the_left_side_of H = the_consequent_of
the_right_argument_of H
proof
assume H is biconditional;
then H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
then
the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H )
& the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) by
Th4;
hence thesis by Th6;
end;
theorem
H is biconditional implies the_right_side_of H = the_consequent_of
the_left_argument_of H & the_right_side_of H = the_antecedent_of
the_right_argument_of H
proof
assume H is biconditional;
then H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
then
the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H )
& the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) by
Th4;
hence thesis by Th6;
end;
theorem
H is existential implies bound_in H = bound_in the_argument_of H &
the_scope_of H = the_argument_of the_scope_of the_argument_of H
proof
assume H is existential;
then H = Ex(bound_in H, the_scope_of H) by ZF_LANG:45;
then
A1: the_argument_of H = All(bound_in H, 'not' the_scope_of H) by Th3;
hence bound_in H = bound_in the_argument_of H by Th8;
'not' the_scope_of H = the_scope_of the_argument_of H by A1,Th8;
hence thesis by Th3;
end;
theorem
the_argument_of F 'or' G = 'not' F '&' 'not' G & the_antecedent_of F
'or' G = 'not' F & the_consequent_of F 'or' G = G
proof
thus the_argument_of F 'or' G = 'not' F '&' 'not' G by Th3;
F 'or' G = 'not' F => G;
hence thesis by Th6;
end;
theorem
the_argument_of F => G = F '&' 'not' G by Th3;
theorem
the_left_argument_of F <=> G = F => G & the_right_argument_of F <=> G
= G => F by Th4;
theorem
the_argument_of Ex(x,H) = All(x,'not' H) by Th3;
theorem
H is disjunctive implies H is conditional & H is negative &
the_argument_of H is conjunctive & the_left_argument_of the_argument_of H is
negative & the_right_argument_of the_argument_of H is negative
proof
assume H is disjunctive;
then
A1: H = (the_left_argument_of H) 'or' (the_right_argument_of H) by ZF_LANG:41;
then H = 'not'(the_left_argument_of H) => (the_right_argument_of H);
hence H is conditional & H is negative;
A2: the_argument_of H = 'not'(the_left_argument_of H) '&' 'not' (
the_right_argument_of H) by A1,Th3;
hence the_argument_of H is conjunctive;
the_left_argument_of the_argument_of H = 'not'(the_left_argument_of H) &
the_right_argument_of the_argument_of H = 'not'(the_right_argument_of H) by A2
,Th4;
hence thesis;
end;
theorem
H is conditional implies H is negative & the_argument_of H is
conjunctive & the_right_argument_of the_argument_of H is negative
proof
assume H is conditional;
then
A1: H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
hence H is negative;
A2: the_argument_of H = (the_antecedent_of H) '&' 'not'(the_consequent_of H)
by A1,Th3;
hence the_argument_of H is conjunctive;
the_right_argument_of the_argument_of H = 'not' (the_consequent_of H) by A2
,Th4;
hence thesis;
end;
theorem
H is biconditional implies H is conjunctive & the_left_argument_of H
is conditional & the_right_argument_of H is conditional
by Th4;
theorem
H is existential implies H is negative & the_argument_of H is
universal & the_scope_of the_argument_of H is negative
proof
assume H is existential;
then
A1: H = Ex(bound_in H, the_scope_of H) by ZF_LANG:45;
hence H is negative;
A2: the_argument_of H = All(bound_in H, 'not' the_scope_of H) by A1,Th3;
hence the_argument_of H is universal;
'not' the_scope_of H = the_scope_of the_argument_of H by A2,Th8;
hence thesis;
end;
theorem
not (H is being_equality & (H is being_membership or H is negative or
H is conjunctive or H is universal)) & not (H is being_membership & (H is
negative or H is conjunctive or H is universal)) & not (H is negative & (H is
conjunctive or H is universal)) & not (H is conjunctive & H is universal)
proof
H.1 = 0 or H.1 = 1 or H.1 = 2 or H.1 = 3 or H.1 = 4 by ZF_LANG:23;
hence thesis by ZF_LANG:18,19,20,21,22;
end;
theorem Th39:
F is_subformula_of G implies len F <= len G
by ZF_LANG:def 41,ZF_LANG:62;
theorem Th40:
F is_proper_subformula_of G & G is_subformula_of H or F
is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G
is_immediate_constituent_of H or F is_immediate_constituent_of G & G
is_subformula_of H or F is_proper_subformula_of G & G
is_immediate_constituent_of H or F is_immediate_constituent_of G & G
is_proper_subformula_of H implies F is_proper_subformula_of H
proof
A1: F is_immediate_constituent_of G implies F is_proper_subformula_of G by
ZF_LANG:61;
A2: now
assume
A3: F is_proper_subformula_of G;
then
A4: len F < len G by ZF_LANG:62;
assume
A5: G is_subformula_of H;
F is_subformula_of G by A3;
then
A6: F is_subformula_of H by A5,ZF_LANG:65;
len G <= len H by A5,Th39;
hence F is_proper_subformula_of H by A4,A6;
end;
G is_immediate_constituent_of H implies G is_proper_subformula_of H by
ZF_LANG:61;
hence thesis by A2,A1;
end;
theorem
not H is_immediate_constituent_of H
proof
assume H is_immediate_constituent_of H;
then H is_proper_subformula_of H by ZF_LANG:61;
hence contradiction;
end;
theorem
not (G is_proper_subformula_of H & H is_subformula_of G)
proof
assume G is_proper_subformula_of H & H is_subformula_of G;
then G is_proper_subformula_of G by Th40;
hence contradiction;
end;
theorem
not (G is_proper_subformula_of H & H is_proper_subformula_of G)
proof
assume G is_proper_subformula_of H & H is_proper_subformula_of G;
then G is_proper_subformula_of G by ZF_LANG:64;
hence contradiction;
end;
theorem
not (G is_subformula_of H & H is_immediate_constituent_of G)
proof
assume G is_subformula_of H & H is_immediate_constituent_of G;
then G is_proper_subformula_of G by Th40;
hence contradiction;
end;
theorem
not (G is_proper_subformula_of H & H is_immediate_constituent_of G)
proof
assume G is_proper_subformula_of H & H is_immediate_constituent_of G;
then G is_proper_subformula_of G by Th40;
hence contradiction;
end;
theorem
'not' F is_subformula_of H implies F is_proper_subformula_of H
proof
F is_immediate_constituent_of 'not' F;
hence thesis by Th40;
end;
theorem
F '&' G is_subformula_of H implies F is_proper_subformula_of H & G
is_proper_subformula_of H
proof
F is_immediate_constituent_of F '&' G & G is_immediate_constituent_of F
'&' G;
hence thesis by Th40;
end;
theorem
All(x,H) is_subformula_of F implies H is_proper_subformula_of F
proof
H is_immediate_constituent_of All(x,H);
hence thesis by Th40;
end;
theorem
F '&' 'not' G is_proper_subformula_of F => G & F
is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G
is_proper_subformula_of F => G
proof
F '&' 'not' G is_immediate_constituent_of F => G;
hence
A1: F '&' 'not' G is_proper_subformula_of F => G by ZF_LANG:61;
F is_immediate_constituent_of F '&' 'not' G & 'not' G
is_immediate_constituent_of F '&' 'not' G;
hence
A2: F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of
F => G by A1,Th40;
G is_immediate_constituent_of 'not' G;
hence thesis by A2,Th40;
end;
theorem
'not' F '&' 'not' G is_proper_subformula_of F 'or' G & 'not' F
is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F
is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G
proof
'not' F '&' 'not' G is_immediate_constituent_of F 'or' G;
hence
A1: 'not' F '&' 'not' G is_proper_subformula_of F 'or' G by ZF_LANG:61;
'not' F is_immediate_constituent_of 'not' F '&' 'not' G & 'not' G
is_immediate_constituent_of 'not' F '&' 'not' G;
hence
A2: 'not' F is_proper_subformula_of F 'or' G & 'not' G
is_proper_subformula_of F 'or' G by A1,Th40;
F is_immediate_constituent_of 'not' F & G is_immediate_constituent_of
'not' G;
hence thesis by A2,Th40;
end;
theorem
All(x,'not' H) is_proper_subformula_of Ex(x,H) & 'not' H
is_proper_subformula_of Ex(x,H)
proof
All(x,'not' H) is_immediate_constituent_of Ex(x,H);
hence
A1: All(x,'not' H) is_proper_subformula_of Ex(x,H) by ZF_LANG:61;
'not' H is_immediate_constituent_of All(x,'not' H);
hence thesis by A1,Th40;
end;
theorem
G is_subformula_of H iff G in Subformulae H by ZF_LANG:78,def 42;
theorem
G in Subformulae H implies Subformulae G c= Subformulae H by ZF_LANG:78,79;
theorem
H in Subformulae H
proof
H is_subformula_of H by ZF_LANG:59;
hence thesis by ZF_LANG:def 42;
end;
theorem Th55:
Subformulae (F => G) = Subformulae F \/ Subformulae G \/ { 'not'
G, F '&' 'not' G, F => G }
proof
thus Subformulae (F => G) = Subformulae (F '&' 'not' G) \/ { F => G } by
ZF_LANG:82
.= Subformulae F \/ Subformulae 'not' G \/ {F '&' 'not' G} \/ {F => G}
by ZF_LANG:83
.= Subformulae F \/ (Subformulae G \/ {'not' G}) \/ {F '&' 'not' G} \/ {
F => G } by ZF_LANG:82
.= Subformulae F \/ Subformulae G \/ {'not' G} \/ {F '&' 'not' G} \/ { F
=> G } by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G} \/ ({F '&' 'not' G} \/ {
F => G }) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ ({'not' G} \/ ({F '&' 'not' G} \/ {
F => G })) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ ({'not' G} \/ { F '&' 'not' G,F =>
G }) by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ { 'not' G,F '&' 'not' G,F => G } by
ENUMSET1:2;
end;
theorem
Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G,
'not' F, 'not' F '&' 'not' G, F 'or' G}
proof
thus Subformulae (F 'or' G) = Subformulae ('not' F '&' 'not' G) \/ { F 'or'
G } by ZF_LANG:82
.= Subformulae 'not' F \/ Subformulae 'not' G \/ {'not' F '&' 'not' G}
\/ {F 'or' G} by ZF_LANG:83
.= Subformulae 'not' F \/ (Subformulae G \/ {'not' G}) \/ {'not' F '&'
'not' G} \/ {F 'or' G} by ZF_LANG:82
.= Subformulae F \/ {'not' F} \/ (Subformulae G \/ {'not' G}) \/ {'not'
F '&' 'not' G} \/ {F 'or' G} by ZF_LANG:82
.= Subformulae F \/ ((Subformulae G \/ {'not' G}) \/ {'not' F}) \/ {
'not' F '&' 'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ (Subformulae G \/ ({'not' G} \/ {'not' F})) \/ {
'not' F '&' 'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ (Subformulae G \/ {'not' G,'not' F}) \/ {'not' F '&'
'not' G} \/ {F 'or' G} by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ {'not' F '&'
'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ ({'not' F '&'
'not' G} \/ {F 'or' G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ {'not' F '&'
'not' G, F 'or' G} by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ ({'not' G,'not' F} \/ {'not' F '&'
'not' G, F 'or' G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&'
'not' G, F 'or' G} by ENUMSET1:5;
end;
theorem
Subformulae (F <=> G) = Subformulae F \/ Subformulae G \/ { 'not' G, F
'&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G }
proof
thus Subformulae (F <=> G) = Subformulae(F => G) \/ Subformulae(G => F) \/ {
F <=> G} by ZF_LANG:83
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
\/ Subformulae(G => F) \/ {F <=> G} by Th55
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
\/ (Subformulae F \/ Subformulae G \/ { 'not' F, G '&' 'not' F, G => F }) \/ {F
<=> G} by Th55
.= Subformulae F \/ Subformulae G \/ ((Subformulae F \/ Subformulae G \/
{ 'not' G, F '&' 'not' G, F => G }) \/ { 'not' F, G '&' 'not' F, G => F }) \/ {
F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ (Subformulae F \/ Subformulae G \/
({ 'not' G, F '&' 'not' G, F => G } \/ { 'not' F, G '&' 'not' F, G => F })) \/
{F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ (Subformulae F \/ Subformulae G) \/
({ 'not' G, F '&' 'not' G, F => G } \/ { 'not' F, G '&' 'not' F, G => F }) \/ {
F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F } \/ {F <=> G} by ENUMSET1:13
.= Subformulae F \/ Subformulae G \/ ({ 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F } \/ {F <=> G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F, F <=> G } by ENUMSET1:21;
end;
theorem Th58:
Free (x '=' y) = {x,y}
proof
A1: Var2 (x '=' y) = y by Th1;
x '=' y is being_equality & Var1 (x '=' y) = x by Th1;
hence thesis by A1,ZF_MODEL:1;
end;
theorem Th59:
Free (x 'in' y) = {x,y}
proof
A1: Var2 (x 'in' y) = y by Th2;
x 'in' y is being_membership & Var1 (x 'in' y) = x by Th2;
hence thesis by A1,ZF_MODEL:1;
end;
theorem Th60:
Free ('not' p) = Free p
proof
'not' p is negative & the_argument_of 'not' p = p by Th3;
hence thesis by ZF_MODEL:1;
end;
theorem Th61:
Free (p '&' q) = Free p \/ Free q
proof
A1: the_right_argument_of (p '&' q) = q by Th4;
p '&' q is conjunctive & the_left_argument_of (p '&' q) = p by Th4;
hence thesis by A1,ZF_MODEL:1;
end;
theorem Th62:
Free All(x,p) = Free p \ {x}
proof
A1: the_scope_of All(x,p) = p by Th8;
All(x,p) is universal & bound_in All(x,p) = x by Th8;
hence thesis by A1,ZF_MODEL:1;
end;
theorem
Free (p 'or' q) = Free p \/ Free q
proof
thus Free (p 'or' q) = Free ('not' p '&' 'not' q) by Th60
.= Free 'not' p \/ Free 'not' q by Th61
.= Free p \/ Free 'not' q by Th60
.= Free p \/ Free q by Th60;
end;
theorem Th64:
Free (p => q) = Free p \/ Free q
proof
thus Free (p => q) = Free (p '&' 'not' q) by Th60
.= Free p \/ Free 'not' q by Th61
.= Free p \/ Free q by Th60;
end;
theorem
Free (p <=> q) = Free p \/ Free q
proof
thus Free (p <=> q) = Free (p => q) \/ Free (q => p) by Th61
.= Free p \/ Free q \/ Free (q => p) by Th64
.= Free p \/ Free q \/ (Free q \/ Free p) by Th64
.= Free p \/ Free q \/ Free q \/ Free p by XBOOLE_1:4
.= Free p \/ (Free q \/ Free q) \/ Free p by XBOOLE_1:4
.= Free p \/ Free p \/ Free q by XBOOLE_1:4
.= Free p \/ Free q;
end;
theorem Th66:
Free Ex(x,p) = Free p \ {x}
proof
thus Free Ex(x,p) = Free All(x,'not' p) by Th60
.= Free 'not' p \ {x} by Th62
.= Free p \ {x} by Th60;
end;
theorem Th67:
Free All(x,y,p) = Free p \ {x,y}
proof
thus Free All(x,y,p) = Free All(y,p) \ {x} by Th62
.= (Free p \ {y}) \ {x} by Th62
.= Free p \ ({x} \/ {y}) by XBOOLE_1:41
.= Free p \ {x,y} by ENUMSET1:1;
end;
theorem
Free All(x,y,z,p) = Free p \ {x,y,z}
proof
thus Free All(x,y,z,p) = Free All(y,z,p) \ {x} by Th62
.= (Free p \ {y,z}) \ {x} by Th67
.= Free p \ ({x} \/ {y,z}) by XBOOLE_1:41
.= Free p \ {x,y,z} by ENUMSET1:2;
end;
theorem Th69:
Free Ex(x,y,p) = Free p \ {x,y}
proof
thus Free Ex(x,y,p) = Free Ex(y,p) \ {x} by Th66
.= (Free p \ {y}) \ {x} by Th66
.= Free p \ ({x} \/ {y}) by XBOOLE_1:41
.= Free p \ {x,y} by ENUMSET1:1;
end;
theorem
Free Ex(x,y,z,p) = Free p \ {x,y,z}
proof
thus Free Ex(x,y,z,p) = Free Ex(y,z,p) \ {x} by Th66
.= (Free p \ {y,z}) \ {x} by Th69
.= Free p \ ({x} \/ {y,z}) by XBOOLE_1:41
.= Free p \ {x,y,z} by ENUMSET1:2;
end;
scheme
ZFInduction { P[ZF-formula] } : for H holds P[H]
provided
A1: for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2] and
A2: for H st P[H] holds P['not' H] and
A3: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2] and
A4: for H,x st P[H] holds P[All(x,H)]
proof
A5: for H st H is conjunctive & P[the_left_argument_of H] & P[
the_right_argument_of H] holds P[H]
proof
let H;
assume H is conjunctive;
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by
ZF_LANG:40;
hence thesis by A3;
end;
A6: for H st H is atomic holds P[H]
proof
let H such that
A7: H is being_equality or H is being_membership;
A8: H is being_membership implies thesis
by A1;
H is being_equality implies thesis
by A1;
hence thesis by A7,A8;
end;
A9: for H st H is universal & P[the_scope_of H] holds P[H]
proof
let H;
assume H is universal;
then H = All(bound_in H, the_scope_of H) by ZF_LANG:44;
hence thesis by A4;
end;
A10: for H st H is negative & P[the_argument_of H] holds P[H]
proof
let H;
assume H is negative;
then H = 'not' the_argument_of H by ZF_LANG:def 30;
hence thesis by A2;
end;
thus for H holds P[H] from ZF_LANG:sch 1(A6,A10,A5,A9);
end;
reserve M for non empty set,
m,m9 for Element of M,
v,v9 for Function of VAR,M;
definition
let D,D1,D2 be non empty set, f be Function of D,D1;
assume
A1: D1 c= D2;
func D2!f -> Function of D,D2 equals
f;
correctness
proof
rng f c= D1 by RELAT_1:def 19;
then
A2: rng f c= D2 by A1;
dom f = D by FUNCT_2:def 1;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
end;
notation
let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
of E;
synonym f / (x,e) for f+*(x,e);
end;
definition
let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
of E;
redefine func f/(x,e) -> Function of VAR, E; :: redefines / (ZF_LANG1, synonym) → +* (FUNCT_7, definition)
coherence
proof
f+*(x,e) is Function of VAR, E;
hence thesis;
end;
end;
theorem Th71:
M,v |= All(x,H) iff for m holds M,v/(x,m) |= H
proof
thus M,v |= All(x,H) implies for m holds M,v/(x,m) |= H
proof
assume
A1: M,v |= All(x,H);
let m;
for y st (v/(x,m)).y <> v.y holds x = y by FUNCT_7:32;
hence thesis by A1,ZF_MODEL:16;
end;
assume
A2: for m holds M,v/(x,m) |= H;
now
let v9;
assume for y st v9.y <> v.y holds x = y;
then v9 = v/(x,v9.x) by FUNCT_7:129;
hence M,v9 |= H by A2;
end;
hence thesis by ZF_MODEL:16;
end;
theorem Th72:
M,v |= All(x,H) iff M,v/(x,m) |= All(x,H)
proof
A1: for v,m st M,v |= All(x,H) holds M,v/(x,m) |= All(x,H)
proof
let v,m such that
A2: M,v |= All(x,H);
now
let m9;
(v/(x,m))/(x,m9) = v/(x,m9) by FUNCT_7:34;
hence M,(v/(x,m))/(x,m9) |= H by A2,Th71;
end;
hence thesis by Th71;
end;
(v/(x,m))/(x,v.x) = v/(x,v.x) by FUNCT_7:34
.= v by FUNCT_7:35;
hence thesis by A1;
end;
theorem Th73:
M,v |= Ex(x,H) iff ex m st M,v/(x,m) |= H
proof
thus M,v |= Ex(x,H) implies ex m st M,v/(x,m) |= H
proof
assume M,v |= Ex(x,H);
then consider v9 such that
A1: ( for y st v9.y <> v.y holds x = y)& M,v9 |= H by ZF_MODEL:20;
take v9.x;
thus thesis by A1,FUNCT_7:129;
end;
given m such that
A2: M,v/(x,m) |= H;
now
take v9 = v/(x,m);
thus for y st v9.y <> v.y holds x = y by FUNCT_7:32;
thus M,v9 |= H by A2;
end;
hence thesis by ZF_MODEL:20;
end;
theorem
M,v |= Ex(x,H) iff M,v/(x,m) |= Ex(x,H)
proof
A1: for v,m st M,v |= Ex(x,H) holds M,v/(x,m) |= Ex(x,H)
proof
let v,m;
assume M,v |= Ex(x,H);
then consider m9 such that
A2: M,v/(x,m9) |= H by Th73;
(v/(x,m))/(x,m9) = v/(x,m9) by FUNCT_7:34;
hence thesis by A2,Th73;
end;
(v/(x,m))/(x,v.x) = v/(x,v.x) by FUNCT_7:34
.= v by FUNCT_7:35;
hence thesis by A1;
end;
theorem
for v,v9 st for x st x in Free H holds v9.x = v.x holds M,v |= H
implies M,v9 |= H
proof
defpred Etha[ZF-formula] means for v,v9 st for x st x in Free $1 holds v9.x
= v.x holds M,v |= $1 implies M,v9 |= $1;
A1: for H1,H2 st Etha[H1] & Etha[H2] holds Etha[H1 '&' H2]
proof
let H1,H2 such that
A2: Etha[H1] and
A3: Etha[H2];
let v,v9;
assume
A4: for x st x in Free H1 '&' H2 holds v9.x = v.x;
A5: Free (H1 '&' H2) = Free H1 \/ Free H2 by Th61;
A6: now
let x;
assume x in Free H2;
then x in Free (H1 '&' H2) by A5,XBOOLE_0:def 3;
hence v9.x = v.x by A4;
end;
assume
A7: M,v |= H1 '&' H2;
then M,v |= H2 by ZF_MODEL:15;
then
A8: M,v9 |= H2 by A3,A6;
A9: now
let x;
assume x in Free H1;
then x in Free (H1 '&' H2) by A5,XBOOLE_0:def 3;
hence v9.x = v.x by A4;
end;
M,v |= H1 by A7,ZF_MODEL:15;
then M,v9 |= H1 by A2,A9;
hence thesis by A8,ZF_MODEL:15;
end;
A10: for x1,x2 holds Etha[x1 '=' x2] & Etha[x1 'in' x2]
proof
let x1,x2;
A11: Free (x1 '=' x2) = {x1,x2} by Th58;
thus Etha[x1 '=' x2]
proof
let v,v9;
assume
A12: for x st x in Free (x1 '=' x2) holds v9.x = v.x;
x2 in Free (x1 '=' x2) by A11,TARSKI:def 2;
then
A13: v9.x2 = v.x2 by A12;
assume M,v |= x1 '=' x2;
then
A14: v.x1 = v.x2 by ZF_MODEL:12;
x1 in Free (x1 '=' x2) by A11,TARSKI:def 2;
then v9.x1 = v.x1 by A12;
hence thesis by A14,A13,ZF_MODEL:12;
end;
let v,v9;
assume
A15: for x st x in Free (x1 'in' x2) holds v9.x = v.x;
A16: Free (x1 'in' x2) = {x1,x2} by Th59;
then x2 in Free (x1 'in' x2) by TARSKI:def 2;
then
A17: v9.x2 = v.x2 by A15;
assume M,v |= x1 'in' x2;
then
A18: v.x1 in v.x2 by ZF_MODEL:13;
x1 in Free (x1 'in' x2) by A16,TARSKI:def 2;
then v9.x1 = v.x1 by A15;
hence thesis by A18,A17,ZF_MODEL:13;
end;
A19: for H,x st Etha[H] holds Etha[All(x,H)]
proof
let H,x1 such that
A20: Etha[H];
let v,v9;
assume that
A21: for x st x in Free All(x1,H) holds v9.x = v.x and
A22: M,v |= All(x1,H);
now
let m;
A23: Free All(x1,H) = Free H \ {x1} by Th62;
A24: now
let x;
assume x in Free H;
then x in Free All(x1,H) & not x in {x1} or x in {x1} by A23,
XBOOLE_0:def 5;
then v9.x = v.x & x <> x1 or x = x1 by A21,TARSKI:def 1;
then
v9/(x1,m).x = v.x & v.x = v/(x1,m).x or v/(x1,m).x = m & v9/(x1,m
).x = m by FUNCT_7:32,128;
hence v9/(x1,m).x = v/(x1,m).x;
end;
M,v/(x1,m) |= H by A22,Th71;
hence M,v9/(x1,m) |= H by A20,A24;
end;
hence thesis by Th71;
end;
A25: for H st Etha[H] holds Etha['not' H]
proof
let H such that
A26: Etha[H];
let v,v9;
assume
A27: for x st x in Free 'not' H holds v9.x = v.x;
A28: now
let x;
assume x in Free H;
then x in Free 'not' H by Th60;
hence v.x = v9.x by A27;
end;
assume M,v |= 'not' H;
then not M,v |= H by ZF_MODEL:14;
then not M,v9 |= H by A26,A28;
hence thesis by ZF_MODEL:14;
end;
for H holds Etha[H] from ZFInduction(A10,A25,A1,A19);
hence thesis;
end;
registration
let H;
cluster Free H -> finite;
coherence
proof
defpred P[ZF-formula] means Free $1 is finite;
A1: P[p] & P[q] implies P[p '&' q]
proof
Free p '&' q = Free p \/ Free q by Th61;
hence thesis;
end;
A2: P[p] implies P[All(x,p)]
proof
Free All(x,p) = Free p \ {x} by Th62;
hence thesis;
end;
A3: P[x '=' y] & P[x 'in' y]
proof
Free (x '=' y) = {x,y} by Th58;
hence thesis by Th59;
end;
A4: P[p] implies P['not' p] by Th60;
P[p] from ZFInduction(A3,A4,A1,A2);
hence thesis;
end;
end;
reserve i,j for Element of NAT;
theorem
x.i = x.j implies i = j;
theorem
ex i st x = x.i
proof
x in VAR;
then consider j such that
A1: x = j and
A2: 5 <= j;
consider i be Nat such that
A3: j = 5+i by A2,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
take i;
thus thesis by A1,A3;
end;
theorem Th78:
M,v |= x '=' x
proof
v.x = v.x;
hence thesis by ZF_MODEL:12;
end;
theorem Th79:
M |= x '=' x
by Th78;
theorem Th80:
not M,v |= x 'in' x
proof
not v.x in v.x;
hence thesis by ZF_MODEL:13;
end;
theorem Th81:
not M |= x 'in' x & M |= 'not' x 'in' x
proof
set v = the Function of VAR,M;
not M,v |= x 'in' x by Th80;
hence not M |= x 'in' x;
let v;
not M,v |= x 'in' x by Th80;
hence thesis by ZF_MODEL:14;
end;
theorem
M |= x '=' y iff x = y or ex a st {a} = M
proof
thus M |= x '=' y implies x = y or ex a st {a} = M
proof
set v = the Function of VAR,M;
set m = the Element of M;
assume that
A1: for v holds M,v |= x '=' y and
A2: x <> y;
reconsider a = m as set;
take a;
thus {a} c= M by ZFMISC_1:31;
let b be object;
assume that
A3: b in M and
A4: not b in {a};
reconsider b as Element of M by A3;
M,(v/(x,m))/(y,b) |= x '=' y by A1;
then
A5: (v/(x,m))/(y,b).x = (v/(x,m))/(y,b).y by ZF_MODEL:12;
A6: v/(x,m).x = m & (v/(x,m))/(y,b).y = b by FUNCT_7:128;
(v/(x,m))/(y,b).x = v/(x,m).x by A2,FUNCT_7:32;
hence contradiction by A4,A5,A6,TARSKI:def 1;
end;
now
given a such that
A7: {a} = M;
let v;
v.x = a & v.y = a by A7,TARSKI:def 1;
hence M,v |= x '=' y by ZF_MODEL:12;
end;
hence thesis by Th79;
end;
theorem
M |= 'not' x 'in' y iff x = y or for X st X in M holds X misses M
proof
thus M |= 'not' x 'in' y implies x = y or for X st X in M holds X misses M
proof
set v = the Function of VAR,M;
assume that
A1: for v holds M,v |= 'not' x 'in' y and
A2: x <> y;
let X;
set a = the Element of X /\ M;
assume X in M;
then reconsider m = X as Element of M;
assume
A3: X /\ M <> {};
then reconsider a as Element of M by XBOOLE_0:def 4;
M,(v/(x,a))/(y,m) |= 'not' x 'in' y by A1;
then not M,(v/(x,a))/(y,m) |= x 'in' y by ZF_MODEL:14;
then
A4: not (v/(x,a))/(y,m).x in (v/(x,a))/(y,m).y by ZF_MODEL:13;
A5: v/(x,a).x = a & (v/(x,a))/(y,m).y = m by FUNCT_7:128;
(v/(x,a))/(y,m).x = v/(x,a).x by A2,FUNCT_7:32;
hence contradiction by A3,A4,A5,XBOOLE_0:def 4;
end;
now
assume
A6: for X st X in M holds X misses M;
let v;
v.y misses M by A6;
then not v.x in v.y by XBOOLE_0:3;
then not M,v |= x 'in' y by ZF_MODEL:13;
hence M,v |= 'not' x 'in' y by ZF_MODEL:14;
end;
hence thesis by Th81;
end;
theorem
H is being_equality implies (M,v |= H iff v.Var1 H = v.Var2 H)
proof
assume H is being_equality;
then H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
hence thesis by ZF_MODEL:12;
end;
theorem
H is being_membership implies (M,v |= H iff v.Var1 H in v.Var2 H)
proof
assume H is being_membership;
then H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
hence thesis by ZF_MODEL:13;
end;
theorem
H is negative implies (M,v |= H iff not M,v |= the_argument_of H)
proof
assume H is negative;
then H = 'not' the_argument_of H by ZF_LANG:def 30;
hence thesis by ZF_MODEL:14;
end;
theorem
H is conjunctive implies (M,v |= H iff M,v |= the_left_argument_of H &
M,v |= the_right_argument_of H)
proof
assume H is conjunctive;
then H = (the_left_argument_of H) '&' (the_right_argument_of H)
by ZF_LANG:40;
hence thesis by ZF_MODEL:15;
end;
theorem
H is universal implies (M,v |= H iff for m holds M,v/(bound_in H,m) |=
the_scope_of H)
proof
assume H is universal;
then H = All(bound_in H, the_scope_of H) by ZF_LANG:44;
hence thesis by Th71;
end;
theorem
H is disjunctive implies (M,v |= H iff M,v |= the_left_argument_of H
or M,v |= the_right_argument_of H)
proof
assume H is disjunctive;
then H = (the_left_argument_of H) 'or' (the_right_argument_of H) by
ZF_LANG:41;
hence thesis by ZF_MODEL:17;
end;
theorem
H is conditional implies (M,v |= H iff (M,v |= the_antecedent_of H
implies M,v |= the_consequent_of H))
proof
assume H is conditional;
then H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
hence thesis by ZF_MODEL:18;
end;
theorem
H is biconditional implies (M,v |= H iff (M,v |= the_left_side_of H
iff M,v |= the_right_side_of H))
proof
assume H is biconditional;
then H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
hence thesis by ZF_MODEL:19;
end;
theorem
H is existential implies (M,v |= H iff ex m st M,v/(bound_in H,m) |=
the_scope_of H)
proof
assume H is existential;
then H = Ex(bound_in H, the_scope_of H) by ZF_LANG:45;
hence thesis by Th73;
end;
theorem
M |= Ex(x,H) iff for v ex m st M,v/(x,m) |= H
proof
thus M |= Ex(x,H) implies for v ex m st M,v/(x,m) |= H
by Th73;
assume
A1: for v ex m st M,v/(x,m) |= H;
let v;
ex m st M,v/(x,m) |= H by A1;
hence thesis by Th73;
end;
theorem Th94:
M |= H implies M |= Ex(x,H)
proof
assume
A1: M |= H;
let v;
M,v/(x,v.x) |= H by A1;
hence thesis by Th73;
end;
theorem Th95:
M |= H iff M |= All(x,y,H)
proof
M |= H iff M |= All(y,H) by ZF_MODEL:23;
hence thesis by ZF_MODEL:23;
end;
theorem Th96:
M |= H implies M |= Ex(x,y,H)
proof
M |= H implies M |= Ex(y,H) by Th94;
hence thesis by Th94;
end;
theorem
M |= H iff M |= All(x,y,z,H)
proof
M |= H iff M |= All(y,z,H) by Th95;
hence thesis by ZF_MODEL:23;
end;
theorem
M |= H implies M |= Ex(x,y,z,H)
proof
M |= H implies M |= Ex(y,z,H) by Th96;
hence thesis by Th94;
end;
::
:: Axioms of Logic
::
theorem
M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q)
proof
A1: now
let v;
M,v |= p <=> q implies M,v |= p => q by ZF_MODEL:15;
hence M,v |= (p <=> q) => (p => q) by ZF_MODEL:18;
end;
hence M,v |= (p <=> q) => (p => q);
let v;
thus thesis by A1;
end;
theorem
M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p)
proof
A1: now
let v;
M,v |= p <=> q implies M,v |= q => p by ZF_MODEL:15;
hence M,v |= (p <=> q) => (q => p) by ZF_MODEL:18;
end;
hence M,v |= (p <=> q) => (q => p);
let v;
thus thesis by A1;
end;
theorem Th101:
M |= (p => q) => ((q => r) => (p => r))
proof
let v;
now
assume
A1: M,v |= p => q;
now
assume
A2: M,v |= q => r;
now
assume M,v |= p;
then M,v |= q by A1,ZF_MODEL:18;
hence M,v |= r by A2,ZF_MODEL:18;
end;
hence M,v |= p => r by ZF_MODEL:18;
end;
hence M,v |= (q => r) => (p => r) by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:18;
end;
theorem Th102:
M,v |= p => q & M,v |= q => r implies M,v |= p => r
proof
assume that
A1: M,v |= p => q and
A2: M,v |= q => r;
M |= (p => q) => ((q => r) => (p => r)) by Th101;
then M,v |= (p => q) => ((q => r) => (p => r));
then M,v |= (q => r) => (p => r) by A1,ZF_MODEL:18;
hence thesis by A2,ZF_MODEL:18;
end;
theorem
M |= p => q & M |= q => r implies M |= p => r
proof
assume
A1: M |= p => q & M |= q => r;
let v;
M,v |= p => q & M,v |= q => r by A1;
hence thesis by Th102;
end;
theorem
M,v |= (p => q) '&' (q => r) => (p => r) & M |= (p => q) '&' (q => r)
=> (p => r)
proof
now
let v;
now
assume M,v |= (p => q) '&' (q => r);
then M,v |= (p => q) & M,v |= (q => r) by ZF_MODEL:15;
hence M,v |= p => r by Th102;
end;
hence M,v |= (p => q) '&' (q => r) => (p => r) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p => (q => p) & M |= p => (q => p)
proof
now
let v;
M,v |= p implies M,v |= q => p by ZF_MODEL:18;
hence M,v |= p => (q => p) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)
) => ((p => q) => (p => r))
proof
now
let v;
now
assume
A1: M,v |= p => (q => r);
now
assume M,v |= p => q;
then
A2: M,v |= p implies M,v |= q => r & M,v |= q by A1,ZF_MODEL:18;
M,v |= q & M,v |= q => r implies M,v |= r by ZF_MODEL:18;
hence M,v |= p => r by A2,ZF_MODEL:18;
end;
hence M,v |= (p => q) => (p => r) by ZF_MODEL:18;
end;
hence M,v |= (p => (q => r)) => ((p => q) => (p => r)) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p '&' q => p & M |= p '&' q => p
proof
now
let v;
M,v |= p '&' q implies M,v |= p by ZF_MODEL:15;
hence M,v |= p '&' q => p by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p '&' q => q & M |= p '&' q => q
proof
now
let v;
M,v |= p '&' q implies M,v |= q by ZF_MODEL:15;
hence M,v |= p '&' q => q by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p
proof
now
let v;
A1: M,v |= p & M,v |= q implies M,v |= q '&' p by ZF_MODEL:15;
M,v |= p '&' q implies M,v |= p & M,v |= q by ZF_MODEL:15;
hence M,v |= p '&' q => q '&' p by A1,ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p => p '&' p & M |= p => p '&' p
proof
now
let v;
M,v |= p implies M,v |= p '&' p by ZF_MODEL:15;
hence M,v |= p => p '&' p by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= (p => q) => ((p => r) => (p => q '&' r)) & M |= (p => q) => ((p
=> r) => (p => q '&' r))
proof
now
let v;
now
assume
A1: M,v |= p => q;
now
assume M,v |= p => r;
then M,v |= p implies M,v |= r & M,v |= q by A1,ZF_MODEL:18;
then M,v |= p implies M,v |= q '&' r by ZF_MODEL:15;
hence M,v |= p => q '&' r by ZF_MODEL:18;
end;
hence M,v |= (p => r) => (p => q '&' r) by ZF_MODEL:18;
end;
hence M,v |= (p => q) => ((p => r) => (p => q '&' r)) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem Th112:
M,v |= p => p 'or' q & M |= p => p 'or' q
proof
now
let v;
M,v |= p implies M,v |= p 'or' q by ZF_MODEL:17;
hence M,v |= p => p 'or' q by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= q => p 'or' q & M |= q => p 'or' q
proof
now
let v;
M,v |= q implies M,v |= p 'or' q by ZF_MODEL:17;
hence M,v |= q => p 'or' q by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p
proof
now
let v;
A1: M,v |= p or M,v |= q implies M,v |= q 'or' p by ZF_MODEL:17;
M,v |= p 'or' q implies M,v |= p or M,v |= q by ZF_MODEL:17;
hence M,v |= p 'or' q => q 'or' p by A1,ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= p => p 'or' p & M |= p => p 'or' p by Th112;
theorem
M,v |= (p => r) => ((q => r) => (p 'or' q => r)) & M |= (p => r) => ((
q => r) => (p 'or' q => r))
proof
now
let v;
now
assume
A1: M,v |= p => r;
now
assume M,v |= q => r;
then M,v |= p or M,v |= q implies M,v |= r by A1,ZF_MODEL:18;
then M,v |= p 'or' q implies M,v |= r by ZF_MODEL:17;
hence M,v |= p 'or' q => r by ZF_MODEL:18;
end;
hence M,v |= (q => r) => (p 'or' q => r) by ZF_MODEL:18;
end;
hence M,v |= (p => r) => ((q => r) => (p 'or' q => r)) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= (p => r) '&' (q => r) => (p 'or' q => r) & M |= (p => r) '&' (q
=> r) => (p 'or' q => r)
proof
now
let v;
now
assume M,v |= (p => r) '&' (q => r);
then M,v |= p => r & M,v |= q => r by ZF_MODEL:15;
then M,v |= p or M,v |= q implies M,v |= r by ZF_MODEL:18;
then M,v |= p 'or' q implies M,v |= r by ZF_MODEL:17;
hence M,v |= p 'or' q => r by ZF_MODEL:18;
end;
hence M,v |= (p => r) '&' (q => r) => (p 'or' q => r) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= (p => 'not' q) => (q => 'not' p) & M |= (p => 'not' q) => (q =>
'not' p)
proof
now
let v;
now
assume M,v |= p => 'not' q;
then M,v |= p implies M,v |= 'not' q by ZF_MODEL:18;
then M,v |= q implies M,v |= 'not' p by ZF_MODEL:14;
hence M,v |= q => 'not' p by ZF_MODEL:18;
end;
hence M,v |= (p => 'not' q) => (q => 'not' p) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= 'not' p => (p => q) & M |= 'not' p => (p => q)
proof
now
let v;
now
assume M,v |= 'not' p;
then not M,v |= p by ZF_MODEL:14;
hence M,v |= p => q by ZF_MODEL:18;
end;
hence M,v |= 'not' p => (p => q) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= (p => q) '&' (p => 'not' q) => 'not' p & M |= (p => q) '&' (p
=> 'not' q) => 'not' p
proof
now
let v;
now
assume M,v |= (p => q) '&' (p => 'not' q);
then M,v |= p => q & M,v |= p => 'not' q by ZF_MODEL:15;
then M,v |= p implies M,v |= q & M,v |= 'not' q by ZF_MODEL:18;
hence M,v |= 'not' p by ZF_MODEL:14;
end;
hence M,v |= (p => q) '&' (p => 'not' q) => 'not' p by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M |= p => q & M |= p implies M |= q
proof
assume
A1: M |= p => q & M |= p;
let v;
M,v |= p => q & M,v |= p by A1;
hence thesis by ZF_MODEL:18;
end;
theorem
M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q & M |= 'not'(p '&' q) =>
'not' p 'or' 'not' q
proof
now
let v;
now
assume M,v |= 'not'(p '&' q);
then not M,v |= p '&' q by ZF_MODEL:14;
then not M,v |= p or not M,v |= q by ZF_MODEL:15;
then M,v |= 'not' p or M,v |= 'not' q by ZF_MODEL:14;
hence M,v |= 'not' p 'or' 'not' q by ZF_MODEL:17;
end;
hence M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) & M |= 'not' p 'or'
'not' q => 'not'(p '&' q)
proof
now
let v;
now
assume M,v |= 'not' p 'or' 'not' q;
then M,v |= 'not' p or M,v |= 'not' q by ZF_MODEL:17;
then not M,v |= p or not M,v |= q by ZF_MODEL:14;
then not M,v |= p '&' q by ZF_MODEL:15;
hence M,v |= 'not'(p '&' q) by ZF_MODEL:14;
end;
hence M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q & M |= 'not'(p 'or' q)
=> 'not' p '&' 'not' q
proof
now
let v;
now
assume M,v |= 'not'(p 'or' q);
then
A1: not M,v |= p 'or' q by ZF_MODEL:14;
then not M,v |= q by ZF_MODEL:17;
then
A2: M,v |= 'not' q by ZF_MODEL:14;
not M,v |= p by A1,ZF_MODEL:17;
then M,v |= 'not' p by ZF_MODEL:14;
hence M,v |= 'not' p '&' 'not' q by A2,ZF_MODEL:15;
end;
hence M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) & M |= 'not' p '&' 'not'
q => 'not'(p 'or' q)
proof
now
let v;
now
assume
A1: M,v |= 'not' p '&' 'not' q;
then M,v |= 'not' q by ZF_MODEL:15;
then
A2: not M,v |= q by ZF_MODEL:14;
M,v |= 'not' p by A1,ZF_MODEL:15;
then not M,v |= p by ZF_MODEL:14;
then not M,v |= p 'or' q by A2,ZF_MODEL:17;
hence M,v |= 'not'(p 'or' q) by ZF_MODEL:14;
end;
hence M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) by ZF_MODEL:18;
end;
hence thesis;
end;
theorem
M |= All(x,H) => H
proof
let v;
M,v |= All(x,H) implies M,v/(x,v.x) |= H by Th71;
then M,v |= All(x,H) implies M,v |= H by FUNCT_7:35;
hence thesis by ZF_MODEL:18;
end;
theorem
M |= H => Ex(x,H)
proof
let v;
M,v/(x,v.x) |= H implies M,v |= Ex(x,H) by Th73;
then M,v |= H implies M,v |= Ex(x,H) by FUNCT_7:35;
hence thesis by ZF_MODEL:18;
end;
theorem Th128:
not x in Free H1 implies M |= All(x,H1 => H2) => (H1 => All(x, H2))
proof
assume
A1: not x in Free H1;
let v;
now
assume
A2: M,v |= All(x,H1 => H2);
now
assume
A3: M,v |= H1;
now
let m;
M,v |= All(x,H1) by A1,A3,ZFMODEL1:10;
then
A4: M,v/(x,m) |= H1 by Th71;
M,v/(x,m) |= H1 => H2 by A2,Th71;
hence M,v/(x,m) |= H2 by A4,ZF_MODEL:18;
end;
hence M,v |= All(x,H2) by Th71;
end;
hence M,v |= H1 => All(x,H2) by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:18;
end;
theorem
not x in Free H1 & M |= H1 => H2 implies M |= H1 => All(x,H2)
proof
assume that
A1: not x in Free H1 and
A2: for v holds M,v |= H1 => H2;
let v;
M |= All(x,H1 => H2) => (H1 => All(x,H2)) by A1,Th128;
then
A3: M,v |= All(x,H1 => H2) => (H1 => All(x,H2));
for m holds M,v/(x,m) |= H1 => H2 by A2;
then M,v |= All(x,H1 => H2) by Th71;
hence thesis by A3,ZF_MODEL:18;
end;
theorem Th130:
not x in Free H2 implies M |= All(x,H1 => H2) => (Ex(x,H1) => H2)
proof
assume
A1: not x in Free H2;
let v;
now
assume
A2: M,v |= All(x,H1 => H2);
now
assume M,v |= Ex(x,H1);
then consider m such that
A3: M,v/(x,m) |= H1 by Th73;
M,v/(x,m) |= H1 => H2 by A2,Th71;
then M,v/(x,m) |= H2 by A3,ZF_MODEL:18;
then M,v/(x,m) |= All(x,H2) by A1,ZFMODEL1:10;
then M,v |= All(x,H2) by Th72;
then M,v/(x,v.x) |= H2 by Th71;
hence M,v |= H2 by FUNCT_7:35;
end;
hence M,v |= Ex(x,H1) => H2 by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:18;
end;
theorem
not x in Free H2 & M |= H1 => H2 implies M |= Ex(x,H1) => H2
proof
assume that
A1: not x in Free H2 and
A2: for v holds M,v |= H1 => H2;
let v;
M |= All(x,H1 => H2) => (Ex(x,H1) => H2) by A1,Th130;
then
A3: M,v |= All(x,H1 => H2) => (Ex(x,H1) => H2);
for m holds M,v/(x,m) |= H1 => H2 by A2;
then M,v |= All(x,H1 => H2) by Th71;
hence thesis by A3,ZF_MODEL:18;
end;
theorem
M |= H1 => All(x,H2) implies M |= H1 => H2
proof
assume
A1: for v holds M,v |= H1 => All(x,H2);
let v;
A2: M,v |= H1 => All(x,H2) by A1;
now
assume M,v |= H1;
then M,v |= All(x,H2) by A2,ZF_MODEL:18;
then M,v/(x,v.x) |= H2 by Th71;
hence M,v |= H2 by FUNCT_7:35;
end;
hence thesis by ZF_MODEL:18;
end;
theorem
M |= Ex(x,H1) => H2 implies M |= H1 => H2
proof
assume
A1: for v holds M,v |= Ex(x,H1) => H2;
let v;
A2: M,v |= Ex(x,H1) => H2 by A1;
now
assume M,v |= H1;
then M,v/(x,v.x) |= H1 by FUNCT_7:35;
then M,v |= Ex(x,H1) by Th73;
hence M,v |= H2 by A2,ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:18;
end;
theorem
WFF c= bool [:NAT,NAT:]
proof
let a be object;
assume a in WFF;
then reconsider H = a as ZF-formula by ZF_LANG:4;
H c= [:NAT,NAT:];
hence thesis;
end;
::
:: Variables in ZF-formula
::
definition
let H;
func variables_in H -> set equals
rng H \ { 0,1,2,3,4 };
correctness;
end;
theorem Th135:
x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4
proof
x in VAR;
then
A1: ex i st x = i & 5 <= i;
assume x = 0 or x = 1 or x = 2 or x = 3 or x = 4;
hence contradiction by A1;
end;
theorem Th136:
not x in { 0,1,2,3,4 }
proof
assume x in { 0,1,2,3,4 };
then x in { 0,1 } \/ { 2,3,4 } by ENUMSET1:8;
then x in { 0,1 } or x in { 2,3,4 } by XBOOLE_0:def 3;
then
A1: x = 0 or x = 1 or x = 2 or x = 3 or x = 4 by ENUMSET1:def 1,TARSKI:def 2;
x in VAR;
then ex i st x = i & 5 <= i;
hence contradiction by A1;
end;
theorem Th137:
a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4
proof
assume a in variables_in H;
then not a in {0,1,2,3,4} by XBOOLE_0:def 5;
then not a in {0,1} \/ {2,3,4} by ENUMSET1:8;
then ( not a in {0,1})& not a in {2,3,4} by XBOOLE_0:def 3;
hence thesis by ENUMSET1:def 1,TARSKI:def 2;
end;
theorem Th138:
variables_in x '=' y = {x,y}
proof
A1: rng (x '=' y) = rng (<*0*>^<*x*>) \/ rng <*y*> by FINSEQ_1:31
.= rng <*0*> \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:31
.= {0} \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:39
.= {0} \/ {x} \/ rng <*y*> by FINSEQ_1:39
.= {0} \/ {x} \/ {y} by FINSEQ_1:39
.= {0} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {0} \/ {x,y} by ENUMSET1:1;
thus variables_in (x '=' y) c= {x,y}
proof
let a be object;
assume
A2: a in variables_in x '=' y;
then a <> 0 by Th137;
then not a in {0} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 3;
end;
let a be object;
assume
A3: a in {x,y};
then a = x or a = y by TARSKI:def 2;
then
A4: not a in {0,1,2,3,4} by Th136;
a in {0} \/ {x,y} by A3,XBOOLE_0:def 3;
hence thesis by A1,A4,XBOOLE_0:def 5;
end;
theorem Th139:
variables_in x 'in' y = {x,y}
proof
A1: rng (x 'in' y) = rng (<*1*>^<*x*>) \/ rng <*y*> by FINSEQ_1:31
.= rng <*1*> \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:31
.= {1} \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:39
.= {1} \/ {x} \/ rng <*y*> by FINSEQ_1:39
.= {1} \/ {x} \/ {y} by FINSEQ_1:39
.= {1} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {1} \/ {x,y} by ENUMSET1:1;
thus variables_in (x 'in' y) c= {x,y}
proof
let a be object;
assume
A2: a in variables_in x 'in' y;
then a <> 1 by Th137;
then not a in {1} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 3;
end;
let a be object;
assume
A3: a in {x,y};
then a = x or a = y by TARSKI:def 2;
then
A4: not a in {0,1,2,3,4} by Th136;
a in {1} \/ {x,y} by A3,XBOOLE_0:def 3;
hence thesis by A1,A4,XBOOLE_0:def 5;
end;
theorem Th140:
variables_in 'not' H = variables_in H
proof
A1: rng 'not' H = rng <*2*> \/ rng H by FINSEQ_1:31
.= {2} \/ rng H by FINSEQ_1:39;
thus variables_in 'not' H c= variables_in H
proof
let a be object;
assume
A2: a in variables_in 'not' H;
then a <> 2 by Th137;
then not a in {2} by TARSKI:def 1;
then
A3: a in rng H by A1,A2,XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A2,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 5;
end;
thus thesis by A1,XBOOLE_1:7,33;
end;
theorem Th141:
variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2
proof
A1: variables_in H1 \/ variables_in H2 = (rng H1 \/ rng H2) \ {0,1,2,3,4} by
XBOOLE_1:42;
A2: rng(H1 '&' H2) = rng (<*3*>^H1) \/ rng H2 by FINSEQ_1:31
.= rng <*3*> \/ rng H1 \/ rng H2 by FINSEQ_1:31
.= {3} \/ rng H1 \/ rng H2 by FINSEQ_1:39
.= {3} \/ (rng H1 \/ rng H2) by XBOOLE_1:4;
thus variables_in H1 '&' H2 c= variables_in H1 \/ variables_in H2
proof
let a be object;
assume
A3: a in variables_in H1 '&' H2;
then a <> 3 by Th137;
then not a in {3} by TARSKI:def 1;
then
A4: a in rng H1 \/ rng H2 by A2,A3,XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A3,XBOOLE_0:def 5;
hence thesis by A1,A4,XBOOLE_0:def 5;
end;
thus thesis by A2,A1,XBOOLE_1:7,33;
end;
theorem Th142:
variables_in All(x,H) = variables_in H \/ {x}
proof
A1: rng All(x,H) = rng (<*4*>^<*x*>) \/ rng H by FINSEQ_1:31
.= rng <*4*> \/ rng <*x*> \/ rng H by FINSEQ_1:31
.= {4} \/ rng <*x*> \/ rng H by FINSEQ_1:39
.= {4} \/ {x} \/ rng H by FINSEQ_1:39
.= {4} \/ ({x} \/ rng H) by XBOOLE_1:4;
thus variables_in All(x,H) c= variables_in H \/ {x}
proof
let a be object;
assume
A2: a in variables_in All(x,H);
then a <> 4 by Th137;
then not a in {4} by TARSKI:def 1;
then a in {x} \/ rng H by A1,A2,XBOOLE_0:def 3;
then
A3: a in {x} or a in rng H by XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A2,XBOOLE_0:def 5;
then a in rng H implies a in variables_in H by XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 3;
end;
let a be object;
assume a in variables_in H \/ {x};
then
A4: a in variables_in H or a in {x} by XBOOLE_0:def 3;
then a in {x} \/ rng H by XBOOLE_0:def 3;
then
A5: a in {4} \/ ({x} \/ rng H) by XBOOLE_0:def 3;
a in rng H & not a in {0,1,2,3,4} or a in {x} & x = a by A4,TARSKI:def 1
,XBOOLE_0:def 5;
then not a in {0,1,2,3,4} by Th136;
hence thesis by A1,A5,XBOOLE_0:def 5;
end;
theorem
variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2
proof
thus variables_in H1 'or' H2 = variables_in 'not' H1 '&' 'not' H2 by Th140
.= variables_in 'not' H1 \/ variables_in 'not' H2 by Th141
.= variables_in H1 \/ variables_in 'not' H2 by Th140
.= variables_in H1 \/ variables_in H2 by Th140;
end;
theorem Th144:
variables_in H1 => H2 = variables_in H1 \/ variables_in H2
proof
thus variables_in H1 => H2 = variables_in H1 '&' 'not' H2 by Th140
.= variables_in H1 \/ variables_in 'not' H2 by Th141
.= variables_in H1 \/ variables_in H2 by Th140;
end;
theorem
variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2
proof
thus variables_in H1 <=> H2 = variables_in H1 => H2 \/ variables_in H2 => H1
by Th141
.= variables_in H1 \/ variables_in H2 \/ variables_in H2 => H1 by Th144
.= variables_in H1 \/ variables_in H2 \/ (variables_in H1 \/
variables_in H2) by Th144
.= variables_in H1 \/ variables_in H2;
end;
theorem Th146:
variables_in Ex(x,H) = variables_in H \/ {x}
proof
thus variables_in Ex(x,H) = variables_in All(x,'not' H) by Th140
.= variables_in 'not' H \/ {x} by Th142
.= variables_in H \/ {x} by Th140;
end;
theorem Th147:
variables_in All(x,y,H) = variables_in H \/ {x,y}
proof
thus variables_in All(x,y,H) = variables_in All(y,H) \/ {x} by Th142
.= variables_in H \/ {y} \/ {x} by Th142
.= variables_in H \/ ({y} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {x,y} by ENUMSET1:1;
end;
theorem Th148:
variables_in Ex(x,y,H) = variables_in H \/ {x,y}
proof
thus variables_in Ex(x,y,H) = variables_in Ex(y,H) \/ {x} by Th146
.= variables_in H \/ {y} \/ {x} by Th146
.= variables_in H \/ ({y} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {x,y} by ENUMSET1:1;
end;
theorem
variables_in All(x,y,z,H) = variables_in H \/ {x,y,z}
proof
thus variables_in All(x,y,z,H) = variables_in All(y,z,H) \/ {x} by Th142
.= variables_in H \/ {y,z} \/ {x} by Th147
.= variables_in H \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {y,z,x} by ENUMSET1:3
.= variables_in H \/ {x,y,z} by ENUMSET1:59;
end;
theorem
variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z}
proof
thus variables_in Ex(x,y,z,H) = variables_in Ex(y,z,H) \/ {x} by Th146
.= variables_in H \/ {y,z} \/ {x} by Th148
.= variables_in H \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {y,z,x} by ENUMSET1:3
.= variables_in H \/ {x,y,z} by ENUMSET1:59;
end;
theorem
Free H c= variables_in H
proof
defpred P[ZF-formula] means Free $1 c= variables_in $1;
A1: P[H1] implies P['not' H1]
proof
assume Free H1 c= variables_in H1;
then Free 'not' H1 c= variables_in H1 by Th60;
hence thesis by Th140;
end;
A2: P[H1] & P[H2] implies P[H1 '&' H2]
proof
assume Free H1 c= variables_in H1 & Free H2 c= variables_in H2;
then Free H1 \/ Free H2 c= variables_in H1 \/ variables_in H2 by
XBOOLE_1:13;
then Free H1 '&' H2 c= variables_in H1 \/ variables_in H2 by Th61;
hence thesis by Th141;
end;
A3: P[H1] implies P[All(x,H1)]
proof
Free H1 \ {x} c= Free H1 by XBOOLE_1:36;
then
A4: Free All(x,H1) c= Free H1 by Th62;
variables_in H1 c= variables_in H1 \/ {x } by XBOOLE_1:7;
then
A5: variables_in H1 c= variables_in All(x, H1) by Th142;
assume Free H1 c= variables_in H1;
then Free H1 c= variables_in All(x,H1) by A5;
hence thesis by A4,XBOOLE_1:1;
end;
A6: P[x '=' y] & P[x 'in' y]
proof
variables_in (x '=' y) = {x,y} & variables_in (x 'in' y) = {x,y} by Th138
,Th139;
hence thesis by Th58,Th59;
end;
for H holds P[H] from ZFInduction(A6,A1,A2,A3);
hence thesis;
end;
definition
let H;
redefine func variables_in H -> non empty Subset of VAR; :: redefines variables_in (ZF_LANG1, definition)
coherence
proof
defpred P[ZF-formula] means variables_in $1 <> {};
A1: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2]
proof
let H1,H2;
variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2 by Th141;
hence thesis;
end;
A2: for H,x st P[H] holds P[All(x,H)]
proof
let H,x;
variables_in All(x,H) = variables_in H \/ {x} by Th142;
hence thesis;
end;
A3: for x,y holds P[x '=' y] & P[x 'in' y]
proof
let x,y;
variables_in x '=' y = {x,y} by Th138;
hence thesis by Th139;
end;
A4: for H st P[H] holds P['not' H] by Th140;
for H holds P[H] from ZFInduction(A3,A4,A1,A2);
then reconsider D = variables_in H as non empty set;
D c= VAR
proof
let a be object;
A5: rng H c= NAT by FINSEQ_1:def 4;
A6: 0+1 = 1;
assume
A7: a in D;
then a in rng H;
then reconsider i = a as Element of NAT by A5;
a <> 0 by A7,Th137;
then
A8: 1 <= i by A6,NAT_1:13;
A9: 3+1 = 4;
A10: 2+1 = 3;
A11: 1+1 = 2;
a <> 1 by A7,Th137;
then 1 < i by A8,XXREAL_0:1;
then
A12: 2 <= i by A11,NAT_1:13;
a <> 2 by A7,Th137;
then 2 < i by A12,XXREAL_0:1;
then
A13: 3 <= i by A10,NAT_1:13;
a <> 3 by A7,Th137;
then 3 < i by A13,XXREAL_0:1;
then
A14: 4 <= i by A9,NAT_1:13;
a <> 4 by A7,Th137;
then
A15: 4 < i by A14,XXREAL_0:1;
4+1 = 5;
then 5 <= i by A15,NAT_1:13;
hence thesis;
end;
hence thesis;
end;
end;
definition
let H,x,y;
func H/(x,y) -> Function means
: Def3:
dom it = dom H & for a being object st a in dom H
holds (H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a);
existence
proof
deffunc G(object) = H.$1;
deffunc F(object) = y;
set A = dom H;
defpred C[object] means H.$1 = x;
thus ex f being Function st dom f = A &
for a being object st a in A holds (C[a]
implies f.a = F(a)) & (not C[a] implies f.a = G(a)) from PARTFUN1:sch 1;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = dom H and
A2: for a being object st a in dom H
holds (H.a = x implies f1.a = y) & (H.a <> x
implies f1.a = H.a) and
A3: dom f2 = dom H and
A4: for a being object st a in dom H
holds (H.a = x implies f2.a = y) & (H.a <> x
implies f2.a = H.a);
now
let a be object;
assume
A5: a in dom H;
then
A6: H.a <> x implies f1.a = H.a by A2;
H.a = x implies f1.a = y by A2,A5;
hence f1.a = f2.a by A4,A5,A6;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
theorem Th152:
(x1 '=' x2)/(y1,y2) = z1 '=' z2 iff x1 <> y1 & x2 <> y1 & z1 =
x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 &
z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2
proof
set H = x1 '=' x2, Hz = z1 '=' z2;
set f = H/(y1,y2);
A1: H.1 = 0 & y1 <> 0 by Th135,ZF_LANG:15;
H is being_equality;
then
A2: H is atomic;
then
A3: len H = 3 by ZF_LANG:11;
then
A4: dom H = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
Hz is being_equality;
then
A5: Hz is atomic;
then len Hz = 3 by ZF_LANG:11;
then
A6: dom Hz = Seg 3 by FINSEQ_1:def 3;
Var1 Hz = z1 by Th1;
then
A7: Hz.2 = z1 by A5,ZF_LANG:35;
Var2 Hz = z2 by Th1;
then
A8: Hz.3 = z2 by A5,ZF_LANG:35;
A9: Var2 H = x2 by Th1;
then
A10: H.3 = x2 by A2,ZF_LANG:35;
A11: Var1 H = x1 by Th1;
then
A12: H.2 = x1 by A2,ZF_LANG:35;
thus (x1 '=' x2)/(y1,y2) = z1 '=' z2 implies x1 <> y1 & x2 <> y1 & z1 = x1 &
z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 =
x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2
proof
assume
A13: (x1 '=' x2)/(y1,y2) = z1 '=' z2;
per cases;
case
A14: x1 <> y1 & x2 <> y1;
2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
hence thesis by A12,A10,A7,A8,A13,A14,Def3;
end;
case
A15: x1 = y1 & x2 <> y1;
A16: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.2 = y1 by A2,A11,A15,ZF_LANG:35;
hence thesis by A10,A7,A8,A13,A15,A16,Def3;
end;
case
A17: x1 <> y1 & x2 = y1;
A18: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.3 = y1 by A2,A9,A17,ZF_LANG:35;
hence thesis by A12,A7,A8,A13,A17,A18,Def3;
end;
case
A19: x1 = y1 & x2 = y1;
A20: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.2 = y1 & H.3 = y1 by A2,A11,A9,A19,ZF_LANG:35;
hence thesis by A7,A8,A13,A20,Def3;
end;
end;
A21: dom H = Seg 3 by A3,FINSEQ_1:def 3;
A22: dom f = dom H by Def3;
A23: now
assume
A24: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;
now
let a be object;
assume
A25: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A1,A24,A25,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
A26: Hz.1 = 0 by ZF_LANG:15;
A27: now
assume
A28: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;
now
let a be object;
assume
A29: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A28,A29,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
A30: now
assume
A31: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;
now
let a be object;
assume
A32: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A31,A32,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
now
assume
A33: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;
now
let a be object;
assume
A34: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A33,A34,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
hence thesis by A23,A27,A30;
end;
theorem Th153:
ex z1,z2 st (x1 '=' x2)/(y1,y2) = z1 '=' z2
proof
x1 <> y1 & x2 <> y1 or x1 = y1 & x2 <> y1 or x1 <> y1 & x2 = y1 or x1 =
y1 & x2 = y1;
then consider z1,z2 such that
A1: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 =
y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 &
z1 = y2 & z2 = y2;
take z1,z2;
thus thesis by A1,Th152;
end;
theorem Th154:
(x1 'in' x2)/(y1,y2) = z1 'in' z2 iff x1 <> y1 & x2 <> y1 & z1
= x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1
& z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2
proof
set H = x1 'in' x2, Hz = z1 'in' z2;
set f = H/(y1,y2);
A1: H.1 = 1 & y1 <> 1 by Th135,ZF_LANG:15;
H is being_membership;
then
A2: H is atomic;
then
A3: len H = 3 by ZF_LANG:11;
then
A4: dom H = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
Hz is being_membership;
then
A5: Hz is atomic;
then len Hz = 3 by ZF_LANG:11;
then
A6: dom Hz = Seg 3 by FINSEQ_1:def 3;
Var1 Hz = z1 by Th2;
then
A7: Hz.2 = z1 by A5,ZF_LANG:35;
Var2 Hz = z2 by Th2;
then
A8: Hz.3 = z2 by A5,ZF_LANG:35;
A9: Var2 H = x2 by Th2;
then
A10: H.3 = x2 by A2,ZF_LANG:35;
A11: Var1 H = x1 by Th2;
then
A12: H.2 = x1 by A2,ZF_LANG:35;
thus (x1 'in' x2)/(y1,y2) = z1 'in' z2 implies x1 <> y1 & x2 <> y1 & z1 = x1
& z2 = x2 or x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1
= x1 & z2 = y2 or x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2
proof
assume
A13: (x1 'in' x2)/(y1,y2) = z1 'in' z2;
per cases;
case
A14: x1 <> y1 & x2 <> y1;
2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
hence thesis by A12,A10,A7,A8,A13,A14,Def3;
end;
case
A15: x1 = y1 & x2 <> y1;
A16: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.2 = y1 by A2,A11,A15,ZF_LANG:35;
hence thesis by A10,A7,A8,A13,A15,A16,Def3;
end;
case
A17: x1 <> y1 & x2 = y1;
A18: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.3 = y1 by A2,A9,A17,ZF_LANG:35;
hence thesis by A12,A7,A8,A13,A17,A18,Def3;
end;
case
A19: x1 = y1 & x2 = y1;
A20: 2 in dom H & 3 in dom H by A4,ENUMSET1:def 1;
H.2 = y1 & H.3 = y1 by A2,A11,A9,A19,ZF_LANG:35;
hence thesis by A7,A8,A13,A20,Def3;
end;
end;
A21: dom H = Seg 3 by A3,FINSEQ_1:def 3;
A22: dom f = dom H by Def3;
A23: now
assume
A24: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;
now
let a be object;
assume
A25: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A1,A24,A25,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
A26: Hz.1 = 1 by ZF_LANG:15;
A27: now
assume
A28: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;
now
let a be object;
assume
A29: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A28,A29,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
A30: now
assume
A31: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;
now
let a be object;
assume
A32: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A31,A32,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
now
assume
A33: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;
now
let a be object;
assume
A34: a in dom H;
then a = 1 or a = 2 or a = 3 by A4,ENUMSET1:def 1;
hence Hz.a = f.a by A12,A10,A26,A7,A8,A1,A33,A34,Def3;
end;
hence f = Hz by A22,A21,A6,FUNCT_1:2;
end;
hence thesis by A23,A27,A30;
end;
theorem Th155:
ex z1,z2 st (x1 'in' x2)/(y1,y2) = z1 'in' z2
proof
x1 <> y1 & x2 <> y1 or x1 = y1 & x2 <> y1 or x1 <> y1 & x2 = y1 or x1 =
y1 & x2 = y1;
then consider z1,z2 such that
A1: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 or x1 = y1 & x2 <> y1 & z1 =
y2 & z2 = x2 or x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 or x1 = y1 & x2 = y1 &
z1 = y2 & z2 = y2;
take z1,z2;
thus thesis by A1,Th154;
end;
theorem Th156:
'not' F = ('not' H)/(x,y) iff F = H/(x,y)
proof
set N = ('not' H)/(x,y);
A1: len <*2*> = 1 by FINSEQ_1:39;
A2: dom 'not' F = Seg len 'not' F & dom 'not' H = Seg len 'not' H by
FINSEQ_1:def 3;
A3: len 'not' F = len <*2*> + len F & len 'not' H = len <*2*> + len H by
FINSEQ_1:22;
A4: dom F = Seg len F & dom H = Seg len H by FINSEQ_1:def 3;
thus 'not' F = ('not' H)/(x,y) implies F = H/(x,y)
proof
assume
A5: 'not' F = N;
then
A6: dom 'not' F = dom 'not' H by Def3;
then
A7: len 'not' F = len 'not' H by FINSEQ_3:29;
A8: now
let a be object;
assume
A9: a in dom F;
then reconsider i = a as Element of NAT;
A10: F.a = N.(1+i) & 1+i in dom N by A1,A5,A9,FINSEQ_1:28,def 7;
A11: ('not' H).(1+i) = H.a by A1,A4,A3,A7,A9,FINSEQ_1:def 7;
then
A12: H.a = x implies F.a = y by A5,A6,A10,Def3;
A13: H.a <> x implies F.a = H.a by A5,A6,A10,A11,Def3;
H.a = x implies H/(x,y).a = y by A4,A3,A7,A9,Def3;
hence F.a = H/(x,y).a by A4,A3,A7,A9,A12,A13,Def3;
end;
A14: dom H = dom (H/(x,y)) by Def3;
dom F = dom H by A3,A7,FINSEQ_3:29;
hence thesis by A14,A8,FUNCT_1:2;
end;
assume
A15: F = H/(x,y);
then
A16: dom F = dom H by Def3;
then
A17: len F = len H by FINSEQ_3:29;
A18: dom <*2*> = {1} by FINSEQ_1:2,def 8;
A19: now
let a be object;
assume
A20: a in dom 'not' F;
then reconsider i = a as Element of NAT;
A21: now
A22: ('not' H).a <> x implies N.a = ('not' H).a by A2,A3,A17,A20,Def3;
given j be Nat such that
A23: j in dom F and
A24: i = 1+j;
A25: H.j = ('not' H).i & F.j = ('not' F).i by A1,A16,A23,A24,FINSEQ_1:def 7;
then
A26: ('not' H).a = x implies ('not' F).a = y by A15,A16,A23,Def3;
('not' H).a <> x implies ('not' F).a = ('not' H).a by A15,A16,A23,A25
,Def3;
hence ('not' F).a = N.a by A2,A3,A17,A20,A26,A22,Def3;
end;
now
A27: ('not' H).1 = 2 & 2 <> x by Th135,FINSEQ_1:41;
assume i in {1};
then
A28: i = 1 by TARSKI:def 1;
then ('not' F).i = 2 by FINSEQ_1:41;
hence ('not' F).a = N.a by A2,A3,A17,A20,A28,A27,Def3;
end;
hence ('not' F).a = N.a by A1,A18,A20,A21,FINSEQ_1:25;
end;
dom 'not' F = dom N by A2,A3,A17,Def3;
hence thesis by A19,FUNCT_1:2;
end;
Lm1: G1 = H1/(x,y) & G2 = H2/(x,y) implies G1 '&' G2 = (H1 '&' H2)/(x,y)
proof
set N = (H1 '&' H2)/(x,y);
A1: dom <*3*> = {1} by FINSEQ_1:2,def 8;
A2: dom (G1 '&' G2) = Seg len (G1 '&' G2) & dom (H1 '&' H2) = Seg len (H1
'&' H2 ) by FINSEQ_1:def 3;
A3: len <*3*> = 1 by FINSEQ_1:39;
then
A4: len (<*3*>^G1) = 1+len G1 by FINSEQ_1:22;
then
A5: len (G1 '&' G2) = 1+len G1 + len G2 by FINSEQ_1:22;
A6: len (<*3*>^H1) = 1+len H1 by A3,FINSEQ_1:22;
then
A7: len (H1 '&' H2) = 1+len H1 + len H2 by FINSEQ_1:22;
A8: dom (<*3*>^H1) = Seg (1+len H1) by A6,FINSEQ_1:def 3;
A9: dom N = dom (H1 '&' H2) by Def3;
assume that
A10: G1 = H1/(x,y) and
A11: G2 = H2/(x,y);
A12: dom G1 = dom H1 by A10,Def3;
then
A13: len G1 = len H1 by FINSEQ_3:29;
A14: dom G2 = dom H2 by A11,Def3;
then len G2 = len H2 by FINSEQ_3:29;
then
A15: dom N = dom (G1 '&' G2) by A2,A5,A7,A13,Def3;
A16: dom (<*3*>^G1) = Seg (1+len G1) by A4,FINSEQ_1:def 3;
now
let a be object;
assume
A17: a in dom N;
then reconsider i = a as Element of NAT by A15;
A18: now
A19: now
assume i in {1};
then
A20: i = 1 by TARSKI:def 1;
(H1 '&' H2).1 = 3 & x <> 3 by Th135,ZF_LANG:16;
then N.i = 3 by A9,A17,A20,Def3;
hence N.a = (G1 '&' G2).a by A20,ZF_LANG:16;
end;
assume
A21: i in dom (<*3*>^G1);
then
A22: (G1 '&' G2).i = (<*3*>^G1).i & (H1 '&' H2).i = (<*3*>^H1).i by A16,A8,A13
,FINSEQ_1:def 7;
now
A23: (H1 '&' H2).a <> x implies N.a = (H1 '&' H2).a by A9,A17,Def3;
given j be Nat such that
A24: j in dom G1 and
A25: i = 1+j;
A26: G1.j = (G1 '&' G2).i & H1.j = (H1 '&' H2).i by A3,A12,A22,A24,A25,
FINSEQ_1:def 7;
then
A27: (H1 '&' H2).a = x implies (G1 '&' G2).a = y by A10,A12,A24,Def3;
(H1 '&' H2).a <> x implies (G1 '&' G2).a = (H1 '&' H2).a by A10,A12,A24
,A26,Def3;
hence (G1 '&' G2).a = N.a by A9,A17,A27,A23,Def3;
end;
hence (G1 '&' G2).a = N.a by A3,A1,A21,A19,FINSEQ_1:25;
end;
now
A28: (H1 '&' H2).a <> x implies N.a = (H1 '&' H2).a by A9,A17,Def3;
given j be Nat such that
A29: j in dom G2 and
A30: i = 1+len G1+j;
A31: G2.j = (G1 '&' G2).i & H2.j = (H1 '&' H2).i by A4,A6,A14,A13,A29,A30,
FINSEQ_1:def 7;
then
A32: (H1 '&' H2).a = x implies (G1 '&' G2).a = y by A11,A14,A29,Def3;
(H1 '&' H2).a <> x implies (G1 '&' G2).a = (H1 '&' H2).a by A11,A14,A29
,A31,Def3;
hence (G1 '&' G2).a = N.a by A9,A17,A28,A32,Def3;
end;
hence (G1 '&' G2).a = N.a by A4,A15,A17,A18,FINSEQ_1:25;
end;
hence thesis by A15,FUNCT_1:2;
end;
Lm2: F = H/(x,y) & (z = s & s <> x or z = y & s = x) implies All(z,F) = All(s,
H)/(x,y)
proof
set N = All(s,H)/(x,y);
A1: len <*4*> = 1 & 1+1 = 2 by FINSEQ_1:39;
len <*s*> = 1 by FINSEQ_1:39;
then
A2: len (<*4*>^<*s*>) = 2 by A1,FINSEQ_1:22;
then
A3: dom (<*4*>^<*s*>) = {1,2} by FINSEQ_1:2,def 3;
len All(s,H) = 2+len H by A2,FINSEQ_1:22;
then
A4: dom All(s,H) = Seg (2+len H) by FINSEQ_1:def 3;
A5: <*4*>^<*z*> = <*4,z*> & <*4*>^<*s*> = <*4,s*> by FINSEQ_1:def 9;
A6: dom N = dom All(s,H) by Def3;
assume that
A7: F = H/(x,y) and
A8: z = s & s <> x or z = y & s = x;
A9: dom F = dom H by A7,Def3;
len <*z*> = 1 by FINSEQ_1:39;
then
A10: len (<*4*>^<*z*>) = 2 by A1,FINSEQ_1:22;
then
A11: dom (<*4*>^<*z*>) = {1,2} by FINSEQ_1:2,def 3;
A12: now
let a be object;
assume
A13: a in dom N;
then reconsider a1=a as Element of NAT by A6;
A14: now
A15: x <> 4 & <*4,z*>.1 = 4 by Th135;
assume
A18: a in {1,2};
then
A19: a = 1 or a = 2 by TARSKI:def 2;
All(z,F).a1 = <*4,z*>.a1 & All(s,H).a1 = <*4,s*>.a1 by A11,A3,A5,A18,
FINSEQ_1:def 7;
hence All(z,F).a = All(s,H)/(x,y).a by A8,A6,A13,A19,A15,Def3;
end;
now
A20: All(s,H).a <> x implies All(s,H)/(x,y).a = All(s,H).a by A6,A13,Def3;
given i be Nat such that
A21: i in dom H and
A22: a1 = 2+i;
A23: All(z,F).a = F.i & All(s,H).a = H.i by A10,A2,A9,A21,A22,FINSEQ_1:def 7;
then
A24: All(s,H).a = x implies All(z,F).a = y by A7,A21,Def3;
All(s,H).a <> x implies All(z,F).a = All(s,H).a by A7,A21,A23,Def3;
hence All(z,F).a = All(s,H)/(x,y).a by A6,A13,A24,A20,Def3;
end;
hence All(z,F).a = All(s,H)/(x,y).a by A2,A3,A6,A13,A14,FINSEQ_1:25;
end;
len All(z,F) = 2+len F by A10,FINSEQ_1:22;
then dom All(z,F) = Seg (2+len F) by FINSEQ_1:def 3;
then dom All(s,H) = dom All(z,F) by A4,A9,FINSEQ_3:29;
hence thesis by A6,A12,FUNCT_1:2;
end;
theorem Th157:
H/(x,y) in WFF
proof
defpred P[ZF-formula] means $1/(x,y) in WFF;
A1: for H st P[H] holds P[('not' H)]
proof
let H;
assume H/(x,y) in WFF;
then reconsider F = H/(x,y) as ZF-formula by ZF_LANG:4;
'not' F = ('not' H)/(x,y) by Th156;
hence thesis by ZF_LANG:4;
end;
A2: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2]
proof
let H1,H2;
assume H1/(x,y) in WFF & H2/(x,y) in WFF;
then reconsider F1 = H1/(x,y), F2 = H2/(x,y) as ZF-formula by ZF_LANG:4;
F1 '&' F2 = (H1 '&' H2)/(x,y) by Lm1;
hence thesis by ZF_LANG:4;
end;
A3: for H,z st P[H] holds P[All(z,H)]
proof
let H,z;
assume H/(x,y) in WFF;
then reconsider F = H/(x,y) as ZF-formula by ZF_LANG:4;
z <> x or z = x;
then consider s such that
A4: s = z & z <> x or s = y & z = x;
All(s,F) = All(z,H)/(x,y) by A4,Lm2;
hence thesis by ZF_LANG:4;
end;
A5: for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2]
proof
let x1,x2;
( ex y1,y2 st (x1 '=' x2)/(x,y) = y1 '=' y2)& ex z1,z2 st (x1 'in' x2)
/(x,y) = z1 'in' z2 by Th153,Th155;
hence thesis by ZF_LANG:4;
end;
for H holds P[H] from ZFInduction(A5,A1,A2,A3);
hence thesis;
end;
definition
let H,x,y;
redefine func H/(x,y) -> ZF-formula; :: redefines / (ZF_LANG1, definition)
coherence
by Th157,ZF_LANG:4;
end;
theorem Th158:
G1 '&' G2 = (H1 '&' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
thus G1 '&' G2 = (H1 '&' H2)/(x,y) implies G1 = H1/(x,y) & G2 = H2/(x,y)
proof
assume G1 '&' G2 = (H1 '&' H2)/(x,y);
then G1 '&' G2 = (H1/(x,y)) '&' (H2/(x,y)) by Lm1;
hence thesis by ZF_LANG:30;
end;
thus thesis by Lm1;
end;
theorem Th159:
z <> x implies (All(z,G) = All(z,H)/(x,y) iff G = H/(x,y))
proof
assume
A1: z <> x;
thus All(z,G) = All(z,H)/(x,y) implies G = H/(x,y)
proof
assume All(z,G) = All(z,H)/(x,y);
then All(z,G) = All(z,H/(x,y)) by A1,Lm2;
hence thesis by ZF_LANG:3;
end;
thus thesis by A1,Lm2;
end;
theorem Th160:
All(y,G) = All(x,H)/(x,y) iff G = H/(x,y)
proof
thus All(y,G) = All(x,H)/(x,y) implies G = H/(x,y)
proof
assume All(y,G) = All(x,H)/(x,y);
then All(y,G) = All(y,H/(x,y)) by Lm2;
hence thesis by ZF_LANG:3;
end;
thus thesis by Lm2;
end;
theorem Th161:
G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x, y)
proof
'not' G1 = ('not' H1)/(x,y) & 'not' G2 = ('not' H2)/(x,y) iff 'not' G1
'&' 'not' G2 = ('not' H1 '&' 'not' H2)/(x,y) by Th158;
hence thesis by Th156;
end;
theorem Th162:
G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
G1 = H1/(x,y) & 'not' G2 = ('not' H2)/(x,y) iff G1 '&' 'not' G2 = (H1
'&' 'not' H2)/(x,y) by Th158;
hence thesis by Th156;
end;
theorem Th163:
G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 => G2 = (H1 => H2)/(x,y) & G2 => G1
= (H2 => H1)/(x,y) by Th158;
hence thesis by Th162;
end;
theorem Th164:
z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y))
proof
assume z <> x;
then 'not' G = ('not' H)/(x,y) iff All(z,'not' G) = All(z,'not' H)/(x,y) by
Th159;
hence thesis by Th156;
end;
theorem Th165:
Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y)
proof
'not' G = ('not' H)/(x,y) iff All(y,'not' G) = All(x,'not' H)/(x,y) by Th160;
hence thesis by Th156;
end;
theorem
H is being_equality iff H/(x,y) is being_equality
proof
thus H is being_equality implies H/(x,y) is being_equality
by Th153;
assume H/(x,y) is being_equality;
then
A1: H/(x,y).1 = 0 by ZF_LANG:18;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then
A2: 1 in dom H by FINSEQ_3:25;
y <> 0 by Th135;
then H.1 <> x by A1,A2,Def3;
then 0 = H.1 by A1,A2,Def3;
hence thesis by ZF_LANG:24;
end;
theorem
H is being_membership iff H/(x,y) is being_membership
proof
thus H is being_membership implies H/(x,y) is being_membership
by Th155;
assume H/(x,y) is being_membership;
then
A1: H/(x,y).1 = 1 by ZF_LANG:19;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then
A2: 1 in dom H by FINSEQ_3:25;
y <> 1 by Th135;
then H.1 <> x by A1,A2,Def3;
then 1 = H.1 by A1,A2,Def3;
hence thesis by ZF_LANG:25;
end;
theorem Th168:
H is negative iff H/(x,y) is negative
proof
thus H is negative implies H/(x,y) is negative
proof
given H1 such that
A1: H = 'not' H1;
H/(x,y) = 'not' (H1/(x,y)) by A1,Th156;
hence thesis;
end;
assume H/(x,y) is negative;
then
A2: H/(x,y).1 = 2 by ZF_LANG:20;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then
A3: 1 in dom H by FINSEQ_3:25;
y <> 2 by Th135;
then H.1 <> x by A2,A3,Def3;
then 2 = H.1 by A2,A3,Def3;
hence thesis by ZF_LANG:26;
end;
theorem Th169:
H is conjunctive iff H/(x,y) is conjunctive
proof
thus H is conjunctive implies H/(x,y) is conjunctive
proof
given H1,H2 such that
A1: H = H1 '&' H2;
H/(x,y) = (H1/(x,y)) '&' (H2/(x,y)) by A1,Th158;
hence thesis;
end;
assume H/(x,y) is conjunctive;
then
A2: H/(x,y).1 = 3 by ZF_LANG:21;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then
A3: 1 in dom H by FINSEQ_3:25;
y <> 3 by Th135;
then H.1 <> x by A2,A3,Def3;
then 3 = H.1 by A2,A3,Def3;
hence thesis by ZF_LANG:27;
end;
theorem Th170:
H is universal iff H/(x,y) is universal
proof
thus H is universal implies H/(x,y) is universal
proof
given z,H1 such that
A1: H = All(z,H1);
z = x or z <> x;
then consider s such that
A2: z = x & s = y or z <> x & s = z;
H/(x,y) = All(s,H1/(x,y)) by A1,A2,Th159,Th160;
hence thesis;
end;
assume H/(x,y) is universal;
then
A3: H/(x,y).1 = 4 by ZF_LANG:22;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then
A4: 1 in dom H by FINSEQ_3:25;
y <> 4 by Th135;
then H.1 <> x by A3,A4,Def3;
then 4 = H.1 by A3,A4,Def3;
hence thesis by ZF_LANG:28;
end;
theorem
H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/
(x, y )
proof
assume
A1: H is negative;
then H/(x,y) is negative by Th168;
then
A2: H/(x,y) = 'not' the_argument_of (H/(x,y)) by ZF_LANG:def 30;
H = 'not' the_argument_of H by A1,ZF_LANG:def 30;
hence thesis by A2,Th156;
end;
theorem
H is conjunctive implies the_left_argument_of (H/(x,y)) = (
the_left_argument_of H)/(x,y) & the_right_argument_of (H/(x,y)) = (
the_right_argument_of H)/(x,y)
proof
assume
A1: H is conjunctive;
then H/(x,y) is conjunctive by Th169;
then
A2: H/(x,y) = (the_left_argument_of (H/(x,y))) '&' (the_right_argument_of (H
/(x,y))) by ZF_LANG:40;
H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1,ZF_LANG:40;
hence thesis by A2,Th158;
end;
theorem
H is universal implies the_scope_of (H/(x,y)) = (the_scope_of H)/(x,y)
& (bound_in H = x implies bound_in (H/(x,y)) = y) & (bound_in H <> x implies
bound_in (H/(x,y)) = bound_in H)
proof
assume
A1: H is universal;
then H/(x,y) is universal by Th170;
then
A2: H/(x,y) = All(bound_in (H/(x,y)),the_scope_of (H/(x,y))) by ZF_LANG:44;
A3: H = All(bound_in H,the_scope_of H) by A1,ZF_LANG:44;
then
A4: bound_in H <> x implies H/(x,y) = All(bound_in H,(the_scope_of H)/(x,y)
) by Th159;
bound_in H = x implies H/(x,y) = All(y,(the_scope_of H)/(x,y)) by A3,Th160;
hence thesis by A2,A4,ZF_LANG:3;
end;
theorem Th174:
H is disjunctive iff H/(x,y) is disjunctive
proof
set G = H/(x,y);
thus H is disjunctive implies H/(x,y) is disjunctive
proof
given H1,H2 such that
A1: H = H1 'or' H2;
H/(x,y) = (H1/(x,y)) 'or' (H2/(x,y)) by A1,Th161;
hence thesis;
end;
given G1,G2 such that
A2: G = G1 'or' G2;
G is negative by A2;
then H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9;
A4: 'not' G1 '&' 'not' G2 = H9/(x,y) by A2,A3,Th156;
then H9/(x,y) is conjunctive;
then H9 is conjunctive by Th169;
then consider H1,H2 such that
A5: H9 = H1 '&' H2;
'not' G2 = H2/(x,y) by A4,A5,Th158;
then H2/(x,y) is negative;
then H2 is negative by Th168;
then consider p2 such that
A6: H2 = 'not' p2;
'not' G1 = H1/(x,y) by A4,A5,Th158;
then H1/(x,y) is negative;
then H1 is negative by Th168;
then consider p1 such that
A7: H1 = 'not' p1;
H = p1 'or' p2 by A3,A5,A7,A6;
hence thesis;
end;
theorem Th175:
H is conditional iff H/(x,y) is conditional
proof
set G = H/(x,y);
thus H is conditional implies H/(x,y) is conditional
proof
given H1,H2 such that
A1: H = H1 => H2;
H/(x,y) = (H1/(x,y)) => (H2/(x,y)) by A1,Th162;
hence thesis;
end;
given G1,G2 such that
A2: G = G1 => G2;
G is negative by A2;
then H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9;
A4: G1 '&' 'not' G2 = H9/(x,y) by A2,A3,Th156;
then H9/(x,y) is conjunctive;
then H9 is conjunctive by Th169;
then consider H1,H2 such that
A5: H9 = H1 '&' H2;
'not' G2 = H2/(x,y) by A4,A5,Th158;
then H2/(x,y) is negative;
then H2 is negative by Th168;
then consider p2 such that
A6: H2 = 'not' p2;
H = H1 => p2 by A3,A5,A6;
hence thesis;
end;
theorem Th176:
H is biconditional implies H/(x,y) is biconditional
proof
given H1,H2 such that
A1: H = H1 <=> H2;
H/(x,y) = (H1/(x,y)) <=> (H2/(x,y)) by A1,Th163;
hence thesis;
end;
theorem Th177:
H is existential iff H/(x,y) is existential
proof
thus H is existential implies H/(x,y) is existential
proof
given z,H1 such that
A1: H = Ex(z,H1);
z = x or z <> x;
then consider s such that
A2: z = x & s = y or z <> x & s = z;
H/(x,y) = Ex(s,H1/(x,y)) by A1,A2,Th164,Th165;
hence thesis;
end;
given z,G such that
A3: H/(x,y) = Ex(z,G);
H/(x,y) is negative by A3;
then H is negative by Th168;
then consider H1 such that
A4: H = 'not' H1;
bound_in H1 = x or bound_in H1 <> x;
then consider s such that
A5: bound_in H1 = x & s = y or bound_in H1 <> x & s = bound_in H1;
A6: H1/(x,y) = All(z,'not' G) by A3,A4,Th156;
then H1/(x,y) is universal;
then H1 is universal by Th170;
then
A7: H1 = All(bound_in H1, the_scope_of H1) by ZF_LANG:44;
then All(z,'not' G) = All(s,(the_scope_of H1)/(x,y)) by A6,A5,Th159,Th160;
then 'not' G = (the_scope_of H1)/(x,y) by ZF_LANG:3;
then (the_scope_of H1)/(x,y) is negative;
then the_scope_of H1 is negative by Th168;
then H = Ex(bound_in H1, the_argument_of the_scope_of H1) by A4,A7,
ZF_LANG:def 30;
hence thesis;
end;
theorem
H is disjunctive implies the_left_argument_of (H/(x,y)) = (
the_left_argument_of H)/(x,y) & the_right_argument_of (H/(x,y)) = (
the_right_argument_of H)/(x,y)
proof
assume
A1: H is disjunctive;
then H/(x,y) is disjunctive by Th174;
then
A2: H/(x,y) = (the_left_argument_of (H/(x,y))) 'or' (the_right_argument_of (
H/(x,y))) by ZF_LANG:41;
H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1,ZF_LANG:41;
hence thesis by A2,Th161;
end;
theorem
H is conditional implies the_antecedent_of (H/(x,y)) = (
the_antecedent_of H)/(x,y) & the_consequent_of (H/(x,y)) = (the_consequent_of H
)/(x,y)
proof
assume
A1: H is conditional;
then H/(x,y) is conditional by Th175;
then
A2: H/(x,y) = (the_antecedent_of (H/(x,y))) => (the_consequent_of (H/(x,y)))
by ZF_LANG:47;
H = (the_antecedent_of H) => (the_consequent_of H) by A1,ZF_LANG:47;
hence thesis by A2,Th162;
end;
theorem
H is biconditional implies the_left_side_of (H/(x,y)) = (
the_left_side_of H)/(x,y) & the_right_side_of (H/(x,y)) = (the_right_side_of H)
/(x,y)
proof
assume H is biconditional;
then H = (the_left_side_of H) <=> (the_right_side_of H) & H/(x,y) = (
the_left_side_of (H/(x,y))) <=> (the_right_side_of (H/(x,y))) by Th176,
ZF_LANG:49;
hence thesis by Th163;
end;
theorem
H is existential implies the_scope_of (H/(x,y)) = (the_scope_of H)/(x,
y) & (bound_in H = x implies bound_in (H/(x,y)) = y) & (bound_in H <> x implies
bound_in (H/(x,y)) = bound_in H)
proof
assume
A1: H is existential;
then H/(x,y) is existential by Th177;
then
A2: H/(x,y) = Ex(bound_in (H/(x,y)),the_scope_of (H/(x,y))) by ZF_LANG:45;
A3: H = Ex(bound_in H,the_scope_of H) by A1,ZF_LANG:45;
then
A4: bound_in H <> x implies H/(x,y) = Ex(bound_in H,(the_scope_of H)/(x,y))
by Th164;
bound_in H = x implies H/(x,y) = Ex(y,(the_scope_of H)/(x,y)) by A3,Th165;
hence thesis by A2,A4,ZF_LANG:34;
end;
theorem Th182:
not x in variables_in H implies H/(x,y) = H
proof
assume
A1: not x in variables_in H;
A2: not x in {0,1,2,3,4} by Th136;
A3: now
let a be object;
assume
A4: a in dom H;
then
A5: H.a in rng H by FUNCT_1:def 3;
H.a <> x implies H/(x,y).a = H.a by A4,Def3;
hence H/(x,y).a = H.a by A1,A2,A5,XBOOLE_0:def 5;
end;
dom H = dom (H/(x,y)) by Def3;
hence thesis by A3,FUNCT_1:2;
end;
theorem
H/(x,x) = H
proof
A1: now
let a be object;
assume
A2: a in dom H;
then H.a = x implies H/(x,x).a = x by Def3;
hence H.a = H/(x,x).a by A2,Def3;
end;
dom (H/(x,x)) = dom H by Def3;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th184:
x <> y implies not x in variables_in (H/(x,y))
proof
assume
A1: x <> y;
assume x in variables_in (H/(x,y));
then consider a being object such that
A2: a in dom (H/(x,y)) and
A3: x = H/(x,y).a by FUNCT_1:def 3;
A4: dom (H/(x,y)) = dom H by Def3;
then H.a = x implies H/(x,y).a = y by A2,Def3;
hence contradiction by A1,A2,A3,A4,Def3;
end;
theorem
x in variables_in H implies y in variables_in (H/(x,y))
proof
assume x in variables_in H;
then consider a being object such that
A1: a in dom H and
A2: x = H.a by FUNCT_1:def 3;
A3: dom (H/(x,y)) = dom H by Def3;
A4: not y in {0,1,2,3,4} by Th136;
H/(x,y).a = y by A1,A2,Def3;
then y in rng (H/(x,y)) by A1,A3,FUNCT_1:def 3;
hence thesis by A4,XBOOLE_0:def 5;
end;
theorem
x <> y implies (H/(x,y))/(x,z) = H/(x,y)
proof
assume x <> y;
then not x in variables_in (H/(x,y)) by Th184;
hence thesis by Th182;
end;
theorem
variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y}
proof
let a be object;
assume
A1: a in variables_in (H/(x,y));
then reconsider z = a as Variable;
consider b being object such that
A2: b in dom (H/(x,y)) and
A3: z = H/(x,y).b by A1,FUNCT_1:def 3;
A4: dom (H/(x,y)) = dom H by Def3;
then
A5: H.b <> x implies z = H.b by A2,A3,Def3;
H.b = x implies z = y by A2,A3,A4,Def3;
then z in {y} or z in rng H & not z in {0,1,2,3,4} & not z in {x} by A2,A4,A5
,Th136,FUNCT_1:def 3,TARSKI:def 1;
then z in {y} or z in rng H \ {0,1,2,3,4} & not z in {x} by XBOOLE_0:def 5;
then z in {y} or z in variables_in H \ {x} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;