Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ZF_LANG, FUNCT_1, FINSEQ_1, BOOLE, ZF_MODEL, ARYTM_3, QC_LANG1,
RELAT_1, FINSET_1, QC_LANG3;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0,
NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG, ZF_MODEL;
constructors ENUMSET1, NAT_1, ZF_MODEL, XREAL_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSET_1, ZF_LANG, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3,
MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ZF_LANG, ZF_MODEL, XBOOLE_0;
theorems AXIOMS, TARSKI, ZFMISC_1, ENUMSET1, REAL_1, NAT_1, FINSEQ_1,
FINSEQ_3, FINSET_1, FUNCT_1, FUNCT_2, ZF_LANG, ZF_MODEL, ZFMODEL1,
RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_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 for set, X for set;
theorem
Th1: Var1 (x '=' y) = x & Var2 (x '=' y) = y
proof x '=' y is_equality by ZF_LANG:16;
then x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:53;
hence thesis by ZF_LANG:6;
end;
theorem
Th2: Var1 (x 'in' y) = x & Var2 (x 'in' y) = y
proof x 'in' y is_membership by ZF_LANG:16;
then x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:54;
hence thesis by ZF_LANG:7;
end;
theorem
Th3: the_argument_of 'not' p = p
proof 'not' p is negative by ZF_LANG:16;
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 by ZF_LANG:16;
then p '&' q = (the_left_argument_of (p '&' q)) '&'
(the_right_argument_of (p '&' q)) by ZF_LANG:58;
hence thesis by ZF_LANG:47;
end;
theorem
the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q
proof p 'or' q is disjunctive by ZF_LANG:22;
then p 'or' q = (the_left_argument_of (p 'or' q)) 'or'
(the_right_argument_of (p 'or' q)) by ZF_LANG:59;
hence thesis by ZF_LANG:48;
end;
theorem Th6:
the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q
proof p => q is conditional by ZF_LANG:22;
then p => q = (the_antecedent_of (p => q)) =>
(the_consequent_of (p => q)) by ZF_LANG:65;
hence thesis by ZF_LANG:49;
end;
theorem
the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q
proof p <=> q is biconditional by ZF_LANG:22;
then p <=> q = (the_left_side_of (p <=> q)) <=>
(the_right_side_of (p <=> q)) by ZF_LANG:67;
hence thesis by ZF_LANG:50;
end;
theorem
Th8: bound_in All(x,p) = x & the_scope_of All(x,p) = p
proof All(x,p) is universal by ZF_LANG:16;
then All(x,p) = All(bound_in All(x,p), the_scope_of All(x,p)) by ZF_LANG:62
;
hence thesis by ZF_LANG:12;
end;
theorem
Th9: bound_in Ex(x,p) = x & the_scope_of Ex(x,p) = p
proof Ex(x,p) is existential by ZF_LANG:22;
then Ex(x,p) = Ex(bound_in Ex(x,p), the_scope_of Ex(x,p)) by ZF_LANG:63;
hence thesis by ZF_LANG:51;
end;
theorem
Th10: p 'or' q = 'not' p => q
proof
thus p 'or' q = 'not'('not' p '&' 'not' q) by ZF_LANG:def 16 .= 'not'
p => q by ZF_LANG:def 17;
end;
theorem
All(x,y,p) = All(z,q) implies x = z & All(y,p) = q
proof All(x,y,p) = All(x,All(y,p)) by ZF_LANG:23;
hence thesis by ZF_LANG:12;
end;
theorem
Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q
proof Ex(x,y,p) = Ex(x,Ex(y,p)) by ZF_LANG:23;
hence thesis by ZF_LANG:51;
end;
theorem
All(x,y,p) is universal &
bound_in All(x,y,p) = x & the_scope_of All(x,y,p) = All(y,p)
proof All(x,y,p) = All(x,All(y,p)) by ZF_LANG:23;
hence thesis by Th8,ZF_LANG:16;
end;
theorem
Ex(x,y,p) is existential &
bound_in Ex(x,y,p) = x & the_scope_of Ex(x,y,p) = Ex(y,p)
proof Ex(x,y,p) = Ex(x,Ex(y,p)) by ZF_LANG:23;
hence thesis by Th9,ZF_LANG:22;
end;
theorem Th15:
All(x,y,z,p) = All(x,All(y,All(z,p))) & All(x,y,z,p) = All(x,y,All(z,p))
proof
All(y,z,p) = All(y,All(z,p)) & All(x,y,z,p) = All(x,All(y,z,p)) &
All(x,y,All(z,p)) = All(x,All(y,All(z,p))) by ZF_LANG:23,24;
hence thesis;
end;
theorem
Th16: 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);
All(x1,y1,p1) = All(x1,All(y1,p1)) & All(x2,y2,p2) = All(x2,All(y2,p2))
by ZF_LANG:23;
then x1 = x2 & All(y1,p1) = All(y2,p2) by A1,ZF_LANG:12;
hence thesis by ZF_LANG:12;
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);
All(x1,y1,z1,p1) = All(x1,All(y1,z1,p1)) &
All(x2,y2,z2,p2) = All(x2,All(y2,z2,p2)) by ZF_LANG:24;
then x1 = x2 & All(y1,z1,p1) = All(y2,z2,p2) by A1,ZF_LANG:12;
hence thesis by Th16;
end;
theorem
All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q
proof All(x,y,z,p) = All(x,All(y,z,p)) by ZF_LANG:24;
hence thesis by ZF_LANG:12;
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)) by Th15;
hence thesis by Th16;
end;
theorem
Th20: 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);
Ex(x1,y1,p1) = Ex(x1,Ex(y1,p1)) & Ex(x2,y2,p2) = Ex(x2,Ex(y2,p2))
by ZF_LANG:23;
then x1 = x2 & Ex(y1,p1) = Ex(y2,p2) by A1,ZF_LANG:51;
hence thesis by ZF_LANG:51;
end;
theorem
Th21: Ex(x,y,z,p) = Ex(x,Ex(y,Ex(z,p))) & Ex(x,y,z,p) = Ex(x,y,Ex(z,p))
proof
Ex(y,z,p) = Ex(y,Ex(z,p)) & Ex(x,y,z,p) = Ex(x,Ex(y,z,p)) &
Ex(x,y,Ex(z,p)) = Ex(x,Ex(y,Ex(z,p))) by ZF_LANG:23,24;
hence thesis;
end;
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);
Ex(x1,y1,z1,p1) = Ex(x1,Ex(y1,z1,p1)) &
Ex(x2,y2,z2,p2) = Ex(x2,Ex(y2,z2,p2)) by ZF_LANG:24;
then x1 = x2 & Ex(y1,z1,p1) = Ex(y2,z2,p2) by A1,ZF_LANG:51;
hence thesis by Th20;
end;
theorem
Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q
proof Ex(x,y,z,p) = Ex(x,Ex(y,z,p)) by ZF_LANG:24;
hence thesis by ZF_LANG:51;
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)) by Th21;
hence thesis by Th20;
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)
proof All(x,y,z,p) = All(x,All(y,z,p)) by ZF_LANG:24;
hence thesis by Th8,ZF_LANG:16;
end;
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)
proof Ex(x,y,z,p) = Ex(x,Ex(y,z,p)) by ZF_LANG:24;
hence thesis by Th9,ZF_LANG:22;
end;
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:59;
then H = 'not'('not'(the_left_argument_of H) '&' 'not'(
the_right_argument_of H))
by ZF_LANG:def 16;
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:59;
then H = 'not'('not'(the_left_argument_of H) '&' 'not'(
the_right_argument_of H))
by ZF_LANG:def 16;
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:65;
then H = 'not'((the_antecedent_of H) '&' 'not'(the_consequent_of H))
by ZF_LANG:def 17;
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:65;
then H = 'not'((the_antecedent_of H) '&' 'not'(the_consequent_of H))
by ZF_LANG:def 17;
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:67;
then H = ((the_left_side_of H) => (the_right_side_of H)) '&'
((the_right_side_of H) => (the_left_side_of H)) by ZF_LANG:def 18;
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:67;
then H = ((the_left_side_of H) => (the_right_side_of H)) '&'
((the_right_side_of H) => (the_left_side_of H)) by ZF_LANG:def 18;
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:63;
then H = 'not' All(bound_in H, 'not' the_scope_of H) by ZF_LANG:def 19;
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 F 'or' G = 'not'('not' F '&' 'not' G) by ZF_LANG:def 16;
hence the_argument_of F 'or' G = 'not' F '&' 'not' G by Th3;
F 'or' G = 'not' F => G by Th10;
hence thesis by Th6;
end;
theorem
the_argument_of F => G = F '&' 'not' G
proof F => G = 'not'(F '&' 'not' G) by ZF_LANG:def 17;
hence thesis by Th3;
end;
theorem
the_left_argument_of F <=> G = F => G &
the_right_argument_of F <=> G = G => F
proof F <=> G = (F => G) '&' (G => F) by ZF_LANG:def 18;
hence thesis by Th4;
end;
theorem
the_argument_of Ex(x,H) = All(x,'not' H)
proof Ex(x,H) = 'not' All(x,'not' H) by ZF_LANG:def 19;
hence thesis by Th3;
end;
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 H = (the_left_argument_of H) 'or' (the_right_argument_of H)
by ZF_LANG:59;
then A1: H = 'not'('not'(the_left_argument_of H) '&' 'not'
(the_right_argument_of H)) &
H = 'not'(the_left_argument_of H) => (the_right_argument_of H)
by Th10,ZF_LANG:def 16;
hence H is conditional & H is negative by ZF_LANG:16,22;
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 by ZF_LANG:16;
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 by ZF_LANG:16;
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 H = (the_antecedent_of H) => (the_consequent_of H)
by ZF_LANG:65;
then A1: H = 'not'((the_antecedent_of H) '&' 'not'(the_consequent_of H))
by ZF_LANG:def 17;
hence H is negative by ZF_LANG:16;
A2: the_argument_of H = (the_antecedent_of H) '&' 'not'(the_consequent_of H)
by A1,Th3;
hence the_argument_of H is conjunctive by ZF_LANG:16;
the_right_argument_of the_argument_of H = 'not'
(the_consequent_of H) by A2,Th4;
hence thesis by ZF_LANG:16;
end;
theorem
H is biconditional implies
H is conjunctive & the_left_argument_of H is conditional &
the_right_argument_of H is conditional
proof assume H is biconditional;
then H = (the_left_side_of H) <=> (the_right_side_of H)
by ZF_LANG:67;
then A1: H = ((the_left_side_of H) => (the_right_side_of H)) '&'
((the_right_side_of H) => (the_left_side_of H)) by ZF_LANG:def 18;
hence H is conjunctive by ZF_LANG:16;
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 A1,Th4;
hence thesis by ZF_LANG:22;
end;
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 H = Ex(bound_in H, the_scope_of H) by ZF_LANG:63;
then A1: H = 'not' All(bound_in H, 'not' the_scope_of H) by ZF_LANG:def 19;
hence H is negative by ZF_LANG:16;
A2: the_argument_of H = All(bound_in H, 'not' the_scope_of H) by A1,Th3;
hence the_argument_of H is universal by ZF_LANG:16;
'not' the_scope_of H = the_scope_of the_argument_of H by A2,Th8;
hence thesis by ZF_LANG:16;
end;
theorem
not (H is_equality & (H is_membership or H is negative or
H is conjunctive or H is universal)) &
not (H is_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:40;
hence thesis by ZF_LANG:35,36,37,38,39;
end;
theorem
Th43: F is_subformula_of G implies len F <= len G
proof assume F is_subformula_of G;
then F is_proper_subformula_of G or F = G by ZF_LANG:def 41;
hence thesis by ZF_LANG:83;
end;
theorem Th44:
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: now assume F is_proper_subformula_of G;
then A2: F is_subformula_of G & len F < len G by ZF_LANG:83,def 41;
assume G is_subformula_of H;
then F is_subformula_of H & len G <= len H by A2,Th43,ZF_LANG:86;
hence F is_proper_subformula_of H by A2,ZF_LANG:def 41;
end;
A3: now assume
A4: F is_subformula_of G & G is_proper_subformula_of H;
then G is_subformula_of H & len F <= len G & len G < len H
by Th43,ZF_LANG:83,def 41;
then F is_subformula_of H & len F < len H by A4,AXIOMS:22,ZF_LANG:86;
hence thesis by ZF_LANG:def 41;
end;
(G is_immediate_constituent_of H implies G is_proper_subformula_of H) &
(F is_immediate_constituent_of G implies F is_proper_subformula_of G)
by ZF_LANG:82;
hence thesis by A1,A3,ZF_LANG:85;
end;
canceled;
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:82;
hence contradiction by ZF_LANG:def 41;
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 Th44;
hence contradiction by ZF_LANG:def 41;
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:85;
hence contradiction by ZF_LANG:def 41;
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 Th44;
hence contradiction by ZF_LANG:def 41;
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 Th44;
hence contradiction by ZF_LANG:def 41;
end;
theorem
'not' F is_subformula_of H implies F is_proper_subformula_of H
proof F is_immediate_constituent_of 'not' F by ZF_LANG:def 39;
hence thesis by Th44;
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 by ZF_LANG:def 39;
hence thesis by Th44;
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) by ZF_LANG:def 39;
hence thesis by Th44;
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 => G = 'not'(F '&' 'not' G) by ZF_LANG:def 17;
then F '&' 'not' G is_immediate_constituent_of F => G by ZF_LANG:def 39;
hence
A1: F '&' 'not' G is_proper_subformula_of F => G by ZF_LANG:82;
F is_immediate_constituent_of F '&' 'not' G &
'not' G is_immediate_constituent_of F '&' 'not' G by ZF_LANG:def 39;
hence
A2: F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G
by A1,Th44;
G is_immediate_constituent_of 'not' G by ZF_LANG:def 39;
hence thesis by A2,Th44;
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 F 'or' G = 'not'('not' F '&' 'not' G) by ZF_LANG:def 16;
then 'not' F '&' 'not' G is_immediate_constituent_of F 'or' G by ZF_LANG:
def 39;
hence
A1: 'not' F '&' 'not' G is_proper_subformula_of F 'or' G by ZF_LANG:82;
'not' F is_immediate_constituent_of 'not' F '&' 'not' G &
'not' G is_immediate_constituent_of 'not' F '&' 'not' G by ZF_LANG:def 39;
hence
A2: 'not' F is_proper_subformula_of F 'or' G &
'not' G is_proper_subformula_of F 'or' G by A1,Th44;
F is_immediate_constituent_of 'not' F &
G is_immediate_constituent_of 'not' G by ZF_LANG:def 39;
hence thesis by A2,Th44;
end;
theorem
All(x,'not' H) is_proper_subformula_of Ex(x,H) &
'not' H is_proper_subformula_of Ex(x,H)
proof Ex(x,H) = 'not' All(x,'not' H) by ZF_LANG:def 19;
then All(x,'not' H) is_immediate_constituent_of Ex(x,H) by ZF_LANG:def 39;
hence
A1: All(x,'not' H) is_proper_subformula_of Ex(x,H) by ZF_LANG:82;
'not' H is_immediate_constituent_of All(x,'not' H) by ZF_LANG:def 39;
hence thesis by A1,Th44;
end;
theorem
G is_subformula_of H iff G in Subformulae H by ZF_LANG:100,def 42;
theorem
G in Subformulae H implies Subformulae G c= Subformulae H
proof assume G in Subformulae H;
then G is_subformula_of H by ZF_LANG:100;
hence thesis by ZF_LANG:101;
end;
theorem
H in Subformulae H
proof
H is_subformula_of H by ZF_LANG:79;
hence thesis by ZF_LANG:def 42;
end;
theorem Th60:
Subformulae (F => G) =
Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
proof F => G = 'not'(F '&' 'not' G) by ZF_LANG:def 17;
hence Subformulae (F => G)
= Subformulae (F '&' 'not' G) \/ { F => G } by ZF_LANG:104
.= Subformulae F \/ Subformulae 'not' G \/ {F '&' 'not' G} \/ {F => G}
by ZF_LANG:105
.= Subformulae F \/ (Subformulae G \/ {'not' G}) \/ {F '&' 'not'
G} \/ { F => G }
by ZF_LANG:104
.= 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:41
.= Subformulae F \/ Subformulae G \/ { 'not' G,F '&' 'not' G,F => G }
by ENUMSET1:42;
end;
theorem
Subformulae (F 'or' G) =
Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&' 'not'
G, F 'or' G}
proof F 'or' G = 'not'('not' F '&' 'not' G) by ZF_LANG:def 16;
hence Subformulae (F 'or' G)
= Subformulae ('not' F '&' 'not' G) \/ { F 'or' G } by ZF_LANG:104
.= Subformulae 'not' F \/ Subformulae 'not' G \/ {'not' F '&' 'not'
G} \/ {F 'or' G}
by ZF_LANG:105
.= Subformulae 'not' F \/ (Subformulae G \/ {'not' G}) \/
{'not' F '&' 'not' G} \/ {F 'or' G}
by ZF_LANG:104
.= Subformulae F \/ {'not' F} \/ (Subformulae G \/ {'not' G}) \/
{'not' F '&' 'not' G} \/ {F 'or' G} by ZF_LANG:104
.= 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:41
.= 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:41
.= 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:45;
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
F <=> G = (F => G) '&' (G => F) by ZF_LANG:def 18;
hence Subformulae (F <=> G)
= Subformulae(F => G) \/ Subformulae(G => F) \/ {F <=> G}
by ZF_LANG:105
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
\/
Subformulae(G => F) \/ {F <=> G} by Th60
.= 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 Th60
.= 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:53
.= 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:61;
end;
theorem
Th63: Free (x '=' y) = {x,y}
proof
x '=' y is_equality & Var1 (x '=' y) = x & Var2 (x '=' y) = y
by Th1,ZF_LANG:16;
hence thesis by ZF_MODEL:1;
end;
theorem
Th64: Free (x 'in' y) = {x,y}
proof
x 'in' y is_membership & Var1 (x 'in' y) = x & Var2 (x 'in' y) = y
by Th2,ZF_LANG:16;
hence thesis by ZF_MODEL:1;
end;
theorem
Th65: Free ('not' p) = Free p
proof 'not' p is negative & the_argument_of 'not' p = p by Th3,ZF_LANG:16;
hence thesis by ZF_MODEL:1;
end;
theorem
Th66: Free (p '&' q) = Free p \/ Free q
proof
p '&' q is conjunctive & the_left_argument_of (p '&' q) = p &
the_right_argument_of (p '&' q) = q by Th4,ZF_LANG:16;
hence thesis by ZF_MODEL:1;
end;
theorem
Th67: Free All(x,p) = Free p \ {x}
proof
All(x,p) is universal & bound_in All(x,p) = x &
the_scope_of All(x,p) = p by Th8,ZF_LANG:16;
hence thesis by ZF_MODEL:1;
end;
theorem
Free (p 'or' q) = Free p \/ Free q
proof p 'or' q = 'not'('not' p '&' 'not' q) by ZF_LANG:def 16;
hence Free (p 'or' q) = Free ('not' p '&' 'not' q) by Th65
.= Free 'not' p \/ Free 'not' q by Th66
.= Free p \/ Free 'not' q by Th65
.= Free p \/ Free q by Th65;
end;
theorem
Th69: Free (p => q) = Free p \/ Free q
proof p => q = 'not'(p '&' 'not' q) by ZF_LANG:def 17;
hence Free (p => q) = Free (p '&' 'not' q) by Th65
.= Free p \/ Free 'not' q by Th66
.= Free p \/ Free q by Th65;
end;
theorem
Free (p <=> q) = Free p \/ Free q
proof p <=> q = (p => q) '&' (q => p) by ZF_LANG:def 18;
hence Free (p <=> q) = Free (p => q) \/ Free (q => p) by Th66
.= Free p \/ Free q \/ Free (q => p) by Th69
.= Free p \/ Free q \/ (Free q \/ Free p) by Th69
.= 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
Th71: Free Ex(x,p) = Free p \ {x}
proof Ex(x,p) = 'not' All(x,'not' p) by ZF_LANG:def 19;
hence Free Ex(x,p) = Free All(x,'not' p) by Th65
.= Free 'not' p \ {x} by Th67
.= Free p \ {x} by Th65;
end;
theorem
Th72: Free All(x,y,p) = Free p \ {x,y}
proof
thus Free All(x,y,p) = Free All(x,All(y,p)) by ZF_LANG:23
.= Free All(y,p) \ {x} by Th67
.= (Free p \ {y}) \ {x} by Th67
.= Free p \ ({x} \/ {y}) by XBOOLE_1:41
.= Free p \ {x,y} by ENUMSET1:41;
end;
theorem
Free All(x,y,z,p) = Free p \ {x,y,z}
proof
thus Free All(x,y,z,p) = Free All(x,All(y,z,p)) by ZF_LANG:24
.= Free All(y,z,p) \ {x} by Th67
.= (Free p \ {y,z}) \ {x} by Th72
.= Free p \ ({x} \/ {y,z}) by XBOOLE_1:41
.= Free p \ {x,y,z} by ENUMSET1:42;
end;
theorem
Th74: Free Ex(x,y,p) = Free p \ {x,y}
proof
thus Free Ex(x,y,p) = Free Ex(x,Ex(y,p)) by ZF_LANG:23
.= Free Ex(y,p) \ {x} by Th71
.= (Free p \ {y}) \ {x} by Th71
.= Free p \ ({x} \/ {y}) by XBOOLE_1:41
.= Free p \ {x,y} by ENUMSET1:41;
end;
theorem
Free Ex(x,y,z,p) = Free p \ {x,y,z}
proof
thus Free Ex(x,y,z,p) = Free Ex(x,Ex(y,z,p)) by ZF_LANG:24
.= Free Ex(y,z,p) \ {x} by Th71
.= (Free p \ {y,z}) \ {x} by Th74
.= Free p \ ({x} \/ {y,z}) by XBOOLE_1:41
.= Free p \ {x,y,z} by ENUMSET1:42;
end;
scheme ZF_Induction { 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
defpred p[ZF-formula] means P[$1];
A5: for H st H is atomic holds p[H]
proof let H such that
A6: H is_equality or H is_membership;
A7: H is_equality implies thesis
proof given x1,x2 such that
A8: H = x1 '=' x2;
thus thesis by A1,A8;
end;
H is_membership implies thesis
proof given x1,x2 such that
A9: H = x1 'in' x2;
thus thesis by A1,A9;
end;
hence thesis by A6,A7;
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;
A11: 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:58;
hence thesis by A3;
end;
A12: 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:62;
hence thesis by A4;
end;
thus for H holds p[H] from ZF_Ind(A5,A10,A11,A12);
end;
reserve M,E for non empty set,
e for Element of E,
m,m' for Element of M,
f,g for Function of VAR,E,
v,v' for Function of VAR,M;
definition let E,f,x,e;
func f / (x,e) -> Function of VAR,E means:
Def1: it.x = e & for y st it.y <> f.y holds x = y;
existence
proof consider g such that
A1: g.x = e & for y st y <> x holds g.y = f.y by ZF_MODEL:21;
take g; thus thesis by A1;
end;
uniqueness
proof let g1,g2 be Function of VAR,E such that
A2: g1.x = e & for y st g1.y <> f.y holds x = y and
A3: g2.x = e & for y st g2.y <> f.y holds x = y;
now let y be Element of VAR;
g1.y = e & g2.y = e or g1.y = f.y & g2.y = f.y by A2,A3;
hence g1.y = g2.y;
end;
hence thesis by FUNCT_2:113;
end;
end;
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 RELSET_1:12;
then rng f c= D2 & dom f = D by A1,FUNCT_2:def 1,XBOOLE_1:1;
hence thesis by FUNCT_2:def 1,RELSET_1:11;
end;
end;
canceled 2;
theorem
Th78: (v/(x,m'))/(x,m) = v/(x,m) & v/(x,v.x) = v
proof
now let y; assume x <> y;
then (v/(x,m'))/(x,m).y = v/(x,m').y & v/(x,m').y = v.y by Def1;
hence (v/(x,m'))/(x,m).y = v.y;
end;
then A1: for y st (v/(x,m'))/(x,m).y <> v.y holds x = y;
(v/(x,m'))/(x,m).x = m by Def1;
hence (v/(x,m'))/(x,m) = v/(x,m) by A1,Def1;
v.x = v.x & for y st v.y <> v.y holds x = y;
hence v/(x,v.x) = v by Def1;
end;
theorem
x <> y implies (v/(x,m))/(y,m') = (v/(y,m'))/(x,m)
proof assume
x <> y;
then A1: (v/(x,m))/(y,m').x = v/(x,m).x by Def1 .= m by Def1;
now let z such that
A2: (v/(x,m))/(y,m').z <> v/(y,m').z;
z = y or z <> y;
then (v/(x,m))/(y,m').z = m' & v/(y,m').z = m' or
(v/(x,m))/(y,m').z = v/(x,m).z & v/(y,m').z = v.z by Def1;
hence x = z by A2,Def1;
end;
hence thesis by A1,Def1;
end;
theorem
Th80: 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 Def1;
hence thesis by A1,ZF_MODEL:16;
end;
assume
A2: for m holds M,v/(x,m) |= H;
now let v'; assume for y st v'.y <> v.y holds x = y;
then v' = v/(x,v'.x) by Def1;
hence M,v' |= H by A2;
end;
hence thesis by ZF_MODEL:16;
end;
theorem
Th81: M,v |= All(x,H) iff M,v/(x,m) |= All(x,H)
proof
A1: (v/(x,m))/(x,v.x) = v/(x,v.x) by Th78 .= v by Th78;
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 m'; (v/(x,m))/(x,m') = v/(x,m') by Th78;
hence M,(v/(x,m))/(x,m') |= H by A2,Th80;
end;
hence thesis by Th80;
end;
hence thesis by A1;
end;
theorem
Th82: 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 v' such that
A1: (for y st v'.y <> v.y holds x = y) & M,v' |= H by ZF_MODEL:20;
take v'.x;
thus thesis by A1,Def1;
end;
given m such that
A2: M,v/(x,m) |= H;
now take v' = v/(x,m);
thus for y st v'.y <> v.y holds x = y by Def1;
thus M,v' |= 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: (v/(x,m))/(x,v.x) = v/(x,v.x) by Th78 .= v by Th78;
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 m' such that
A2: M,v/(x,m') |= H by Th82;
(v/(x,m))/(x,m') = v/(x,m') by Th78;
hence thesis by A2,Th82;
end;
hence thesis by A1;
end;
theorem
for v,v' st for x st x in Free H holds v'.x = v.x holds
M,v |= H implies M,v' |= H
proof
defpred Etha[ZF-formula] means
for v,v' st for x st x in Free $1 holds v'.x = v.x holds
M,v |= $1 implies M,v' |= $1;
A1: for x1,x2 holds Etha[x1 '=' x2] & Etha[x1 'in' x2]
proof let x1,x2;
A2: Free (x1 '=' x2) = {x1,x2} & Free (x1 'in' x2) = {x1,x2} by Th63,Th64;
thus Etha[x1 '=' x2]
proof let v,v'; assume
A3: for x st x in Free (x1 '=' x2) holds v'.x = v.x;
assume M,v |= x1 '=' x2;
then A4: v.x1 = v.x2 by ZF_MODEL:12;
x1 in Free (x1 '=' x2) & x2 in Free (x1 '=' x2)
by A2,TARSKI:def 2;
then v'.x1 = v.x1 & v'.x2 = v.x2 by A3;
hence thesis by A4,ZF_MODEL:12;
end;
let v,v'; assume
A5: for x st x in Free (x1 'in' x2) holds v'.x = v.x;
assume M,v |= x1 'in' x2;
then A6: v.x1 in v.x2 by ZF_MODEL:13;
x1 in Free (x1 'in' x2) & x2 in Free (x1 'in' x2)
by A2,TARSKI:def 2;
then v'.x1 = v.x1 & v'.x2 = v.x2 by A5;
hence thesis by A6,ZF_MODEL:13;
end;
A7: for H st Etha[H] holds Etha['not' H]
proof let H such that
A8: Etha[H];
let v,v'; assume
A9: for x st x in Free 'not' H holds v'.x = v.x;
assume M,v |= 'not' H;
then A10: not M,v |= H by ZF_MODEL:14;
now let x; assume x in Free H;
then x in Free 'not' H by Th65;
hence v.x = v'.x by A9;
end;
then not M,v' |= H by A8,A10;
hence M,v' |= 'not' H by ZF_MODEL:14;
end;
A11: for H1,H2 st Etha[H1] & Etha[H2] holds Etha[H1 '&' H2]
proof let H1,H2 such that
A12: Etha[H1] & Etha[H2];
A13: Free (H1 '&' H2) = Free H1 \/ Free H2 by Th66;
let v,v'; assume
A14: for x st x in Free H1 '&' H2 holds v'.x = v.x;
assume M,v |= H1 '&' H2;
then A15: M,v |= H1 & M,v |= H2 by ZF_MODEL:15;
now let x; assume x in Free H1;
then x in Free (H1 '&' H2) by A13,XBOOLE_0:def 2;
hence v'.x = v.x by A14;
end;
then A16: M,v' |= H1 by A12,A15;
now let x; assume x in Free H2;
then x in Free (H1 '&' H2) by A13,XBOOLE_0:def 2;
hence v'.x = v.x by A14;
end;
then M,v' |= H2 by A12,A15;
hence thesis by A16,ZF_MODEL:15;
end;
A17: for H,x st Etha[H] holds Etha[All(x,H)]
proof let H,x1 such that
A18: Etha[H];
let v,v';
assume that
A19: for x st x in Free All(x1,H) holds v'.x = v.x and
A20: M,v |= All(x1,H);
now let m;
A21: M,v/(x1,m) |= H & Free All(x1,H) = Free H \ {x1} by A20,Th67,Th80;
now let x; assume
x in Free H;
then x in Free All(x1,H) & not x in {x1} or x in {x1}
by A21,XBOOLE_0:def 4;
then v'.x = v.x & x <> x1 or x = x1 by A19,TARSKI:def 1;
then v'/(x1,m).x = v.x & v.x = v/(x1,m).x or
v/(x1,m).x = m & v'/(x1,m).x = m by Def1;
hence v'/(x1,m).x = v/(x1,m).x;
end;
hence M,v'/(x1,m) |= H by A18,A21;
end;
hence thesis by Th80;
end;
for H holds Etha[H] from ZF_Induction(A1,A7,A11,A17);
hence thesis;
end;
theorem Th85:
Free H is finite
proof
defpred P[ZF-formula] means Free $1 is finite;
A1: P[x '=' y] & P[x 'in' y]
proof Free (x '=' y) = {x,y} & Free (x 'in' y) = {x,y} by Th63,Th64;
hence thesis;
end;
A2: P[p] implies P['not' p] by Th65;
A3: P[p] & P[q] implies P[p '&' q]
proof Free p '&' q = Free p \/ Free q by Th66;
hence thesis by FINSET_1:14;
end;
A4: P[p] implies P[All(x,p)]
proof Free All(x,p) = Free p \ {x} by Th67;
hence thesis by FINSET_1:16;
end;
P[p] from ZF_Induction(A1,A2,A3,A4);
hence thesis;
end;
definition let H;
cluster Free H -> finite;
coherence by Th85;
end;
reserve i,j for Nat;
theorem
x.i = x.j implies i = j
proof x.i = 5+i & x.j = 5+j by ZF_LANG:def 2;
hence thesis by XCMPLX_1:2;
end;
theorem
ex i st x = x.i
proof x in VAR;
then consider j such that
A1: x = j & 5 <= j by ZF_LANG:def 1;
consider i such that
A2: j = 5+i by A1,NAT_1:28;
take i; thus thesis by A1,A2,ZF_LANG:def 2;
end;
canceled;
theorem
Th89: M,v |= x '=' x
proof v.x = v.x;
hence thesis by ZF_MODEL:12;
end;
theorem
Th90: M |= x '=' x
proof
M,v |= x '=' x by Th89;
hence thesis by ZF_MODEL:def 5;
end;
theorem
Th91: not M,v |= x 'in' x
proof not v.x in v.x;
hence thesis by ZF_MODEL:13;
end;
theorem
Th92: not M |= x 'in' x & M |= 'not' x 'in' x
proof consider v;
not M,v |= x 'in' x by Th91;
hence not M |= x 'in' x by ZF_MODEL:def 5;
let v;
not M,v |= x 'in' x by Th91;
hence M,v |= 'not' x 'in' x 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 assume
A1: (for v holds M,v |= x '=' y) & x <> y;
consider m; reconsider a = m as set;
take a;
thus {a} c= M by ZFMISC_1:37;
let b be set; assume
A2: b in M & not b in {a};
then reconsider b as Element of M;
consider v;
M,(v/(x,m))/(y,b) |= x '=' y by A1;
then (v/(x,m))/(y,b).x = (v/(x,m))/(y,b).y & v/(x,m).x = m &
(v/(x,m))/(y,b).y = b & (v/(x,m))/(y,b).x = v/(x,m).x
by A1,Def1,ZF_MODEL:12;
hence contradiction by A2,TARSKI:def 1;
end;
now given a such that
A3: {a} = M;
let v;
v.x = a & v.y = a by A3,TARSKI:def 1;
hence M,v |= x '=' y by ZF_MODEL:12;
end;
hence thesis by Th90,ZF_MODEL:def 5;
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 assume
A1: (for v holds M,v |= 'not' x 'in' y) & x <> y;
let X; assume X in M;
then reconsider m = X as Element of M;
assume
A2: X /\ M <> {};
consider a being Element of X /\ M;
reconsider a as Element of M by A2,XBOOLE_0:def 3;
consider v;
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 not (v/(x,a))/(y,m).x in (v/(x,a))/(y,m).y & v/(x,a).x = a &
(v/(x,a))/(y,m).y = m & (v/(x,a))/(y,m).x = v/(x,a).x
by A1,Def1,ZF_MODEL:13;
hence contradiction by A2,XBOOLE_0:def 3;
end;
now assume
A3: for X st X in M holds X misses M;
let v;
v.y misses M by A3;
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 Th92,ZF_MODEL:def 5;
end;
theorem
H is_equality implies (M,v |= H iff v.Var1 H = v.Var2 H)
proof assume H is_equality;
then H = (Var1 H) '=' (Var2 H) by ZF_LANG:53;
hence thesis by ZF_MODEL:12;
end;
theorem
H is_membership implies (M,v |= H iff v.Var1 H in v.Var2 H)
proof assume H is_membership;
then H = (Var1 H) 'in' (Var2 H) by ZF_LANG:54;
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:
58;
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:62;
hence thesis by Th80;
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
:59;
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:65;
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:67;
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:63;
hence thesis by Th82;
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
proof assume
A1: M,v |= Ex(x,H);
let v; M,v |= Ex(x,H) by A1;
hence thesis by Th82;
end;
assume
A2: for v ex m st M,v/(x,m) |= H;
let v; ex m st M,v/(x,m) |= H by A2;
hence thesis by Th82;
end;
theorem
Th105: M |= H implies M |= Ex(x,H)
proof assume
A1: M |= H;
let v;
M,v/(x,v.x) |= H by A1,ZF_MODEL:def 5;
hence M,v |= Ex(x,H) by Th82;
end;
theorem
Th106: M |= H iff M |= All(x,y,H)
proof All(x,y,H) = All(x,All(y,H)) by ZF_LANG:23;
then (M |= H iff M |= All(y,H)) &
(M |= All(y,H) iff M |= All(x,y,H)) by ZF_MODEL:25;
hence thesis;
end;
theorem
Th107: M |= H implies M |= Ex(x,y,H)
proof Ex(x,y,H) = Ex(x,Ex(y,H)) by ZF_LANG:23;
then (M |= H implies M |= Ex(y,H)) &
(M |= Ex(y,H) implies M |= Ex(x,y,H)) by Th105;
hence thesis;
end;
theorem
M |= H iff M |= All(x,y,z,H)
proof All(x,y,z,H) = All(x,All(y,z,H)) by ZF_LANG:24;
then (M |= H iff M |= All(y,z,H)) &
(M |= All(y,z,H) iff M |= All(x,y,z,H)) by Th106,ZF_MODEL:25;
hence thesis;
end;
theorem
M |= H implies M |= Ex(x,y,z,H)
proof Ex(x,y,z,H) = Ex(x,Ex(y,z,H)) by ZF_LANG:24;
then (M |= H implies M |= Ex(y,z,H)) &
(M |= Ex(y,z,H) implies M |= Ex(x,y,z,H)) by Th105,Th107;
hence thesis;
end;
::
:: Axioms of Logic
::
theorem
M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q)
proof
A1: now let v;
now assume M,v |= p <=> q;
then M,v |= (p => q) '&' (q => p) by ZF_LANG:def 18;
hence M,v |= p => q by ZF_MODEL:15;
end;
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;
now assume M,v |= p <=> q;
then M,v |= (p => q) '&' (q => p) by ZF_LANG:def 18;
hence M,v |= q => p by ZF_MODEL:15;
end;
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
Th112: 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 M,v |= (p => q) => ((q => r) => (p => r)) by ZF_MODEL:18;
end;
theorem
Th113: M,v |= p => q & M,v |= q => r implies M,v |= p => r
proof assume
A1: M,v |= p => q & M,v |= q => r;
M |= (p => q) => ((q => r) => (p => r)) by Th112;
then M,v |= (p => q) => ((q => r) => (p => r)) by ZF_MODEL:def 5;
then M,v |= (q => r) => (p => r) by A1,ZF_MODEL:18;
hence M,v |= p => r by A1,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,ZF_MODEL:def 5;
hence M,v |= p => r by Th113;
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 Th113;
end;
hence M,v |= (p => q) '&' (q => r) => (p => r) by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 (M,v |= p implies M,v |= q => r & M,v |= q) &
(M,v |= q & M,v |= q => r implies M,v |= r)
by A1,ZF_MODEL:18;
hence M,v |= p => r by 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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
end;
theorem
M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p
proof
now let v;
(M,v |= p '&' q implies M,v |= p & M,v |= q) &
(M,v |= p & M,v |= q implies M,v |= q '&' p)
by ZF_MODEL:15;
hence M,v |= p '&' q => q '&' p by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
end;
theorem Th123:
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
end;
theorem
M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p
proof
now let v;
(M,v |= p 'or' q implies M,v |= p or M,v |= q) &
(M,v |= p or M,v |= q implies M,v |= q 'or' p)
by ZF_MODEL:17;
hence M,v |= p 'or' q => q 'or' p by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:def 5;
end;
theorem
M,v |= p => p 'or' p & M |= p => p 'or' p by Th123;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
end;
canceled;
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,ZF_MODEL:def 5;
hence M,v |= q 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 by ZF_MODEL:def 5;
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 by ZF_MODEL:def 5;
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 not M,v |= p 'or' q by ZF_MODEL:14;
then not M,v |= p & not M,v |= q by ZF_MODEL:17;
then M,v |= 'not' p & M,v |= 'not' q by ZF_MODEL:14;
hence M,v |= 'not' p '&' 'not' q by ZF_MODEL:15;
end;
hence M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:def 5;
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 M,v |= 'not' p '&' 'not' q;
then M,v |= 'not' p & M,v |= 'not' q by ZF_MODEL:15;
then not M,v |= p & not M,v |= q by ZF_MODEL:14;
then not M,v |= p 'or' q by 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 by ZF_MODEL:def 5;
end;
theorem
M |= All(x,H) => H
proof let v;
M,v |= All(x,H) implies M,v/(x,v.x) |= H by Th80;
then M,v |= All(x,H) implies M,v |= H by Th78;
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 Th82;
then M,v |= H implies M,v |= Ex(x,H) by Th78;
hence thesis by ZF_MODEL:18;
end;
theorem
Th140: 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 M,v/(x,m) |= H1 & M,v/(x,m) |= H1 => H2 by A2,Th80;
hence M,v/(x,m) |= H2 by ZF_MODEL:18;
end;
hence M,v |= All(x,H2) by Th80;
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
A1: not x in Free H1 & for v holds M,v |= H1 => H2;
let v;
(for m holds M,v/(x,m) |= H1 => H2) &
M |= All(x,H1 => H2) => (H1 => All(x,H2)) by A1,Th140;
then M,v |= All(x,H1 => H2) => (H1 => All(x,H2)) & M,v |= All(x,H1 => H2)
by Th80,ZF_MODEL:def 5;
hence M,v |= H1 => All(x,H2) by ZF_MODEL:18;
end;
theorem
Th142: 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 Th82;
M,v/(x,m) |= H1 => H2 by A2,Th80;
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 Th81;
then M,v/(x,v.x) |= H2 by Th80;
hence M,v |= H2 by Th78;
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
A1: not x in Free H2 & for v holds M,v |= H1 => H2;
let v;
(for m holds M,v/(x,m) |= H1 => H2) &
M |= All(x,H1 => H2) => (Ex(x,H1) => H2) by A1,Th142;
then M,v |= All(x,H1 => H2) => (Ex(x,H1) => H2) & M,v |= All(x,H1 => H2)
by Th80,ZF_MODEL:def 5;
hence M,v |= Ex(x,H1) => H2 by 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 Th80;
hence M,v |= H2 by Th78;
end;
hence M,v |= H1 => H2 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 Th78;
then M,v |= Ex(x,H1) by Th82;
hence M,v |= H2 by A2,ZF_MODEL:18;
end;
hence M,v |= H1 => H2 by ZF_MODEL:18;
end;
theorem
WFF c= bool [:NAT,NAT:]
proof let a; assume a in WFF;
then reconsider H = a as ZF-formula by ZF_LANG:14;
H c= [:NAT,NAT:] & H = H;
hence thesis;
end;
::
:: Variables in ZF-formula
::
definition let H;
func variables_in H -> set equals:
Def3: rng H \ { 0,1,2,3,4 };
correctness;
end;
canceled;
theorem
Th148: x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4
proof assume
A1: x = 0 or x = 1 or x = 2 or x = 3 or x = 4;
x in VAR;
then ex i st x = i & 5 <= i by ZF_LANG:def 1;
hence contradiction by A1;
end;
theorem
Th149: 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:48;
then x in { 0,1 } or x in { 2,3,4 } by XBOOLE_0:def 2;
then A1: x = 0 or x = 1 or x = 2 or x = 3 or x = 4 by ENUMSET1:13,TARSKI:def 2
;
x in VAR;
then ex i st x = i & 5 <= i by ZF_LANG:def 1;
hence contradiction by A1;
end;
theorem
Th150: a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4
proof assume a in variables_in H;
then a in rng H \ {0,1,2,3,4} by Def3;
then not a in {0,1,2,3,4} by XBOOLE_0:def 4;
then not a in {0,1} \/ {2,3,4} by ENUMSET1:48;
then not a in {0,1} & not a in {2,3,4} by XBOOLE_0:def 2;
hence a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 by ENUMSET1:14,TARSKI:def 2
;
end;
theorem
Th151: variables_in x '=' y = {x,y}
proof x '=' y = <*0*>^<*x*>^<*y*> by ZF_LANG:def 3;
then rng (x '=' y) = rng (<*0*>^<*x*>) \/ rng <*y*> by FINSEQ_1:44
.= rng <*0*> \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:44
.= {0} \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:56
.= {0} \/ {x} \/ rng <*y*> by FINSEQ_1:56
.= {0} \/ {x} \/ {y} by FINSEQ_1:56
.= {0} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {0} \/ {x,y} by ENUMSET1:41;
then A1: variables_in (x '=' y) = ({0} \/ {x,y}) \ {0,1,2,3,4} by Def3;
thus variables_in (x '=' y) c= {x,y}
proof let a; assume a in variables_in x '=' y;
then A2: a in {0} \/ {x,y} & a <> 0 by A1,Th150,XBOOLE_0:def 4;
then not a in {0} by TARSKI:def 1;
hence a in {x,y} by A2,XBOOLE_0:def 2;
end;
let a; assume a in {x,y};
then A3: a in {0} \/ {x,y} & (a = x or a = y) by TARSKI:def 2,XBOOLE_0:def 2;
then not a in {0,1,2,3,4} by Th149;
hence thesis by A1,A3,XBOOLE_0:def 4;
end;
theorem
Th152: variables_in x 'in' y = {x,y}
proof x 'in' y = <*1*>^<*x*>^<*y*> by ZF_LANG:def 4;
then rng (x 'in' y) = rng (<*1*>^<*x*>) \/ rng <*y*> by FINSEQ_1:44
.= rng <*1*> \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:44
.= {1} \/ rng <*x*> \/ rng <*y*> by FINSEQ_1:56
.= {1} \/ {x} \/ rng <*y*> by FINSEQ_1:56
.= {1} \/ {x} \/ {y} by FINSEQ_1:56
.= {1} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {1} \/ {x,y} by ENUMSET1:41;
then A1: variables_in (x 'in' y) = ({1} \/ {x,y}) \ {0,1,2,3,4} by Def3;
thus variables_in (x 'in' y) c= {x,y}
proof let a; assume a in variables_in x 'in' y;
then A2: a in {1} \/ {x,y} & a <> 1 by A1,Th150,XBOOLE_0:def 4;
then not a in {1} by TARSKI:def 1;
hence a in {x,y} by A2,XBOOLE_0:def 2;
end;
let a; assume a in {x,y};
then A3: a in {1} \/ {x,y} & (a = x or a = y) by TARSKI:def 2,XBOOLE_0:def 2;
then not a in {0,1,2,3,4} by Th149;
hence thesis by A1,A3,XBOOLE_0:def 4;
end;
theorem
Th153: variables_in 'not' H = variables_in H
proof 'not' H = <*2*>^H by ZF_LANG:def 5;
then rng 'not' H = rng <*2*> \/ rng H by FINSEQ_1:44
.= {2} \/ rng H by FINSEQ_1:56;
then A1: variables_in 'not' H = ({2} \/ rng H) \ {0,1,2,3,4} &
variables_in H = rng H \ {0,1,2,3,4} by Def3;
thus variables_in 'not' H c= variables_in H
proof let a; assume a in variables_in 'not' H;
then A2: a in {2} \/ rng H & not a in
{0,1,2,3,4} & a <> 2 by A1,Th150,XBOOLE_0:def 4
;
then not a in {2} by TARSKI:def 1;
then a in rng H by A2,XBOOLE_0:def 2;
hence a in variables_in H by A1,A2,XBOOLE_0:def 4;
end;
rng H c= {2} \/ rng H by XBOOLE_1:7;
hence variables_in H c= variables_in 'not' H by A1,XBOOLE_1:33;
end;
theorem
Th154: variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2
proof H1 '&' H2 = <*3*>^H1^H2 by ZF_LANG:def 6;
then rng H1 '&' H2 = rng (<*3*>^H1) \/ rng H2 by FINSEQ_1:44
.= rng <*3*> \/ rng H1 \/ rng H2 by FINSEQ_1:44
.= {3} \/ rng H1 \/ rng H2 by FINSEQ_1:56
.= {3} \/ (rng H1 \/ rng H2) by XBOOLE_1:4;
then A1: variables_in H1 '&' H2 = ({3} \/ (rng H1 \/ rng H2)) \ {0,1,2,3,4} &
variables_in H1 = rng H1 \ {0,1,2,3,4} &
variables_in H2 = rng H2 \ {0,1,2,3,4} by Def3;
then A2: variables_in H1 \/ variables_in H2 = (rng H1 \/ rng H2) \ {0,1,2,3,4}
by XBOOLE_1:42;
thus variables_in H1 '&' H2 c= variables_in H1 \/ variables_in H2
proof let a; assume a in variables_in H1 '&' H2;
then A3: a in {3} \/ (rng H1 \/ rng H2) & not a in {0,1,2,3,4} & a <> 3
by A1,Th150,XBOOLE_0:def 4;
then not a in {3} by TARSKI:def 1;
then a in rng H1 \/ rng H2 by A3,XBOOLE_0:def 2;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
rng H1 \/ rng H2 c= {3} \/ (rng H1 \/ rng H2) by XBOOLE_1:7;
hence thesis by A1,A2,XBOOLE_1:33;
end;
theorem
Th155: variables_in All(x,H) = variables_in H \/ {x}
proof All(x,H) = <*4*>^<*x*>^H by ZF_LANG:def 7;
then rng All(x,H) = rng (<*4*>^<*x*>) \/ rng H by FINSEQ_1:44
.= rng <*4*> \/ rng <*x*> \/ rng H by FINSEQ_1:44
.= {4} \/ rng <*x*> \/ rng H by FINSEQ_1:56
.= {4} \/ {x} \/ rng H by FINSEQ_1:56
.= {4} \/ ({x} \/ rng H) by XBOOLE_1:4;
then A1: variables_in All(x,H) = ({4} \/ ({x} \/ rng H)) \ {0,1,2,3,4} &
variables_in H = rng H \ {0,1,2,3,4} by Def3;
thus variables_in All(x,H) c= variables_in H \/ {x}
proof let a; assume a in variables_in All(x,H);
then A2: a in {4} \/ ({x} \/ rng H) & not a in {0,1,2,3,4} & a <> 4
by A1,Th150,XBOOLE_0:def 4;
then not a in {4} by TARSKI:def 1;
then a in {x} \/ rng H by A2,XBOOLE_0:def 2;
then (a in {x} or a in rng H) & (a in rng H implies a in variables_in H
)
by A1,A2,XBOOLE_0:def 2,def 4;
hence a in variables_in H \/ {x} by XBOOLE_0:def 2;
end;
let a; assume a in variables_in H \/ {x};
then a in variables_in H or a in {x} by XBOOLE_0:def 2;
then a in rng H & not a in {0,1,2,3,4} or a in {x} & x = a
by A1,TARSKI:def 1,XBOOLE_0:def 4;
then A3: a in {x} \/ rng H & not a in {0,1,2,3,4} by Th149,XBOOLE_0:def 2;
then a in {4} \/ ({x} \/ rng H) by XBOOLE_0:def 2;
hence thesis by A1,A3,XBOOLE_0:def 4;
end;
theorem
variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2
proof H1 'or' H2 = 'not'('not' H1 '&' 'not' H2) by ZF_LANG:def 16;
hence variables_in H1 'or' H2 = variables_in 'not' H1 '&' 'not' H2 by Th153
.= variables_in 'not' H1 \/ variables_in 'not' H2 by Th154
.= variables_in H1 \/ variables_in 'not' H2 by Th153
.= variables_in H1 \/ variables_in H2 by Th153;
end;
theorem
Th157: variables_in H1 => H2 = variables_in H1 \/ variables_in H2
proof H1 => H2 = 'not'(H1 '&' 'not' H2) by ZF_LANG:def 17;
hence variables_in H1 => H2 = variables_in H1 '&' 'not' H2 by Th153
.= variables_in H1 \/ variables_in 'not' H2 by Th154
.= variables_in H1 \/ variables_in H2 by Th153;
end;
theorem
variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2
proof H1 <=> H2 = (H1 => H2) '&' (H2 => H1) by ZF_LANG:def 18;
hence variables_in H1 <=> H2
= variables_in H1 => H2 \/ variables_in H2 => H1 by Th154
.= variables_in H1 \/ variables_in H2 \/ variables_in H2 => H1
by Th157
.= variables_in H1 \/ variables_in H2 \/
(variables_in H1 \/ variables_in H2) by Th157
.= variables_in H1 \/ variables_in H2;
end;
theorem
Th159: variables_in Ex(x,H) = variables_in H \/ {x}
proof Ex(x,H) = 'not' All(x,'not' H) by ZF_LANG:def 19;
hence variables_in Ex(x,H) = variables_in All(x,'not' H) by Th153
.= variables_in 'not' H \/ {x} by Th155
.= variables_in H \/ {x} by Th153;
end;
theorem
Th160: variables_in All(x,y,H) = variables_in H \/ {x,y}
proof All(x,y,H) = All(x,All(y,H)) by ZF_LANG:23;
hence variables_in All(x,y,H) = variables_in All(y,H) \/ {x} by Th155
.= variables_in H \/ {y} \/ {x} by Th155
.= variables_in H \/ ({y} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {x,y} by ENUMSET1:41;
end;
theorem
Th161: variables_in Ex(x,y,H) = variables_in H \/ {x,y}
proof Ex(x,y,H) = Ex(x,Ex(y,H)) by ZF_LANG:23;
hence variables_in Ex(x,y,H) = variables_in Ex(y,H) \/ {x} by Th159
.= variables_in H \/ {y} \/ {x} by Th159
.= variables_in H \/ ({y} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {x,y} by ENUMSET1:41;
end;
theorem
variables_in All(x,y,z,H) = variables_in H \/ {x,y,z}
proof All(x,y,z,H) = All(x,All(y,z,H)) by ZF_LANG:24;
hence variables_in All(x,y,z,H) = variables_in All(y,z,H) \/ {x} by Th155
.= variables_in H \/ {y,z} \/ {x} by Th160
.= variables_in H \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {y,z,x} by ENUMSET1:43
.= variables_in H \/ {x,y,z} by ENUMSET1:100;
end;
theorem
variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z}
proof Ex(x,y,z,H) = Ex(x,Ex(y,z,H)) by ZF_LANG:24;
hence variables_in Ex(x,y,z,H) = variables_in Ex(y,z,H) \/ {x} by Th159
.= variables_in H \/ {y,z} \/ {x} by Th161
.= variables_in H \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= variables_in H \/ {y,z,x} by ENUMSET1:43
.= variables_in H \/ {x,y,z} by ENUMSET1:100;
end;
theorem
Free H c= variables_in H
proof
defpred P[ZF-formula] means Free $1 c= variables_in $1;
A1: P[x '=' y] & P[x 'in' y]
proof
variables_in (x '=' y) = {x,y} & variables_in (x 'in' y) = {x,y} &
Free (x '=' y) = {x,y} & Free (x 'in' y) = {x,y}
by Th63,Th64,Th151,Th152;
hence thesis;
end;
A2: P[H1] implies P['not' H1]
proof assume Free H1 c= variables_in H1;
then Free 'not' H1 c= variables_in H1 by Th65;
hence thesis by Th153;
end;
A3: 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 Th66;
hence thesis by Th154;
end;
A4: P[H1] implies P[All(x,H1)]
proof assume
A5: Free H1 c= variables_in H1;
Free H1 \ {x} c= Free H1 & variables_in H1 c= variables_in H1 \/ {x}
by XBOOLE_1:7,36; then
A6: Free All(x,H1) c= Free H1 & variables_in H1 c= variables_in All(x,H1)
by Th67,Th155; then
Free H1 c= variables_in All(x,H1) by A5,XBOOLE_1:1;
hence thesis by A6,XBOOLE_1:1;
end;
for H holds P[H] from ZF_Induction(A1,A2,A3,A4);
hence thesis;
end;
definition let H;
redefine func variables_in H -> non empty Subset of VAR;
coherence
proof
defpred P[ZF-formula] means variables_in $1 <> {};
A1: variables_in H = rng H \ { 0,1,2,3,4 } by Def3;
A2: for x,y holds P[x '=' y] & P[x 'in' y]
proof let x,y;
variables_in x '=' y = {x,y} & variables_in x 'in' y = {x,y}
by Th151,Th152;
hence thesis;
end;
A3: for H st P[H] holds P['not' H] by Th153;
A4: 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 Th154
;
hence thesis by XBOOLE_1:15;
end;
A5: for H,x st P[H] holds P[All(x,H)]
proof let H,x;
variables_in All(x,H) = variables_in H \/ {x} & {x} <> {}
by Th155;
hence thesis;
end;
for H holds P[H] from ZF_Induction(A2,A3,A4,A5);
then reconsider D = variables_in H as non empty set;
D c= VAR
proof let a; assume a in D;
then A6: a in rng H & rng H c= NAT & a <> 0 & a <> 1 & a <> 2 &
a <> 3 & a <> 4 by A1,Th150,FINSEQ_1:def 4,XBOOLE_0:def 4;
then reconsider i = a as Nat;
0 < i & 0+1 = 1 by A6,NAT_1:18;
then 1 <= i by NAT_1:38;
then 1 < i & 1+1 = 2 by A6,REAL_1:def 5;
then 2 <= i by NAT_1:38;
then 2 < i & 2+1 = 3 by A6,REAL_1:def 5;
then 3 <= i by NAT_1:38;
then 3 < i & 3+1 = 4 by A6,REAL_1:def 5;
then 4 <= i by NAT_1:38;
then 4 < i & 4+1 = 5 by A6,REAL_1:def 5;
then 5 <= i by NAT_1:38;
hence a in VAR by ZF_LANG:def 1;
end;
hence variables_in H is non empty Subset of VAR;
end;
end;
definition let H,x,y;
func H/(x,y) -> Function means:
Def4: dom it = dom H & for a st a in dom H holds
(H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a);
existence
proof
defpred C[set] means H.$1 = x;
set A = dom H;
deffunc F(set) = y;
deffunc G(set) = H.$1;
thus ex f being Function st dom f = A &
for a st a in A holds
(C[a] implies f.a = F(a)) & (not C[a] implies f.a = G(a))
from LambdaC;
end;
uniqueness
proof let f1,f2 be Function such that
A1: dom f1 = dom H and
A2: for a 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 st a in dom H holds
(H.a = x implies f2.a = y) & (H.a <> x implies f2.a = H.a);
now let a; assume a in dom H;
then (H.a = x or H.a <> x) &
(H.a = x implies f1.a = y) & (H.a <> x implies f1.a = H.a) &
(H.a = x implies f2.a = y) & (H.a <> x implies f2.a = H.a)
by A2,A4;
hence f1.a = f2.a;
end;
hence thesis by A1,A3,FUNCT_1:9;
end;
end;
canceled;
theorem Th166:
(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);
H is_equality & Hz is_equality by ZF_LANG:16;
then A1: H is atomic & Hz is atomic by ZF_LANG:def 15;
then A2: len H = 3 & len Hz = 3 by ZF_LANG:27;
then A3: dom H = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
A4: Var1 H = x1 & Var2 H = x2 & Var1 Hz = z1 & Var2 Hz = z2 by Th1;
then A5: H.1 = 0 & H.2 = x1 & H.3 = x2 & Hz.1 = 0 & Hz.2 = z1 & Hz.3 = z2
by A1,ZF_LANG:31,52;
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
A6: (x1 '=' x2)/(y1,y2) = z1 '=' z2;
per cases;
case x1 <> y1 & x2 <> y1;
then H.2 <> y1 & H.3 <> y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = x1 & z2 = x2 by A5,A6,Def4;
case x1 = y1 & x2 <> y1;
then H.2 = y1 & H.3 <> y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = y2 & z2 = x2 by A5,A6,Def4;
case x1 <> y1 & x2 = y1;
then H.2 <> y1 & H.3 = y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = x1 & z2 = y2 by A5,A6,Def4;
case x1 = y1 & x2 = y1;
then H.2 = y1 & H.3 = y1 & 2 in dom H & 3 in dom H by A1,A3,A4,
ENUMSET1:14,ZF_LANG:52;
hence z1 = y2 & z2 = y2 by A5,A6,Def4;
end;
A7: dom f = dom H & dom H = Seg 3 & dom Hz = Seg 3 by A2,Def4,FINSEQ_1:def 3;
A8: y1 <> 0 by Th148;
A9: now assume
A10: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;
now let a; assume
A11: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A10,A11,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
A12: now assume
A13: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;
now let a; assume
A14: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A13,A14,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
A15: now assume
A16: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;
now let a; assume
A17: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A16,A17,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
now assume
A18: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;
now let a; assume
A19: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A18,A19,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
hence thesis by A9,A12,A15;
end;
theorem Th167:
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,Th166;
end;
theorem Th168:
(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);
H is_membership & Hz is_membership by ZF_LANG:16;
then A1: H is atomic & Hz is atomic by ZF_LANG:def 15;
then A2: len H = 3 & len Hz = 3 by ZF_LANG:27;
then A3: dom H = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
A4: Var1 H = x1 & Var2 H = x2 & Var1 Hz = z1 & Var2 Hz = z2 by Th2;
then A5: H.1 = 1 & H.2 = x1 & H.3 = x2 & Hz.1 = 1 & Hz.2 = z1 & Hz.3 = z2
by A1,ZF_LANG:31,52;
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
A6: (x1 'in' x2)/(y1,y2) = z1 'in' z2;
per cases;
case x1 <> y1 & x2 <> y1;
then H.2 <> y1 & H.3 <> y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = x1 & z2 = x2 by A5,A6,Def4;
case x1 = y1 & x2 <> y1;
then H.2 = y1 & H.3 <> y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = y2 & z2 = x2 by A5,A6,Def4;
case x1 <> y1 & x2 = y1;
then H.2 <> y1 & H.3 = y1 & 2 in dom H & 3 in
dom H by A1,A3,A4,ENUMSET1:14,ZF_LANG:52;
hence z1 = x1 & z2 = y2 by A5,A6,Def4;
case x1 = y1 & x2 = y1;
then H.2 = y1 & H.3 = y1 & 2 in dom H & 3 in dom H by A1,A3,A4,
ENUMSET1:14,ZF_LANG:52;
hence z1 = y2 & z2 = y2 by A5,A6,Def4;
end;
A7: dom f = dom H & dom H = Seg 3 & dom Hz = Seg 3 by A2,Def4,FINSEQ_1:def 3;
A8: y1 <> 1 by Th148;
A9: now assume
A10: x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2;
now let a; assume
A11: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A10,A11,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
A12: now assume
A13: x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2;
now let a; assume
A14: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A13,A14,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
A15: now assume
A16: x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2;
now let a; assume
A17: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A16,A17,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
now assume
A18: x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2;
now let a; assume
A19: a in dom H;
then a = 1 or a = 2 or a = 3 by A3,ENUMSET1:13;
hence Hz.a = f.a by A5,A8,A18,A19,Def4;
end;
hence f = Hz by A7,FUNCT_1:9;
end;
hence thesis by A9,A12,A15;
end;
theorem Th169:
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,Th168;
end;
theorem Th170:
'not' F = ('not' H)/(x,y) iff F = H/(x,y)
proof set N = ('not' H)/(x,y);
A1: len <*2*> = 1 & dom <*2*> = {1} by FINSEQ_1:4,56,def 8;
A2: 'not' F = <*2*>^F & 'not' H = <*2*>^H by ZF_LANG:def 5;
A3: dom 'not' F = Seg len 'not' F & dom 'not' H = Seg len 'not' H &
dom F = Seg len F & dom H = Seg len H by FINSEQ_1:def 3;
A4: len 'not' F = len <*2*> + len F & len 'not'
H = len <*2*> + len H by A2,FINSEQ_1:35;
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 Def4;
then len 'not' F = len 'not' H by FINSEQ_3:31;
then A7: len F = len H by A4,XCMPLX_1:2;
then A8: dom H = dom (H/(x,y)) & dom F = dom H by Def4,FINSEQ_3:31;
now let a; assume
A9: a in dom F;
then reconsider i = a as Nat;
F.a = N.(1+i) & 1+i in dom N
by A1,A2,A5,A9,FINSEQ_1:41,def 7;
then (('not' H).(1+i) = x implies F.a = y) & ('not' H).(1+i) = H.a &
(('not' H).(1+i) <> x implies F.a = ('not' H).(1+i))
by A1,A2,A3,A5,A6,A7,A9,Def4,FINSEQ_1:def 7;
then (H.a = x or H.a <> x) & (H.a = x implies H/(x,y).a = y) &
(H.a <> x implies H/(x,y).a = H.a) &
(H.a = x implies F.a = y) & (H.a <> x implies F.a = H.a) by A3,A7,A9,
Def4;
hence F.a = H/(x,y).a;
end;
hence F = H/(x,y) by A8,FUNCT_1:9;
end;
assume
A10: F = H/(x,y);
then A11: dom F = dom H by Def4;
then A12: len F = len H by FINSEQ_3:31;
then A13: dom 'not' F = dom N & dom N = dom 'not' H by A3,A4,Def4;
now let a; assume
A14: a in dom 'not' F;
then reconsider i = a as Nat;
A15: now assume i in {1};
then i = 1 & ('not' H).1 = 2 & 2 <> x by Th148,TARSKI:def 1,ZF_LANG:32
;
then ('not' F).i = 2 & N.i = 2 by A3,A4,A12,A14,Def4,ZF_LANG:32;
hence ('not' F).a = N.a;
end;
now given j such that
A16: j in dom F & i = 1+j;
H.j = ('not' H).i & F.j = ('not'
F).i by A1,A2,A11,A16,FINSEQ_1:def 7;
then (('not' H).a <> x implies ('not' F).a = ('not' H).a) &
(('not' H).a = x implies ('not' F).a = y) &
(('not' H).a <> x implies N.a = ('not' H).a) & (('not'
H).a = x implies N.a = y)
by A3,A4,A10,A12,A14,A16,Def4;
hence ('not' F).a = N.a;
end;
hence ('not' F).a = N.a by A1,A2,A14,A15,FINSEQ_1:38;
end;
hence thesis by A13,FUNCT_1:9;
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: len <*3*> = 1 & dom <*3*> = {1} by FINSEQ_1:4,56,def 8;
A2: G1 '&' G2 = <*3*>^G1^G2 & H1 '&' H2 = <*3*>^H1^H2 by ZF_LANG:def 6;
A3: dom (G1 '&' G2) = Seg len (G1 '&' G2) & dom G1 = Seg len G1 &
dom G2 = Seg len G2 & dom (H1 '&' H2) = Seg len (H1 '&' H2) &
dom H1 = Seg len H1 & dom H2 = Seg len H2 by FINSEQ_1:def 3;
A4: len (<*3*>^G1) = 1+len G1 & len (<*3*>^H1) = 1+len H1
by A1,FINSEQ_1:35;
then A5: len (G1 '&' G2) = 1+len G1 + len G2 & len (H1 '&' H2) = 1+len H1 + len
H2
by A2,FINSEQ_1:35;
A6: dom (<*3*>^G1) = Seg (1+len G1) & dom (<*3*>^H1) = Seg (1+len H1)
by A4,FINSEQ_1:def 3;
assume
A7: G1 = H1/(x,y) & G2 = H2/(x,y);
then A8: dom G1 = dom H1 & dom G2 = dom H2 by Def4;
then A9: len G1 = len H1 & len G2 = len H2 by FINSEQ_3:31;
then A10: dom N = dom (G1 '&' G2) & dom N = dom (H1 '&' H2) by A3,A5,Def4;
now let a; assume
A11: a in dom N; then reconsider i = a as Nat by A10;
A12: now assume
A13: i in dom (<*3*>^G1);
then A14: (G1 '&' G2).i = (<*3*>^G1).i & (H1 '&' H2).i = (<*3*>^H1).i
by A2,A6,A9,FINSEQ_1:def 7;
A15: now assume i in {1};
then i = 1 & (H1 '&' H2).1 = 3 & x <> 3 by Th148,TARSKI:def 1,ZF_LANG
:33
;
then N.i = 3 & (G1 '&' G2).i = 3 by A10,A11,Def4,ZF_LANG:33;
hence N.a = (G1 '&' G2).a;
end;
now given j such that
A16: j in dom G1 & i = 1+j;
G1.j = (G1 '&' G2).i & H1.j = (H1 '&' H2).i & j in dom H1
by A1,A8,A14,A16,FINSEQ_1:def 7;
then ((H1 '&' H2).a <> x implies (G1 '&' G2).a = (H1 '&' H2).a) &
((H1 '&' H2).a = x implies (G1 '&' G2).a = y) &
((H1 '&' H2).a <> x implies N.a = (H1 '&' H2).a) &
((H1 '&' H2).a = x implies N.a = y)
by A7,A10,A11,Def4;
hence (G1 '&' G2).a = N.a;
end;
hence (G1 '&' G2).a = N.a by A1,A13,A15,FINSEQ_1:38;
end;
now given j such that
A17: j in dom G2 & i = 1+len G1+j;
G2.j = (G1 '&' G2).i & H2.j = (H1 '&' H2).i & j in dom H2
by A2,A3,A4,A9,A17,FINSEQ_1:def 7;
then ((H1 '&' H2).a <> x or (H1 '&' H2).a = x) &
((H1 '&' H2).a <> x implies N.a = (H1 '&' H2).a) &
((H1 '&' H2).a = x implies N.a = y) &
((H1 '&' H2).a <> x implies (G1 '&' G2).a = (H1 '&' H2).a) &
((H1 '&' H2).a = x implies (G1 '&' G2).a = y) by A7,A10,A11,Def4;
hence (G1 '&' G2).a = N.a;
end;
hence (G1 '&' G2).a = N.a by A2,A4,A10,A11,A12,FINSEQ_1:38;
end;
hence thesis by A10,FUNCT_1:9;
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: All(z,F) = <*4*>^<*z*>^F & All(s,H) = <*4*>^<*s*>^H by ZF_LANG:def 7;
len <*4*> = 1 & len <*z*> = 1 & len <*s*> = 1 & 1+1 = 2
by FINSEQ_1:56;
then A2: len (<*4*>^<*z*>) = 2 & len (<*4*>^<*s*>) = 2 by FINSEQ_1:35;
then len All(z,F) = 2+len F & len All(s,H) = 2+len H by A1,FINSEQ_1:35;
then A3: dom All(z,F) = Seg (2+len F) & dom All(s,H) = Seg (2+len H) &
dom H = Seg len H & dom F = Seg len F by FINSEQ_1:def 3;
A4: dom (<*4*>^<*z*>) = {1,2} & dom (<*4*>^<*s*>) = {1,2} &
<*4*>^<*z*> = <*4,z*> & <*4*>^<*s*> = <*4,s*>
by A2,FINSEQ_1:4,def 3,def 9;
assume
A5: F = H/(x,y) & (z = s & s <> x or z = y & s = x);
then A6: dom F = dom H by Def4;
then A7: dom All(s,H) = dom All(z,F) & dom N = dom All(s,H) by A3,Def4,
FINSEQ_3:31;
now let a; assume
A8: a in dom N;
A9: now assume A10: a in {1,2};
then A11: (a = 1 or a = 2) & x <> 4 & a in dom <*4,z*> by A4,Th148,TARSKI:
def 2;
All(z,F).a = <*4,z*>.a & All(s,H).a = <*4,s*>.a & <*4,z*>.1 = 4 &
<*4,s*>.1 = 4 & <*4,z*>.2 = z & <*4,s*>.2 = s
by A1,A4,A10,FINSEQ_1:61,def 7;
hence All(z,F).a = All(s,H)/(x,y).a by A5,A7,A8,A11,Def4;
end;
now given i such that
A12: i in dom H & a = 2+i;
All(z,F).a = F.i & All(s,H).a = H.i
by A1,A2,A6,A12,FINSEQ_1:def 7;
then (All(s,H).a <> x implies All(z,F).a = All(s,H).a) &
(All(s,H).a = x implies All(z,F).a = y) &
(All(s,H).a <> x implies All(s,H)/(x,y).a = All(s,H).a) &
(All(s,H).a = x implies All(s,H)/(x,y).a = y) by A5,A7,A8,A12,Def4;
hence All(z,F).a = All(s,H)/(x,y).a;
end;
hence All(z,F).a = All(s,H)/(x,y).a by A1,A2,A4,A7,A8,A9,FINSEQ_1:38;
end;
hence thesis by A7,FUNCT_1:9;
end;
theorem
Th171: H/(x,y) in WFF
proof
defpred P[ZF-formula] means $1/(x,y) in WFF;
A1: for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2]
proof let x1,x2;
A2: ex y1,y2 st (x1 '=' x2)/(x,y) = y1 '=' y2 by Th167;
ex z1,z2 st (x1 'in' x2)/(x,y) = z1 'in' z2 by Th169;
hence thesis by A2,ZF_LANG:14;
end;
A3: 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:14;
'not' F = ('not' H)/(x,y) by Th170;
hence thesis by ZF_LANG:14;
end;
A4: 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:14;
F1 '&' F2 = (H1 '&' H2)/(x,y) by Lm1;
hence thesis by ZF_LANG:14;
end;
A5: 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:14;
z <> x or z = x;
then consider s such that
A6: s = z & z <> x or s = y & z = x;
All(s,F) = All(z,H)/(x,y) by A6,Lm2;
hence thesis by ZF_LANG:14;
end;
for H holds P[H] from ZF_Induction(A1,A3,A4,A5);
hence thesis;
end;
definition let H,x,y;
redefine func H/(x,y) -> ZF-formula;
coherence
proof
A1: dom (H/(x,y)) = dom H & for a st a in dom H holds
(H.a = x implies H/(x,y).a = y) & (H.a <> x implies H/(x,y).a = H.a)
by Def4;
dom H = Seg len H by FINSEQ_1:def 3;
then reconsider f = H/(x,y) as FinSequence by A1,FINSEQ_1:def 2;
rng f c= NAT
proof let a; assume a in rng f;
then consider b being set such that
A2: b in dom f & a = f.b by FUNCT_1:def 5;
(H.b = x or H.b <> x) &
rng H c= NAT & H.b in rng H by A1,A2,FINSEQ_1:def 4,FUNCT_1:def 5
;
then a = y or a = H.b & H.b in NAT by A1,A2;
hence thesis;
end;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
f in WFF by Th171;
hence thesis by ZF_LANG:14;
end;
end;
theorem Th172:
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:47;
end;
thus thesis by Lm1;
end;
theorem Th173:
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:12;
end;
thus thesis by A1,Lm2;
end;
theorem Th174:
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:12;
end;
thus thesis by Lm2;
end;
theorem Th175:
G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
G1 'or' G2 = 'not'('not' G1 '&' 'not' G2) & H1 'or' H2 = 'not'('not' H1
'&'
'not' H2)
by ZF_LANG:def 16;
then (G1 'or' G2 = (H1 'or' H2)/(x,y) iff 'not' G1 '&' 'not' G2 = ('not'
H1 '&'
'not' H2)/(x,y)) &
('not' G1 = ('not' H1)/(x,y) & 'not' G2 = ('not' H2)/(x,y) iff
'not' G1 '&' 'not' G2 = ('not' H1 '&' 'not' H2)/(x,y)) &
('not' G1 = ('not' H1)/(x,y) iff G1 = H1/(x,y)) &
('not' G2 = ('not' H2)/(x,y) iff G2 = H2/(x,y)) by Th170,Th172;
hence thesis;
end;
theorem Th176:
G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
G1 => G2 = 'not'(G1 '&' 'not' G2) & H1 => H2 = 'not'(H1 '&' 'not'
H2) by ZF_LANG:def 17;
then (G1 => G2 = (H1 => H2)/(x,y) iff G1 '&' 'not' G2 =
(H1 '&' 'not' H2)/(x,y)) &
(G1 = H1/(x,y) & 'not' G2 = ('not' H2)/(x,y) iff G1 '&' 'not' G2 = (H1 '&'
'not' H2)/(x,y)) &
('not' G2 = ('not' H2)/(x,y) iff G2 = H2/(x,y)) by Th170,Th172;
hence thesis;
end;
theorem Th177:
G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)
proof
G1 <=> G2 = (G1 => G2) '&' (G2 => G1) &
H1 <=> H2 = (H1 => H2) '&' (H2 => H1) by ZF_LANG:def 18;
then (G1 <=> G2 = (H1 <=> H2)/(x,y) iff
G1 => G2 = (H1 => H2)/(x,y) & G2 => G1 = (H2 => H1)/(x,y)) &
(G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y)) &
(G2 => G1 = (H2 => H1)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y))
by Th172,Th176;
hence thesis;
end;
theorem Th178:
z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y))
proof assume
A1: z <> x;
Ex(z,G) = 'not' All(z,'not' G) & Ex(z,H) = 'not' All(z,'not'
H) by ZF_LANG:def 19;
then (Ex(z,G) = Ex(z,H)/(x,y) iff All(z,'not' G) = All(z,'not' H)/(x,y)) &
('not' G = ('not' H)/(x,y) iff All(z,'not' G) = All(z,'not' H)/(x,y)) &
('not' G = ('not' H)/(x,y) iff G = H/(x,y)) by A1,Th170,Th173;
hence thesis;
end;
theorem Th179:
Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y)
proof
Ex(y,G) = 'not' All(y,'not' G) & Ex(x,H) = 'not' All(x,'not'
H) by ZF_LANG:def 19;
then (Ex(y,G) = Ex(x,H)/(x,y) iff All(y,'not' G) = All(x,'not' H)/(x,y)) &
('not' G = ('not' H)/(x,y) iff All(y,'not' G) = All(x,'not' H)/(x,y)) &
('not' G = ('not' H)/(x,y) iff G = H/(x,y)) by Th170,Th174;
hence thesis;
end;
theorem
H is_equality iff H/(x,y) is_equality
proof
thus H is_equality implies H/(x,y) is_equality
proof given x1,x2 such that
A1: H = x1 '=' x2;
ex z1,z2 st H/(x,y) = z1 '=' z2 by A1,Th167;
hence thesis by ZF_LANG:16;
end;
assume
A2: H/(x,y) is_equality;
1 <= 3 & 3 <= len H by ZF_LANG:29;
then 1 <= 1 & 1 <= len H & dom H = Seg len H by AXIOMS:22,FINSEQ_1:def 3;
then A3: H/(x,y).1 = 0 & y <> 0 & 1 in dom H by A2,Th148,FINSEQ_3:27,ZF_LANG:
35
;
then H.1 <> x by Def4;
then 0 = H.1 by A3,Def4;
hence thesis by ZF_LANG:41;
end;
theorem
H is_membership iff H/(x,y) is_membership
proof
thus H is_membership implies H/(x,y) is_membership
proof given x1,x2 such that
A1: H = x1 'in' x2;
ex z1,z2 st H/(x,y) = z1 'in' z2 by A1,Th169;
hence thesis by ZF_LANG:16;
end;
assume
A2: H/(x,y) is_membership;
1 <= 3 & 3 <= len H by ZF_LANG:29;
then 1 <= 1 & 1 <= len H & dom H = Seg len H by AXIOMS:22,FINSEQ_1:def 3;
then A3: H/(x,y).1 = 1 & y <> 1 & 1 in dom H by A2,Th148,FINSEQ_3:27,ZF_LANG:
36
;
then H.1 <> x by Def4;
then 1 = H.1 by A3,Def4;
hence thesis by ZF_LANG:42;
end;
theorem Th182:
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,Th170;
hence thesis by ZF_LANG:16;
end;
assume
A2: H/(x,y) is negative;
1 <= 3 & 3 <= len H by ZF_LANG:29;
then 1 <= 1 & 1 <= len H & dom H = Seg len H by AXIOMS:22,FINSEQ_1:def 3;
then A3: H/(x,y).1 = 2 & y <> 2 & 1 in dom H by A2,Th148,FINSEQ_3:27,ZF_LANG:
37
;
then H.1 <> x by Def4;
then 2 = H.1 by A3,Def4;
hence thesis by ZF_LANG:43;
end;
theorem Th183:
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,Th172;
hence thesis by ZF_LANG:16;
end;
assume
A2: H/(x,y) is conjunctive;
1 <= 3 & 3 <= len H by ZF_LANG:29;
then 1 <= 1 & 1 <= len H by AXIOMS:22;
then A3: H/(x,y).1 = 3 & y <> 3 & 1 in dom H by A2,Th148,FINSEQ_3:27,ZF_LANG:
38
;
then H.1 <> x by Def4;
then 3 = H.1 by A3,Def4;
hence thesis by ZF_LANG:44;
end;
theorem Th184:
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,Th173,Th174;
hence thesis by ZF_LANG:16;
end;
assume
A3: H/(x,y) is universal;
1 <= 3 & 3 <= len H by ZF_LANG:29;
then 1 <= 1 & 1 <= len H by AXIOMS:22;
then A4: H/(x,y).1 = 4 & y <> 4 & 1 in dom H by A3,Th148,FINSEQ_3:27,ZF_LANG:
39
;
then H.1 <> x by Def4;
then 4 = H.1 by A4,Def4;
hence thesis by ZF_LANG:45;
end;
theorem
H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/(x,y)
proof assume H is negative;
then H/(x,y) is negative & H = 'not'
the_argument_of H by Th182,ZF_LANG:def 30;
then H/(x,y) = 'not' the_argument_of (H/(x,y)) &
H/(x,y) = 'not' ((the_argument_of H)/(x,y)) by Th170,ZF_LANG:def 30;
hence the_argument_of (H/(x,y)) = (the_argument_of H)/(x,y) by ZF_LANG:10;
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 H is conjunctive;
then H/(x,y) is conjunctive &
H = (the_left_argument_of H) '&' (the_right_argument_of H)
by Th183,ZF_LANG:58;
then H/(x,y) = (the_left_argument_of (H/(x,y))) '&'
(the_right_argument_of (H/(x,y))) &
H/(x,y) = ((the_left_argument_of H)/(x,y)) '&'
((the_right_argument_of H)/(x,y)) by Th172,ZF_LANG:58;
hence thesis by ZF_LANG:47;
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 H is universal;
then H/(x,y) is universal & H = All(bound_in H,the_scope_of H)
by Th184,ZF_LANG:62;
then H/(x,y) = All(bound_in (H/(x,y)),the_scope_of (H/(x,y))) &
(bound_in H = x implies H/(x,y) = All(y,(the_scope_of H)/(x,y))) &
(bound_in H <> x implies H/(x,y) = All(bound_in H,(the_scope_of H)/(x,y)))
by Th173,Th174,ZF_LANG:62;
hence thesis by ZF_LANG:12;
end;
theorem Th188:
H is disjunctive iff H/(x,y) is disjunctive
proof
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,Th175;
hence thesis by ZF_LANG:22;
end;
set G = H/(x,y);
given G1,G2 such that
A2: G = G1 'or' G2;
A3: G = 'not'('not' G1 '&' 'not' G2) by A2,ZF_LANG:def 16;
then G is negative by ZF_LANG:16;
then H is negative by Th182;
then consider H' being ZF-formula such that
A4: H = 'not' H' by ZF_LANG:16;
A5: 'not' G1 '&' 'not' G2 = H'/(x,y) by A3,A4,Th170;
then H'/(x,y) is conjunctive by ZF_LANG:16;
then H' is conjunctive by Th183;
then consider H1,H2 such that
A6: H' = H1 '&' H2 by ZF_LANG:16;
A7: 'not' G1 = H1/(x,y) & 'not' G2 = H2/(x,y) by A5,A6,Th172;
then H1/(x,y) is negative by ZF_LANG:16;
then H1 is negative by Th182;
then consider p1 such that
A8: H1 = 'not' p1 by ZF_LANG:16;
H2/(x,y) is negative by A7,ZF_LANG:16;
then H2 is negative by Th182;
then consider p2 such that
A9: H2 = 'not' p2 by ZF_LANG:16;
H = p1 'or' p2 by A4,A6,A8,A9,ZF_LANG:def 16;
hence thesis by ZF_LANG:22;
end;
theorem Th189:
H is conditional iff H/(x,y) is conditional
proof
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,Th176;
hence thesis by ZF_LANG:22;
end;
set G = H/(x,y);
given G1,G2 such that
A2: G = G1 => G2;
A3: G = 'not'(G1 '&' 'not' G2) by A2,ZF_LANG:def 17;
then G is negative by ZF_LANG:16;
then H is negative by Th182;
then consider H' being ZF-formula such that
A4: H = 'not' H' by ZF_LANG:16;
A5: G1 '&' 'not' G2 = H'/(x,y) by A3,A4,Th170;
then H'/(x,y) is conjunctive by ZF_LANG:16;
then H' is conjunctive by Th183;
then consider H1,H2 such that
A6: H' = H1 '&' H2 by ZF_LANG:16;
G1 = H1/(x,y) & 'not' G2 = H2/(x,y) by A5,A6,Th172;
then H2/(x,y) is negative by ZF_LANG:16;
then H2 is negative by Th182;
then consider p2 such that
A7: H2 = 'not' p2 by ZF_LANG:16;
H = H1 => p2 by A4,A6,A7,ZF_LANG:def 17;
hence thesis by ZF_LANG:22;
end;
theorem Th190:
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,Th177;
hence thesis by ZF_LANG:22;
end;
theorem Th191:
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,Th178,Th179;
hence thesis by ZF_LANG:22;
end;
given z,G such that
A3: H/(x,y) = Ex(z,G);
A4: H/(x,y) = 'not' All(z,'not' G) by A3,ZF_LANG:def 19;
then H/(x,y) is negative by ZF_LANG:16;
then H is negative by Th182;
then consider H1 such that
A5: H = 'not' H1 by ZF_LANG:16;
A6: H1/(x,y) = All(z,'not' G) by A4,A5,Th170;
bound_in H1 = x or bound_in H1 <> x;
then consider s such that
A7: bound_in H1 = x & s = y or bound_in H1 <> x & s = bound_in H1;
H1/(x,y) is universal by A6,ZF_LANG:16;
then H1 is universal by Th184;
then A8: H1 = All(bound_in H1, the_scope_of H1) by ZF_LANG:62;
then All(z,'not' G) = All(s,(the_scope_of H1)/(x,y)) by A6,A7,Th173,Th174;
then 'not' G = (the_scope_of H1)/(x,y) by ZF_LANG:12;
then (the_scope_of H1)/(x,y) is negative by ZF_LANG:16;
then the_scope_of H1 is negative by Th182;
then the_scope_of H1 = 'not'
the_argument_of the_scope_of H1 by ZF_LANG:def 30;
then H = Ex(bound_in H1, the_argument_of the_scope_of H1) by A5,A8,ZF_LANG:
def 19;
hence thesis by ZF_LANG:22;
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 H is disjunctive;
then H/(x,y) is disjunctive &
H = (the_left_argument_of H) 'or' (the_right_argument_of H)
by Th188,ZF_LANG:59;
then H/(x,y) = (the_left_argument_of (H/(x,y))) 'or'
(the_right_argument_of (H/(x,y))) &
H/(x,y) = ((the_left_argument_of H)/(x,y)) 'or'
((the_right_argument_of H)/(x,y)) by Th175,ZF_LANG:59;
hence thesis by ZF_LANG:48;
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 H is conditional;
then H/(x,y) is conditional &
H = (the_antecedent_of H) => (the_consequent_of H)
by Th189,ZF_LANG:65;
then H/(x,y) = (the_antecedent_of (H/(x,y))) =>
(the_consequent_of (H/(x,y))) &
H/(x,y) = ((the_antecedent_of H)/(x,y)) =>
((the_consequent_of H)/(x,y)) by Th176,ZF_LANG:65;
hence thesis by ZF_LANG:49;
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/(x,y) is biconditional &
H = (the_left_side_of H) <=> (the_right_side_of H)
by Th190,ZF_LANG:67;
then H/(x,y) = (the_left_side_of (H/(x,y))) <=>
(the_right_side_of (H/(x,y))) &
H/(x,y) = ((the_left_side_of H)/(x,y)) <=>
((the_right_side_of H)/(x,y)) by Th177,ZF_LANG:67;
hence thesis by ZF_LANG:50;
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 H is existential;
then H/(x,y) is existential & H = Ex(bound_in H,the_scope_of H)
by Th191,ZF_LANG:63;
then H/(x,y) = Ex(bound_in (H/(x,y)),the_scope_of (H/(x,y))) &
(bound_in H = x implies H/(x,y) = Ex(y,(the_scope_of H)/(x,y))) &
(bound_in H <> x implies H/(x,y) = Ex(bound_in H,(the_scope_of H)/(x,y)))
by Th178,Th179,ZF_LANG:63;
hence thesis by ZF_LANG:51;
end;
theorem
Th196: not x in variables_in H implies H/(x,y) = H
proof assume not x in variables_in H;
then A1: not x in rng H \ {0,1,2,3,4} & not x in {0,1,2,3,4} by Def3,Th149;
then A2: not x in rng H & dom H = dom (H/(x,y)) by Def4,XBOOLE_0:def 4;
now let a; assume a in dom H;
then H.a in rng H & (H.a <> x implies H/(x,y).a = H.a) by Def4,FUNCT_1:
def 5;
hence H/(x,y).a = H.a by A1,XBOOLE_0:def 4;
end;
hence H/(x,y) = H by A2,FUNCT_1:9;
end;
theorem
Th197: H/(x,x) = H
proof
A1: dom (H/(x,x)) = dom H by Def4;
now let a; assume a in dom H;
then (H.a = x implies H/(x,x).a = x) & (H.a <> x implies H/(x,x).a = H.a
)
by Def4;
hence H.a = H/(x,x).a;
end;
hence thesis by A1,FUNCT_1:9;
end;
theorem
Th198: 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 x in rng (H/(x,y)) \ {0,1,2,3,4} by Def3;
then x in rng (H/(x,y)) by XBOOLE_0:def 4;
then consider a such that
A2: a in dom (H/(x,y)) & x = H/(x,y).a by FUNCT_1:def 5;
dom (H/(x,y)) = dom H by Def4;
then (H.a = x implies H/(x,y).a = y) & (H.a <> x implies H/(x,y).a = H.a)
by A2,Def4;
hence contradiction by A1,A2;
end;
theorem
x in variables_in H implies y in variables_in (H/(x,y))
proof assume
x in variables_in H;
then x in rng H \ {0,1,2,3,4} by Def3;
then x in rng H by XBOOLE_0:def 4;
then consider a such that
A1: a in dom H & x = H.a by FUNCT_1:def 5;
dom (H/(x,y)) = dom H & H/(x,y).a = y by A1,Def4;
then y in rng (H/(x,y)) & not y in {0,1,2,3,4} by A1,Th149,FUNCT_1:def 5;
then y in rng (H/(x,y)) \ {0,1,2,3,4} by XBOOLE_0:def 4;
hence thesis by Def3;
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 Th198;
hence thesis by Th196;
end;
theorem
variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y}
proof
A1: X c= (X \ {a}) \/ {a}
proof let b be set; assume b in X;
then b in X \ {a} or b in {a} by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 2;
end;
now per cases;
suppose
A2: x = y; then H = H/(x,y) by Th197;
hence thesis by A1,A2;
suppose A3: x <> y;
thus thesis
proof let a; assume A4: a in variables_in (H/(x,y));
then A5: a in rng (H/(x,y)) \ {0,1,2,3,4} & a in VAR & a <> x
by A3,Def3,Th198;
reconsider z = a as Variable by A4;
z in rng (H/(x,y)) by A5,XBOOLE_0:def 4;
then consider b being set such that
A6: b in dom (H/(x,y)) & z = H/(x,y).b by FUNCT_1:def 5;
A7: dom (H/(x,y)) = dom H by Def4;
then (H.b = x implies z = y) & (H.b <> x implies z = H.b) by A6,Def4;
then z in {y} or z in rng H & not z in {0,1,2,3,4} & not z in {x}
by A6,A7,Th149,FUNCT_1:def 5,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 4;
then z in {y} or z in variables_in H & not z in {x} by Def3;
then z in {y} or z in variables_in H \ {x} by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 2;
end;
end;
hence thesis;
end;