:: Properties of ZF Models
:: by Grzegorz Bancerek
::
:: Received July 5, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, ZF_MODEL,
TARSKI, BVFUNC_2, XBOOLEAN, FUNCT_4, ZFMISC_1, NAT_1, FINSEQ_1, ARYTM_3,
CLASSES2, XXREAL_0, MCART_1, RELAT_1, ZFMODEL1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, XXREAL_0,
ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, ZF_LANG, RELSET_1,
FUNCT_2, FUNCT_7, NAT_1, ZF_MODEL, MCART_1;
constructors ENUMSET1, XXREAL_0, NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, RELSET_1,
XTUPLE_0, NUMBERS;
registrations SUBSET_1, MEMBERED, ZF_LANG, RELAT_1, XXREAL_0, RELSET_1,
XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ORDINAL1, ZF_MODEL, ZF_LANG, RELAT_1, FUNCT_1, XBOOLE_0,
FUNCT_2;
equalities ZF_MODEL, ZF_LANG, XBOOLE_0;
expansions TARSKI, ORDINAL1, ZF_MODEL, ZF_LANG, XBOOLE_0;
theorems TARSKI, ZF_LANG, ZF_MODEL, ZFMISC_1, FUNCT_1, FUNCT_2, ENUMSET1,
RELAT_1, RELSET_1, XBOOLE_0, FUNCT_7, XTUPLE_0;
schemes NAT_1, ZF_LANG, XBOOLE_0;
begin
reserve x,y,z for Variable,
H for ZF-formula,
E for non empty set,
a,b,c,X,Y,Z for set,
u,v,w for Element of E,
f,g,h,i,j for Function of VAR,E;
set x0 = x.0, x1 = x.1, x2 = x.2, x3 = x.3, x4 = x.4;
theorem
E is epsilon-transitive implies E |= the_axiom_of_extensionality
proof
assume
A1: X in E implies X c= E;
E |= All(x2,x2 'in' x0 <=> x2 'in' x1) => x0 '=' x1
proof
let f;
now
assume
A2: E,f |= All(x2,x2 'in' x0 <=> x2 'in' x1);
f.x0 = f.x1
proof
thus for a being object holds a in f.x0 implies a in f.x1
proof let a be object;
assume
A3: a in f.x0;
f.x0 c= E by A1;
then reconsider a9 = a as Element of E by A3;
set g = f+*(x2,a9);
A4: g.x1 = f.x1 by FUNCT_7:32;
for x st g.x <> f.x holds x2 = x by FUNCT_7:32;
then E,g |= x2 'in' x0 <=> x2 'in' x1 by A2,ZF_MODEL:16;
then
A5: E,g |= x2 'in' x0 iff E,g |= x2 'in' x1 by ZF_MODEL:19;
g.x2 = a9 & g.x0 = f.x0 by FUNCT_7:32,128;
hence thesis by A3,A5,A4,ZF_MODEL:13;
end;
let a be object such that
A6: a in f.x1;
f.x1 c= E by A1;
then reconsider a9 = a as Element of E by A6;
set g = f+*(x2,a9);
A7: g.x1 = f.x1 by FUNCT_7:32;
for x st g.x <> f.x holds x2 = x by FUNCT_7:32;
then E,g |= x2 'in' x0 <=> x2 'in' x1 by A2,ZF_MODEL:16;
then
A8: E,g |= x2 'in' x0 iff E,g |= x2 'in' x1 by ZF_MODEL:19;
g.x2 = a9 & g.x0 = f.x0 by FUNCT_7:32,128;
hence thesis by A6,A8,A7,ZF_MODEL:13;
end;
hence E,f |= x0 '=' x1 by ZF_MODEL:12;
end;
hence thesis by ZF_MODEL:18;
end;
then E |= All(x1,All(x2,x2 'in' x0 <=> x2 'in' x1) => x0 '=' x1) by
ZF_MODEL:23;
hence thesis by ZF_MODEL:23;
end;
theorem Th2:
E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for
u,v holds { u,v } in E)
proof
assume
A1: X in E implies X c= E;
A2: a in u implies a is Element of E
proof
assume
A3: a in u;
u c= E by A1;
hence thesis by A3;
end;
A4: E |= All(x1,Ex(x2,All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) )) iff
E |= Ex(x2,All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) ) by ZF_MODEL:23;
thus E |= the_axiom_of_pairs implies for u,v holds { u,v } in E
proof
set fv = the Function of VAR,E;
assume
A5: E |= the_axiom_of_pairs;
let u,v;
set g = fv+*(x0,u);
set f = g+*(x1,v);
E,f |= Ex(x2,All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) ) by A4,A5,
ZF_MODEL:23;
then consider h such that
A6: for x st h.x <> f.x holds x2 = x and
A7: E,h |= All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) by ZF_MODEL:20;
A8: f.x1 = v by FUNCT_7:128;
A9: g.x0 = u by FUNCT_7:128;
then
A10: f.x0 = u by FUNCT_7:32;
for a be object holds a in h.x2 iff a = u or a = v
proof
let a be object;
thus a in h.x2 implies a = u or a = v
proof
assume
A11: a in h.x2;
then reconsider a9 = a as Element of E by A2;
set f3 = h+*(x3,a9);
A12: f3.x3 = a9 by FUNCT_7:128;
for x st f3.x <> h.x holds x3 = x by FUNCT_7:32;
then E,f3 |= x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1 by A7,ZF_MODEL:16;
then
A13: E,f3 |= x3 'in' x2 iff E,f3 |= x3 '=' x0 'or' x3 '=' x1 by ZF_MODEL:19;
f3.x2 = h.x2 by FUNCT_7:32;
then E,f3 |= x3 '=' x0 or E,f3 |= x3 '=' x1 by A11,A12,A13,ZF_MODEL:13
,17;
then
A14: f3.x3 = f3.x0 or f3.x3 = f3.x1 by ZF_MODEL:12;
A15: f3.x1 = h.x1 by FUNCT_7:32;
f3.x0 = h.x0 & h.x0 = f.x0 by A6,FUNCT_7:32;
hence thesis by A9,A8,A6,A12,A14,A15,FUNCT_7:32;
end;
assume
A16: a = u or a = v;
then reconsider a9 = a as Element of E;
set f3 = h+*(x3,a9);
A17: f3.x3 = a9 by FUNCT_7:128;
for x st f3.x <> h.x holds x3 = x by FUNCT_7:32;
then E,f3 |= x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1 by A7,ZF_MODEL:16;
then
A18: E,f3 |= x3 'in' x2 iff E,f3 |= x3 '=' x0 'or' x3 '=' x1 by ZF_MODEL:19;
A19: f3.x1 = h.x1 & h.x1 = f.x1 by A6,FUNCT_7:32;
f3.x0 = h.x0 & h.x0 = f.x0 by A6,FUNCT_7:32;
then E,f3 |= x3 '=' x0 or E,f3 |= x3 '=' x1 by A8,A10,A16,A17,A19,
ZF_MODEL:12;
then f3.x3 in f3.x2 by A18,ZF_MODEL:13,17;
hence thesis by A17,FUNCT_7:32;
end;
then h.x2 = { u,v } by TARSKI:def 2;
hence thesis;
end;
assume
A20: for u,v holds { u,v } in E;
let f;
now
let g such that
for x st g.x <> f.x holds x0 = x or x1 = x;
reconsider w = { g.x0,g.x1 } as Element of E by A20;
set h = g+*(x2,w);
A21: h.x2 = w by FUNCT_7:128;
now
let m be Function of VAR,E;
A22: h.x0 = g.x0 & h.x1 = g.x1 by FUNCT_7:32;
A23: E,m |= x3 'in' x2 iff m.x3 in m.x2 by ZF_MODEL:13;
A24: E,m |= x3 '=' x0 'or' x3 '=' x1 iff E,m |= x3 '=' x0 or E,m |= x3
'=' x1 by ZF_MODEL:17;
A25: E,m |= x3 '=' x1 iff m.x3 = m.x1 by ZF_MODEL:12;
A26: E,m |= x3 '=' x0 iff m.x3 = m.x0 by ZF_MODEL:12;
assume
A27: for x st m.x <> h.x holds x3 = x;
then
A28: m.x2 = h .x2;
m.x0 = h.x0 & m.x1 = h.x1 by A27;
hence E,m |= x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1 by A21,A22,A28,A23
,A26,A25,A24,TARSKI:def 2,ZF_MODEL:19;
end;
then
A29: E,h |= All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) by ZF_MODEL:16;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
hence
E,g |= Ex(x2,All(x3,x3 'in' x2 <=> x3 '=' x0 'or' x3 '=' x1) ) by A29,
ZF_MODEL:20;
end;
hence thesis by ZF_MODEL:21;
end;
theorem
E is epsilon-transitive implies (E |= the_axiom_of_pairs iff for X,Y
st X in E & Y in E holds { X,Y } in E)
proof
assume
A1: E is epsilon-transitive;
hence E |= the_axiom_of_pairs implies for X,Y st X in E & Y in E holds { X,Y
} in E by Th2;
assume for X,Y st X in E & Y in E holds { X,Y } in E;
then for u,v holds { u,v } in E;
hence thesis by A1,Th2;
end;
theorem Th4:
E is epsilon-transitive implies (E |= the_axiom_of_unions iff for
u holds union u in E)
proof
assume
A1: X in E implies X c= E;
thus E |= the_axiom_of_unions implies for u holds union u in E
proof
set f0 = the Function of VAR,E;
assume
A2: E |= the_axiom_of_unions;
let u;
set f = f0+*(x0,u);
E |= Ex(x1,All(x2,x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) ))
by A2,ZF_MODEL:23;
then
E,f |= Ex(x1,All(x2,x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0 ) )
);
then consider g such that
A3: for x st g.x <> f.x holds x1 = x and
A4: E,g |= All(x2,x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) ) by
ZF_MODEL:20;
A5: f.x0= u by FUNCT_7:128;
for a be object holds a in g.x1 iff ex X st a in X & X in u
proof
let a be object;
A6: g.x0 = f.x0 by A3;
thus a in g.x1 implies ex X st a in X & X in u
proof
assume
A7: a in g.x1;
g.x1 c= E by A1;
then reconsider a9 = a as Element of E by A7;
set h = g+*(x2,a9);
A8: h.x2= a9 by FUNCT_7:128;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
then
A9: E,h |= x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) by A4,
ZF_MODEL:16;
h.x1 = g.x1 by FUNCT_7:32;
then E,h |= x2 'in' x1 by A7,A8,ZF_MODEL:13;
then E,h |= Ex(x3,x2 'in' x3 '&' x3 'in' x0) by A9,ZF_MODEL:19;
then consider m being Function of VAR,E such that
A10: for x st m.x <> h.x holds x3 = x and
A11: E,m |= x2 'in' x3 '&' x3 'in' x0 by ZF_MODEL:20;
A12: m.x0 = h.x0 & m.x2 = h.x2 by A10;
reconsider X = m.x3 as set;
take X;
A13: h.x0 = g.x0 & g.x0 = f.x0 by A3,FUNCT_7:32;
E,m |= x2 'in' x3 & E,m |= x3 'in' x0 by A11,ZF_MODEL:15;
hence thesis by A5,A8,A13,A12,ZF_MODEL:13;
end;
given X such that
A14: a in X and
A15: X in u;
u c= E by A1;
then reconsider X as Element of E by A15;
X c= E by A1;
then reconsider a9 = a as Element of E by A14;
set h = g+*(x2,a9);
set m = h+*(x3,X);
A16: m.x3= X by FUNCT_7:128;
m.x0 = h.x0 & h.x0 = g.x0 by FUNCT_7:32;
then
A17: E,m |= x3 'in' x0 by A5,A15,A16,A6,ZF_MODEL:13;
A18: h.x2= a9 by FUNCT_7:128;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
then
A19: E,h |= x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) by A4,ZF_MODEL:16;
m.x2 = h.x2 by FUNCT_7:32;
then E,m |= x2 'in' x3 by A14,A18,A16,ZF_MODEL:13;
then ( for x st m.x <> h.x holds x3 = x)& E,m |= x2 'in' x3 '&' x3 'in'
x0 by A17,FUNCT_7:32,ZF_MODEL:15;
then E,h |= Ex(x3,x2 'in' x3 '&' x3 'in' x0) by ZF_MODEL:20;
then E,h |= x2 'in' x1 by A19,ZF_MODEL:19;
then h.x2 in h.x1 by ZF_MODEL:13;
hence thesis by A18,FUNCT_7:32;
end;
then g.x1 = union u by TARSKI:def 4;
hence thesis;
end;
assume
A20: for u holds union u in E;
now
let f;
reconsider v = union(f.x0) as Element of E by A20;
set g = f+*(x1,v);
A21: g.x1= v by FUNCT_7:128;
now
let h;
assume
A22: for x st h.x <> g.x holds x2 = x;
then
A23: h.x1 = g.x1;
E,h |= x2 'in' x1 iff E,h |= Ex(x3,x2 'in' x3 '&' x3 'in' x0)
proof
thus E,h |= x2 'in' x1 implies E,h |= Ex(x3,x2 'in' x3 '&' x3 'in' x0)
proof
assume E,h |= x2 'in' x1;
then h.x2 in h.x1 by ZF_MODEL:13;
then consider X such that
A24: h.x2 in X and
A25: X in f.x0 by A21,A23,TARSKI:def 4;
f.x0 c= E by A1;
then reconsider X as Element of E by A25;
set m = h+*(x3,X);
A26: m.x3= X by FUNCT_7:128;
A27: g.x0 = f.x0 by FUNCT_7:32;
m.x2 = h.x2 by FUNCT_7:32;
then
A28: E,m |= x2 'in' x3 by A24,A26,ZF_MODEL:13;
m.x0 = h.x0 & h.x0 = g.x0 by A22,FUNCT_7:32;
then E,m |= x3 'in' x0 by A25,A26,A27,ZF_MODEL:13;
then ( for x st m.x <> h.x holds x3 = x)& E,m |= x2 'in' x3 '&' x3
'in' x0 by A28,FUNCT_7:32,ZF_MODEL:15;
hence thesis by ZF_MODEL:20;
end;
assume E,h |= Ex(x3,x2 'in' x3 '&' x3 'in' x0);
then consider m being Function of VAR,E such that
A29: for x st m.x <> h.x holds x3 = x and
A30: E,m |= x2 'in' x3 '&' x3 'in' x0 by ZF_MODEL:20;
E,m |= x3 'in' x0 by A30,ZF_MODEL:15;
then
A31: m.x3 in m.x0 by ZF_MODEL:13;
E,m |= x2 'in' x3 by A30,ZF_MODEL:15;
then m.x2 in m.x3 by ZF_MODEL:13;
then
A32: m.x2 in union(m.x0) by A31,TARSKI:def 4;
A33: h.x1 = g.x1 by A22;
A34: h.x0 = g.x0 & g.x0 = f.x0 by A22,FUNCT_7:32;
m.x2 = h.x2 & m.x0 = h.x0 by A29;
hence thesis by A21,A32,A34,A33,ZF_MODEL:13;
end;
hence E,h |= x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) by
ZF_MODEL:19;
end;
then
( for x st g.x <> f.x holds x1 = x)& E,g |= All(x2,x2 'in' x1 <=> Ex(
x3,x2 'in' x3 '&' x3 'in' x0) ) by FUNCT_7:32,ZF_MODEL:16;
hence
E,f |= Ex(x1,All(x2,x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) )
) by ZF_MODEL:20;
end;
then
E |= Ex(x1,All(x2,x2 'in' x1 <=> Ex(x3,x2 'in' x3 '&' x3 'in' x0) ));
hence thesis by ZF_MODEL:23;
end;
theorem
E is epsilon-transitive implies (E |= the_axiom_of_unions iff for X st
X in E holds union X in E)
proof
assume
A1: E is epsilon-transitive;
hence E |= the_axiom_of_unions implies for X st X in E holds union X in E by
Th4;
assume for X st X in E holds union X in E;
then for u holds union u in E;
hence thesis by A1,Th4;
end;
theorem Th6:
E is epsilon-transitive implies (E |= the_axiom_of_infinity iff
ex u st u <> {} & for v st v in u ex w st v c< w & w in u)
proof
assume
A1: X in E implies X c= E;
thus E |= the_axiom_of_infinity implies ex u st u <> {} & for v st v in u ex
w st v c< w & w in u
proof
set f = the Function of VAR,E;
assume E,g |= the_axiom_of_infinity;
then E,f |= the_axiom_of_infinity;
then consider g such that
for x st g.x <> f.x holds x0 = x or x1 = x and
A2: E,g |= x1 'in' x0 '&' All(x2,x2 'in' x0 => Ex(x3,x3 'in' x0 '&'
'not' x3 '=' x2 '&' All(x4,x4 'in' x2 => x4 'in' x3) )) by ZF_MODEL:22;
take u = g.x0;
E,g |= x1 'in' x0 by A2,ZF_MODEL:15;
hence u <> {} by ZF_MODEL:13;
let v such that
A3: v in u;
set h = g+*(x2,v);
( for x st h.x <> g.x holds x2 = x)& E,g |= All(x2,x2 'in' x0 => Ex(
x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2 => x4 'in' x3) )) by A2
,FUNCT_7:32,ZF_MODEL:15;
then
A4: E,h |= x2 'in' x0 => Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,
x4 'in' x2 => x4 'in' x3) ) by ZF_MODEL:16;
A5: h.x2= v by FUNCT_7:128;
h.x0 = g.x0 by FUNCT_7:32;
then E,h |= x2 'in' x0 by A3,A5,ZF_MODEL:13;
then E,h |= Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2 =>
x4 'in' x3) ) by A4,ZF_MODEL:18;
then consider f such that
A6: for x st f.x <> h.x holds x3 = x and
A7: E,f |= x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2 => x4
'in' x3) by ZF_MODEL:20;
A8: f.x0 = h.x0 by A6;
take w = f.x3;
A9: E,f |= All(x4,x4 'in' x2 => x4 'in' x3) by A7,ZF_MODEL:15;
thus v c= w
proof
let a be object such that
A10: a in v;
v c= E by A1;
then reconsider a9 = a as Element of E by A10;
set m = f+*(x4,a9);
A11: m.x4= a9 by FUNCT_7:128;
for x st m.x <> f.x holds x4 = x by FUNCT_7:32;
then
A12: E,m |= x4 'in' x2 => x4 'in' x3 by A9,ZF_MODEL:16;
m.x2 = f.x2 & f.x2 = h.x2 by A6,FUNCT_7:32;
then E,m |= x4 'in' x2 by A5,A10,A11,ZF_MODEL:13;
then E,m |= x4 'in' x3 by A12,ZF_MODEL:18;
then m.x4 in m.x3 by ZF_MODEL:13;
hence thesis by A11,FUNCT_7:32;
end;
A13: E,f |= x3 'in' x0 '&' 'not' x3 '=' x2 by A7,ZF_MODEL:15;
then E,f |= 'not' x3 '=' x2 by ZF_MODEL:15;
then not E,f |= x3 '=' x2 by ZF_MODEL:14;
then f.x3 <> f.x2 by ZF_MODEL:12;
hence v <> w by A5,A6;
A14: h.x0 = g.x0 by FUNCT_7:32;
E,f |= x3 'in' x0 by A13,ZF_MODEL:15;
hence thesis by A8,A14,ZF_MODEL:13;
end;
given u such that
A15: u <> {} and
A16: for v st v in u ex w st v c< w & w in u;
set a = the Element of u;
u c= E by A1;
then reconsider a as Element of E by A15;
let f0 be Function of VAR,E;
set f1 = f0+*(x0,u);
set f2 = f1+*(x1,a);
A17: f1.x0= u by FUNCT_7:128;
now
let f such that
A18: for x st f.x <> f2.x holds x2 = x;
now
assume E,f |= x2 'in' x0;
then
A19: f.x2 in f.x0 by ZF_MODEL:13;
f.x0 = f2.x0 & f2.x0 = f1.x0 by A18,FUNCT_7:32;
then consider w such that
A20: f.x2 c< w and
A21: w in u by A16,A17,A19;
set g = f+*(x3,w);
A22: g.x3= w by FUNCT_7:128;
A23: f.x2 c=w by A20;
now
let h such that
A24: for x st h.x <> g.x holds x4 = x;
now
assume E,h |= x4 'in' x2;
then
A25: h.x4 in h.x2 by ZF_MODEL:13;
A26: h.x3 = g.x3 by A24;
h.x2 = g.x2 & g.x2 = f.x2 by A24,FUNCT_7:32;
hence E,h |= x4 'in' x3 by A23,A22,A25,A26,ZF_MODEL:13;
end;
hence E,h |= x4 'in' x2 => x4 'in' x3 by ZF_MODEL:18;
end;
then
A27: E,g |= All(x4,x4 'in' x2 => x4 'in' x3) by ZF_MODEL:16;
A28: f2.x0 = f1.x0 by FUNCT_7:32;
g.x2 = f.x2 by FUNCT_7:32;
then not E,g |= x3 '=' x2 by A20,A22,ZF_MODEL:12;
then
A29: E,g |= 'not' x3 '=' x2 by ZF_MODEL:14;
g.x0 = f.x0 & f.x0 = f2.x0 by A18,FUNCT_7:32;
then E,g |= x3 'in' x0 by A17,A21,A22,A28,ZF_MODEL:13;
then E,g |= x3 'in' x0 '&' 'not' x3 '=' x2 by A29,ZF_MODEL:15;
then
( for x st g.x <> f.x holds x3 = x)& E,g |= x3 'in' x0 '&' 'not' x3
'=' x2 '&' All(x4,x4 'in' x2 => x4 'in' x3) by A27,FUNCT_7:32,ZF_MODEL:15;
hence E,f |= Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2
=> x4 'in' x3) ) by ZF_MODEL:20;
end;
hence
E,f |= x2 'in' x0 => Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,
x4 'in' x2 => x4 'in' x3) ) by ZF_MODEL:18;
end;
then
A30: E,f2 |= All(x2,x2 'in' x0 => Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&'
All(x4,x4 'in' x2 => x4 'in' x3) )) by ZF_MODEL:16;
f2.x1= a & f2.x0 = f1.x0 by FUNCT_7:32,128;
then E,f2 |= x1 'in' x0 by A15,A17,ZF_MODEL:13;
then
( for x st f2.x <> f1.x holds x1 = x)& E,f2 |= x1 'in' x0 '&' All(x2,x2
'in' x0 => Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2 => x4
'in' x3) )) by A30,FUNCT_7:32,ZF_MODEL:15;
then
( for x st f1.x <> f0.x holds x0 = x)& E,f1 |= Ex(x1,x1 'in' x0 '&' All
(x2,x2 'in' x0 => Ex(x3,x3 'in' x0 '&' 'not' x3 '=' x2 '&' All(x4,x4 'in' x2 =>
x4 'in' x3) ))) by FUNCT_7:32,ZF_MODEL:20;
hence thesis by ZF_MODEL:20;
end;
theorem
E is epsilon-transitive implies (E |= the_axiom_of_infinity iff ex X
st X in E & X <> {} & for Y st Y in X ex Z st Y c< Z & Z in X)
proof
assume
A1: E is epsilon-transitive;
thus E |= the_axiom_of_infinity implies ex X st X in E & X <> {} & for Y st
Y in X ex Z st Y c< Z & Z in X
proof
assume E |= the_axiom_of_infinity;
then consider u such that
A2: u <> {} and
A3: for v st v in u ex w st v c< w & w in u by A1,Th6;
reconsider X = u as set;
take X;
thus X in E & X <> {} by A2;
let Y such that
A4: Y in X;
X c= E by A1;
then reconsider v = Y as Element of E by A4;
consider w such that
A5: v c< w & w in u by A3,A4;
reconsider w as set;
take w;
thus thesis by A5;
end;
given X such that
A6: X in E and
A7: X <> {} and
A8: for Y st Y in X ex Z st Y c< Z & Z in X;
ex u st u <> {} & for v st v in u ex w st v c< w & w in u
proof
reconsider u = X as Element of E by A6;
take u;
thus u <> {} by A7;
let v;
assume v in u;
then consider Z such that
A9: v c< Z and
A10: Z in X by A8;
X c= E by A1,A6;
then reconsider w = Z as Element of E by A10;
take w;
thus thesis by A9,A10;
end;
hence thesis by A1,Th6;
end;
theorem Th8:
E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff
for u holds E /\ bool u in E)
proof
assume
A1: X in E implies X c= E;
thus E |= the_axiom_of_power_sets implies for u holds E /\ bool u in E
proof
set f0 = the Function of VAR,E;
assume
A2: E |= the_axiom_of_power_sets;
let u;
set f = f0+*(x0,u);
E |= Ex(x1,All(x2,x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) ))
by A2,ZF_MODEL:23;
then
E,f |= Ex(x1,All(x2,x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0 ) )
);
then consider g such that
A3: for x st g.x <> f.x holds x1 = x and
A4: E,g |= All(x2,x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) ) by
ZF_MODEL:20;
A5: f.x0= u by FUNCT_7:128;
g.x1 = E /\ bool u
proof
thus for a being object holds a in g.x1 implies a in E /\ bool u
proof let a be object;
assume
A6: a in g.x1;
g.x1 c= E by A1;
then reconsider a9 = a as Element of E by A6;
set h = g+*(x2,a9);
A7: h.x2= a9 by FUNCT_7:128;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
then
A8: E,h |= x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) by A4,
ZF_MODEL:16;
h.x1 = g.x1 by FUNCT_7:32;
then E,h |= x2 'in' x1 by A6,A7,ZF_MODEL:13;
then
A9: E,h |= All(x3,x3 'in' x2 => x3 'in' x0) by A8,ZF_MODEL:19;
a9 c= u
proof
let b be object such that
A10: b in a9;
a9 c= E by A1;
then reconsider b9 = b as Element of E by A10;
set m = h+*(x3,b9);
A11: m.x3= b9 by FUNCT_7:128;
for x st m.x <> h.x holds x3 = x by FUNCT_7:32;
then
A12: E,m |= x3 'in' x2 => x3 'in' x0 by A9,ZF_MODEL:16;
m.x2 = h.x2 by FUNCT_7:32;
then E,m |= x3 'in' x2 by A7,A10,A11,ZF_MODEL:13;
then
A13: E,m |= x3 'in' x0 by A12,ZF_MODEL:18;
A14: m.x0 = h.x0 & h.x0 = g.x0 by FUNCT_7:32;
g.x0 = f.x0 by A3;
hence thesis by A5,A11,A13,A14,ZF_MODEL:13;
end;
hence thesis by XBOOLE_0:def 4;
end;
let a be object;
assume
A15: a in E /\ bool u;
then
A16: a in bool u by XBOOLE_0:def 4;
reconsider a as Element of E by A15,XBOOLE_0:def 4;
set h = g+*(x2,a);
A17: h.x2= a by FUNCT_7:128;
now
let m be Function of VAR,E such that
A18: for x st m.x <> h.x holds x3 = x;
now
assume E,m |= x3 'in' x2;
then
A19: m.x3 in m.x2 by ZF_MODEL:13;
A20: h.x0 = g.x0 & g.x0 = f.x0 by A3,FUNCT_7:32;
m.x2 = h.x2 & m.x0 = h.x0 by A18;
hence E,m |= x3 'in' x0 by A5,A16,A17,A19,A20,ZF_MODEL:13;
end;
hence E,m |= x3 'in' x2 => x3 'in' x0 by ZF_MODEL:18;
end;
then
A21: E,h |= All(x3,x3 'in' x2 => x3 'in' x0) by ZF_MODEL:16;
A22: h.x1 = g.x1 by FUNCT_7:32;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
then E,h |= x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) by A4,
ZF_MODEL:16;
then E,h |= x2 'in' x1 by A21,ZF_MODEL:19;
hence thesis by A17,A22,ZF_MODEL:13;
end;
hence thesis;
end;
assume
A23: for u holds E /\ bool u in E;
E |= Ex(x1,All(x2,x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) ))
proof
let f;
reconsider v = E /\ bool(f.x0) as Element of E by A23;
set g = f+*(x1,v);
A24: g.x1= v by FUNCT_7:128;
now
let h such that
A25: for x st h.x <> g.x holds x2 = x;
now
thus E,h |= x2 'in' x1 implies E,h |= All(x3,x3 'in' x2 => x3 'in' x0)
proof
assume E,h |= x2 'in' x1;
then
A26: h.x2 in h.x1 by ZF_MODEL:13;
h.x1 = v by A24,A25;
then
A27: h.x2 in bool(f.x0) by A26,XBOOLE_0:def 4;
now
let m be Function of VAR,E such that
A28: for x st m.x <> h.x holds x3 = x;
now
assume E,m |= x3 'in' x2;
then
A29: m.x3 in m.x2 by ZF_MODEL:13;
A30: m.x2 = h.x2 & f.x0 = g.x0 by A28,FUNCT_7:32;
g.x0 = h.x0 & h.x0 = m.x0 by A25,A28;
hence E,m |= x3 'in' x0 by A27,A29,A30,ZF_MODEL:13;
end;
hence E,m |= x3 'in' x2 => x3 'in' x0 by ZF_MODEL:18;
end;
hence thesis by ZF_MODEL:16;
end;
assume
A31: E,h |= All(x3,x3 'in' x2 => x3 'in' x0);
A32: h.x2 c= f.x0
proof
let a be object such that
A33: a in h.x2;
h.x2 c= E by A1;
then reconsider a9 = a as Element of E by A33;
set m = h+*(x3,a9);
A34: m.x3= a9 by FUNCT_7:128;
for x st m.x <> h.x holds x3 = x by FUNCT_7:32;
then
A35: E,m |= x3 'in' x2 => x3 'in' x0 by A31,ZF_MODEL:16;
m.x2 = h.x2 by FUNCT_7:32;
then E,m |= x3 'in' x2 by A33,A34,ZF_MODEL:13;
then E,m |= x3 'in' x0 by A35,ZF_MODEL:18;
then
A36: m.x3 in m.x0 by ZF_MODEL:13;
m.x0 = h.x0 & g.x0 = f.x0 by FUNCT_7:32;
hence thesis by A25,A34,A36;
end;
h.x1 = g.x1 by A25;
then h.x2 in h.x1 by A24,A32,XBOOLE_0:def 4;
hence E,h |= x2 'in' x1 by ZF_MODEL:13;
end;
hence E,h |= x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) by
ZF_MODEL:19;
end;
then
A37: E,g |= All(x2,x2 'in' x1 <=> All(x3,x3 'in' x2 => x3 'in' x0) ) by
ZF_MODEL:16;
for x st g.x <> f.x holds x1 = x by FUNCT_7:32;
hence thesis by A37,ZF_MODEL:20;
end;
hence thesis by ZF_MODEL:23;
end;
theorem
E is epsilon-transitive implies (E |= the_axiom_of_power_sets iff for
X st X in E holds E /\ bool X in E)
proof
assume
A1: E is epsilon-transitive;
hence E |= the_axiom_of_power_sets implies for X st X in E holds E /\ bool X
in E by Th8;
assume for X st X in E holds E /\ bool X in E;
then for u holds E /\ bool u in E;
hence thesis by A1,Th8;
end;
defpred Lm2[Nat] means for x,E,H,f st len H = $1 & not x in Free H & E,f |= H
holds E,f |= All(x,H);
Lm1: for n being Nat st for k being Nat st k < n holds Lm2[k] holds Lm2[n]
proof
let n be Nat such that
A1: for k being Nat st k < n for x,E,H,f st len H = k & not x in Free H
& E,f |= H holds E,f |= All(x,H);
let x,E,H,f such that
A2: len H = n and
A3: not x in Free H and
A4: E,f |= H;
A5: now
assume
A6: H is being_equality;
then Free H = { Var1 H,Var2 H } by ZF_MODEL:1;
then
A7: x <> Var1 H & x <> Var2 H by A3,TARSKI:def 2;
A8: H = (Var1 H) '=' Var2 H by A6,ZF_LANG:36;
then
A9: f.(Var1 H) = f.(Var2 H) by A4,ZF_MODEL:12;
now
let g;
assume for y st g.y <> f.y holds x = y;
then g.(Var1 H) = f.(Var1 H) & g.(Var2 H) = f.(Var2 H) by A7;
hence E,g |= H by A8,A9,ZF_MODEL:12;
end;
hence thesis by ZF_MODEL:16;
end;
A10: now
assume
A11: H is universal;
then
A12: H = All(bound_in H,the_scope_of H) by ZF_LANG:44;
Free H = Free the_scope_of H \ { bound_in H } by A11,ZF_MODEL:1;
then
A13: not x in Free the_scope_of H or x in { bound_in H } by A3,XBOOLE_0:def 5;
A14: now
assume
A15: x <> bound_in H;
assume not thesis;
then consider g such that
A16: for y st g.y <> f.y holds x = y and
A17: not E,g |= H by ZF_MODEL:16;
consider h such that
A18: for y st h.y <> g.y holds bound_in H = y and
A19: not E,h |= the_scope_of H by A12,A17,ZF_MODEL:16;
set m = f+*(bound_in H,h.(bound_in H));
A20: now
let y;
assume
A21: h.y <> m.y;
assume x <> y;
then
A22: f.y = g.y by A16;
A23: y <> bound_in H by A21,FUNCT_7:128;
then m.y = f.y by FUNCT_7:32;
hence contradiction by A18,A21,A23,A22;
end;
the_scope_of H is_immediate_constituent_of H by A12;
then
A24: len the_scope_of H < len H by ZF_LANG:60;
for y st m.y <> f.y holds bound_in H = y by FUNCT_7:32;
then E,m |= the_scope_of H by A4,A12,ZF_MODEL:16;
then E,m |= All(x,the_scope_of H) by A1,A2,A13,A15,A24,TARSKI:def 1;
hence contradiction by A19,A20,ZF_MODEL:16;
end;
now
assume
A25: x = bound_in H;
now
let g;
assume for y st g.y <> f.y holds x = y or bound_in H = y;
then for y st g.y <> f.y holds bound_in H = y by A25;
hence E,g |= the_scope_of H by A4,A12,ZF_MODEL:16;
end;
then E,f |= All(x,bound_in H,the_scope_of H) by ZF_MODEL:21;
hence thesis by A11,ZF_LANG:44;
end;
hence thesis by A14;
end;
A26: now
assume
A27: H is conjunctive;
then
A28: H = (the_left_argument_of H) '&' the_right_argument_of H by ZF_LANG:40;
then the_right_argument_of H is_immediate_constituent_of H;
then
A29: len the_right_argument_of H < len H by ZF_LANG:60;
the_left_argument_of H is_immediate_constituent_of H by A28;
then
A30: len the_left_argument_of H < len H by ZF_LANG:60;
A31: Free H = Free the_left_argument_of H \/ Free the_right_argument_of H
by A27,ZF_MODEL:1;
then
A32: not x in Free the_left_argument_of H by A3,XBOOLE_0:def 3;
A33: not x in Free the_right_argument_of H by A3,A31,XBOOLE_0:def 3;
E,f |= the_right_argument_of H by A4,A28,ZF_MODEL:15;
then
A34: E,f |= All(x,the_right_argument_of H) by A1,A2,A33,A29;
E,f |= the_left_argument_of H by A4,A28,ZF_MODEL:15;
then
A35: E,f |= All(x,the_left_argument_of H) by A1,A2,A32,A30;
now
let g;
assume for y st g.y <> f.y holds x = y;
then E,g |= the_left_argument_of H & E,g |= the_right_argument_of H by
A35,A34,ZF_MODEL:16;
hence E,g |= H by A28,ZF_MODEL:15;
end;
hence thesis by ZF_MODEL:16;
end;
A36: now
assume
A37: H is being_membership;
then Free H = { Var1 H,Var2 H } by ZF_MODEL:1;
then
A38: x <> Var1 H & x <> Var2 H by A3,TARSKI:def 2;
A39: H = (Var1 H) 'in' Var2 H by A37,ZF_LANG:37;
then
A40: f.(Var1 H) in f.(Var2 H) by A4,ZF_MODEL:13;
now
let g;
assume for y st g.y <> f.y holds x = y;
then g.(Var1 H) = f.(Var1 H) & g.(Var2 H) = f.(Var2 H) by A38;
hence E,g |= H by A39,A40,ZF_MODEL:13;
end;
hence thesis by ZF_MODEL:16;
end;
now
assume
A41: H is negative;
then
A42: H = 'not' the_argument_of H by ZF_LANG:def 30;
then the_argument_of H is_immediate_constituent_of H;
then
A43: len the_argument_of H < len H by ZF_LANG:60;
A44: not x in Free the_argument_of H by A3,A41,ZF_MODEL:1;
assume not thesis;
then consider g such that
A45: for y st g.y <> f.y holds x = y and
A46: not E,g |= H by ZF_MODEL:16;
E,g |= the_argument_of H by A42,A46,ZF_MODEL:14;
then E,g |= All(x,the_argument_of H) by A1,A2,A43,A44;
then E,f |= the_argument_of H by A45,ZF_MODEL:16;
hence contradiction by A4,A42,ZF_MODEL:14;
end;
hence thesis by A5,A36,A26,A10,ZF_LANG:9;
end;
theorem Th10:
not x in Free H & E,f |= H implies E,f |= All(x,H)
proof
A1: len H = len H;
for n being Nat holds Lm2[n] from NAT_1:sch 4(Lm1);
hence thesis by A1;
end;
Lm2: the_scope_of All(x,H) = H & bound_in All(x,H) = x
proof
All(x,H) is universal;
then All(x,H) = All(bound_in All(x,H),the_scope_of All(x,H)) by ZF_LANG:44;
hence thesis by ZF_LANG:3;
end;
theorem Th11:
{ x,y } misses Free H & E,f |= H implies E,f |= All(x,y,H)
proof
assume that
A1: { x,y } misses Free H and
A2: E,f |= H;
A3: bound_in All(y,H) = y by Lm2;
All(y,H) is universal & the_scope_of All(y,H) = H by Lm2;
then
A4: Free All(y,H) = Free H \ { y } by A3,ZF_MODEL:1;
x in { x,y } by TARSKI:def 2;
then not x in Free H by A1,XBOOLE_0:3;
then
A5: not x in Free All(y,H) by A4,XBOOLE_0:def 5;
y in { x,y } by TARSKI:def 2;
then not y in Free H by A1,XBOOLE_0:3;
then E,f |= All(y,H) by A2,Th10;
hence thesis by A5,Th10;
end;
theorem
{ x,y,z } misses Free H & E,f |= H implies E,f |= All(x,y,z,H)
proof
assume that
A1: { x,y,z } misses Free H and
A2: E,f |= H;
A3: bound_in All(y,All(z,H)) = y by Lm2;
now
let a be object;
assume a in { y,z };
then a = y or a = z by TARSKI:def 2;
then a in { x,y,z } by ENUMSET1:def 1;
hence not a in Free H by A1,XBOOLE_0:3;
end;
then { y,z } misses Free H by XBOOLE_0:3;
then
A4: E,f |= All(y,z,H) by A2,Th11;
A5: All(z,H) is universal & the_scope_of All(z,H) = H by Lm2;
x in { x,y,z } by ENUMSET1:def 1;
then not x in Free H by A1,XBOOLE_0:3;
then not x in Free H \ { z } by XBOOLE_0:def 5;
then
A6: not x in (Free H \ { z }) \ { y } by XBOOLE_0:def 5;
A7: bound_in All(z,H)= z by Lm2;
All(y,All(z,H)) is universal & the_scope_of All(y,All(z,H)) = All(z,H)
by Lm2;
then Free All(y,z,H) = Free All(z,H) \ { y } by A3,ZF_MODEL:1
.= (Free H \ { z }) \ { y } by A5,A7,ZF_MODEL:1;
hence thesis by A4,A6,Th10;
end;
definition
let H,E;
let val be Function of VAR,E;
assume that
A1: not x.0 in Free H and
A2: E,val |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func'(H,val) -> Function of E,E means
:Def1:
for g st for y st g.y
<> val.y holds x.0 = y or x.3 = y or x.4 = y holds E,g |= H iff it.(g.x.3) = g.
x.4;
existence
proof
defpred Like[Function of VAR,E] means for y st $1.y <> val.y holds x0 = y
or x3 = y or x4 = y;
defpred P[object] means
for g st Like[g] & g.x3 = $1`1 & g.x4 = $1`2 holds E,
g |= H;
consider X such that
A3: for a being object holds a in X iff a in [:E,E:] & P[a]
from XBOOLE_0:sch 1;
X is Relation-like Function-like
proof
thus for a being object holds a in X implies
ex b,c being object st [b,c] = a
by A3,RELAT_1:def 1;
let a,b,c be object;
assume that
A4: [a,b] in X and
A5: [a,c] in X;
[a,b] in [:E,E:] & [a,c] in [:E,E:] by A3,A4,A5;
then reconsider a9 = a, b9 = b, c9 = c as Element of E by ZFMISC_1:87;
set f = val+*(x3,a9);
for x st f.x <> val.x holds x = x3 by FUNCT_7:32;
then E,f |= Ex(x0,All(x4,H <=> x4 '=' x0)) by A2,ZF_MODEL:16;
then consider g such that
A6: for x st g.x <> f.x holds x0 = x and
A7: E,g |= All(x4,H <=> x4 '=' x0) by ZF_MODEL:20;
A8: f.x3 = a9 & g.x3 = f.x3 by A6,FUNCT_7:128;
set g1 = g+*(x4,b9);
A9: g1.x4 = b9 by FUNCT_7:128;
A10: Like[g1]
proof
let y;
assume
A11: g1.y <> val.y;
assume that
A12: x0 <> y and
A13: x3 <> y & x4 <> y;
f.y = val.y & g1.y = g.y by A13,FUNCT_7:32;
hence contradiction by A6,A11,A12;
end;
for x st g1.x <> g.x holds x4 = x by FUNCT_7:32;
then
A14: E,g1 |= H <=> x4 '=' x0 by A7,ZF_MODEL:16;
A15: g1.x3 = g. x3 by FUNCT_7:32;
[a,b]`1 = a9 & [a,b]`2 = b9;
then E,g1 |= H by A3,A4,A9,A15,A8,A10;
then E,g1 |= x4 '=' x0 by A14,ZF_MODEL:19;
then
A16: g1.x4 = g1.x0 by ZF_MODEL:12;
set g2 = g+*(x4,c9);
A17: g2.x4 = c9 by FUNCT_7:128;
A18: Like[g2]
proof
let y;
assume
A19: g2.y <> val.y;
assume that
A20: x0 <> y and
A21: x3 <> y & x4 <> y;
f.y = val.y & g2.y = g.y by A21,FUNCT_7:32;
hence contradiction by A6,A19,A20;
end;
for x st g2.x <> g.x holds x4 = x by FUNCT_7:32;
then
A22: E,g2 |= H <=> x4 '=' x0 by A7,ZF_MODEL:16;
A23: g2.x3 = g.x3 by FUNCT_7:32;
[a,c]`1 = a9 & [a,c]`2 = c9;
then E,g2 |= H by A3,A5,A17,A23,A8,A18;
then
A24: E,g2 |= x4 '=' x0 by A22,ZF_MODEL:19;
g1.x0 = g.x0 & g2.x0 = g.x0 by FUNCT_7:32;
hence thesis by A9,A17,A24,A16,ZF_MODEL:12;
end;
then reconsider F = X as Function;
A25: rng F c= E
proof
let b be object;
assume b in rng F;
then consider a being object such that
A26: a in dom F & b = F.a by FUNCT_1:def 3;
[a,b] in F by A26,FUNCT_1:1;
then [a,b] in [:E,E:] by A3;
hence thesis by ZFMISC_1:87;
end;
A27: E c= dom F
proof
let a be object;
assume a in E;
then reconsider a9 = a as Element of E;
set g = val+*(x3,a9);
for x st g.x <> val.x holds x = x3 by FUNCT_7:32;
then E,g |= Ex(x0,All(x4,H <=> x4 '=' x0)) by A2,ZF_MODEL:16;
then consider h such that
A28: for x st h.x <> g.x holds x = x0 and
A29: E,h |= All(x4,H <=> x4 '=' x0) by ZF_MODEL:20;
set u = h.x0;
A30: g.x3 = a9 by FUNCT_7:128;
A31: now
set m = h+*(x4,u);
let f such that
A32: Like[f] and
A33: f.x3 = [a9,u]`1 and
A34: f.x4 = [a9,u]`2;
A35: m.x4 = u by FUNCT_7:128;
A36: now
let x such that
A37: f.x <> m.x;
A38: x <> x4 by A34,A35,A37;
then
A39: m.x = h.x by FUNCT_7:32;
g.x3 = h.x3 & h.x3 = m.x3 by A28,FUNCT_7:32;
then
A40: x <> x3 by A30,A33,A37;
then
A41: g.x = val.x by FUNCT_7:32;
assume
A42: x0 <> x;
then f.x = val.x by A32,A38,A40;
hence contradiction by A28,A37,A42,A41,A39;
end;
for x st m.x <> h.x holds x4 = x by FUNCT_7:32;
then
A43: E,m |= H <=> x4 '=' x0 by A29,ZF_MODEL:16;
m.x0 = h.x0 by FUNCT_7:32;
then E,m |= x4 '=' x0 by A35,ZF_MODEL:12;
then E,m |= H by A43,ZF_MODEL:19;
then E,m |= All(x0,H) by A1,Th10;
hence E,f |= H by A36,ZF_MODEL:16;
end;
[a9,u] in [:E,E:] by ZFMISC_1:87;
then [a9,u] in X by A3,A31;
hence thesis by FUNCT_1:1;
end;
dom F c= E
proof
let a be object;
assume a in dom F;
then consider b being object such that
A44: [a,b] in F by XTUPLE_0:def 12;
[a,b] in [:E,E:] by A3,A44;
hence thesis by ZFMISC_1:87;
end;
then E = dom F by A27;
then reconsider F as Function of E,E by A25,FUNCT_2:def 1,RELSET_1:4;
take F;
let f such that
A45: for y st f.y <> val.y holds x.0 = y or x.3 = y or x.4 = y;
thus E,f |= H implies F.(f.x.3) = f.x.4
proof
assume E,f |= H;
then
A46: E,f |= All(x0,H) by A1,Th10;
A47: now
let g such that
A48: Like[g] and
A49: g.x3 = [f.x3,f.x4]`1 & g.x4 = [f.x3,f.x4]`2;
now
let x;
assume that
A50: g.x <> f.x and
A51: x0 <> x;
A52: x <> x3 & x <> x4 by A49,A50;
then f.x = val.x by A45,A51;
hence contradiction by A48,A50,A51,A52;
end;
hence E,g |= H by A46,ZF_MODEL:16;
end;
[f.x3,f.x4] in [:E,E:] by ZFMISC_1:87;
then [f.x3,f.x4] in X by A3,A47;
hence thesis by FUNCT_1:1;
end;
A53: [f.x3,f.x4]`1 = f.x3 & [f.x3,f.x4]`2 = f.x4;
A54: dom F = E by FUNCT_2:def 1;
assume F.(f.x.3) = f.x.4;
then [f.x3,f.x4] in F by A54,FUNCT_1:1;
hence thesis by A3,A45,A53;
end;
uniqueness
proof
let F1,F2 be Function of E,E;
assume that
A55: for g st for y st g.y <> val.y holds x.0 = y or x.3 = y or x.4 =
y holds E,g |= H iff F1.(g.x.3) = g.x.4 and
A56: for g st for y st g.y <> val.y holds x.0 = y or x.3 = y or x.4 =
y holds E,g |= H iff F2.(g.x.3) = g.x.4;
let a be Element of E;
set f = val+*(x3,a);
for x st f.x <> val.x holds x3 = x by FUNCT_7:32;
then E,f |= Ex(x0,All(x4,H <=> x4 '=' x0)) by A2,ZF_MODEL:16;
then consider g such that
A57: for x st g.x <> f.x holds x0 = x and
A58: E,g |= All(x4,H <=> x4 '=' x0) by ZF_MODEL:20;
A59: g.x3 = f.x3 by A57;
set h = g+*(x4,g.x0);
A60: now
let x;
assume that
A61: h.x <> val.x & x.0 <> x and
A62: x.3 <> x & x.4 <> x;
f.x = val.x & h.x = g.x by A62,FUNCT_7:32;
hence contradiction by A57,A61;
end;
h.x4 = g.x0 & h.x0 = g.x0 by FUNCT_7:32,128;
then
A63: E,h |= x4 '=' x0 by ZF_MODEL:12;
A64: f.x3 = a & h.x3 = g.x3 by FUNCT_7:32,128;
for x st h.x <> g.x holds x4 = x by FUNCT_7:32;
then E,h |= H <=> x4 '=' x0 by A58,ZF_MODEL:16;
then
A65: E,h |= H by A63,ZF_MODEL:19;
then F1.(h.x.3) = h.x.4 by A55,A60;
hence F1.a = F2.a by A56,A65,A60,A64,A59;
end;
end;
theorem Th13:
for H,f,g st (for x st f.x <> g.x holds not x in Free H) & E,f
|= H holds E,g |= H
proof
defpred Th[ZF-formula] means for f,g st (for x st f.x <> g.x holds not x in
Free $1) & E,f |= $1 holds E,g |= $1;
A1: for H st H is atomic holds Th[H]
proof
let H such that
A2: H is being_equality or H is being_membership;
let f,g such that
A3: for x st f.x <> g.x holds not x in Free H and
A4: E,f |= H;
A5: now
assume
A6: H is being_membership;
then
A7: Free H = { Var1 H,Var2 H } by ZF_MODEL:1;
then Var1 H in Free H by TARSKI:def 2;
then
A8: f.(Var1 H) = g.(Var1 H) by A3;
Var2 H in Free H by A7,TARSKI:def 2;
then
A9: f.(Var2 H) = g.(Var2 H) by A3;
A10: H = (Var1 H) 'in' Var2 H by A6,ZF_LANG:37;
then f.(Var1 H) in f.(Var2 H) by A4,ZF_MODEL:13;
hence thesis by A10,A8,A9,ZF_MODEL:13;
end;
now
assume
A11: H is being_equality;
then
A12: Free H = { Var1 H,Var2 H } by ZF_MODEL:1;
then Var1 H in Free H by TARSKI:def 2;
then
A13: f.(Var1 H) = g.(Var1 H) by A3;
Var2 H in Free H by A12,TARSKI:def 2;
then
A14: f.(Var2 H) = g.(Var2 H) by A3;
A15: H = (Var1 H) '=' Var2 H by A11,ZF_LANG:36;
then f.(Var1 H) = f.(Var2 H) by A4,ZF_MODEL:12;
hence thesis by A15,A13,A14,ZF_MODEL:12;
end;
hence thesis by A2,A5;
end;
A16: for H st H is conjunctive & Th[the_left_argument_of H] & Th[
the_right_argument_of H] holds Th[H]
proof
let H;
assume
A17: H is conjunctive;
then
A18: H = (the_left_argument_of H) '&' the_right_argument_of H by ZF_LANG:40;
assume that
A19: for f,g st (for x st f.x <> g.x holds not x in Free
the_left_argument_of H)& E,f |= the_left_argument_of H holds E,g |=
the_left_argument_of H and
A20: for f,g st (for x st f.x <> g.x holds not x in Free
the_right_argument_of H)& E,f |= the_right_argument_of H holds E,g |=
the_right_argument_of H;
let f,g such that
A21: for x st f.x <> g.x holds not x in Free H and
A22: E,f |= H;
A23: Free H = Free the_left_argument_of H \/ Free the_right_argument_of H
by A17,ZF_MODEL:1;
A24: now
let x;
assume f.x <> g.x;
then not x in Free H by A21;
hence not x in Free the_right_argument_of H by A23,XBOOLE_0:def 3;
end;
A25: now
let x;
assume f.x <> g.x;
then not x in Free H by A21;
hence not x in Free the_left_argument_of H by A23,XBOOLE_0:def 3;
end;
E,f |= the_right_argument_of H by A18,A22,ZF_MODEL:15;
then
A26: E,g |= the_right_argument_of H by A20,A24;
E,f |= the_left_argument_of H by A18,A22,ZF_MODEL:15;
then E,g |= the_left_argument_of H by A19,A25;
hence thesis by A18,A26,ZF_MODEL:15;
end;
A27: for H st H is universal & Th[the_scope_of H] holds Th[H]
proof
let H;
assume
A28: H is universal;
then
A29: H = All(bound_in H,the_scope_of H) by ZF_LANG:44;
assume
A30: for f,g st (for x st f.x <> g.x holds not x in Free the_scope_of
H)& E,f |= the_scope_of H holds E,g |= the_scope_of H;
let f,g such that
A31: for x st f.x <> g.x holds not x in Free H and
A32: E,f |= H;
A33: Free H = Free the_scope_of H \ { bound_in H } by A28,ZF_MODEL:1;
now
let j such that
A34: for x st j.x <> g.x holds bound_in H = x;
set h = f+*(bound_in H,j.(bound_in H));
A35: now
let x;
assume
A36: h.x <> j.x;
then
A37: x <> bound_in H by FUNCT_7:128;
then h.x = f.x & j.x = g.x by A34,FUNCT_7:32;
then
A38: not x in Free H by A31,A36;
not x in { bound_in H } by A37,TARSKI:def 1;
hence not x in Free the_scope_of H by A33,A38,XBOOLE_0:def 5;
end;
for x st h.x <> f.x holds bound_in H = x by FUNCT_7:32;
then E,h |= the_scope_of H by A29,A32,ZF_MODEL:16;
hence E,j |= the_scope_of H by A30,A35;
end;
hence thesis by A29,ZF_MODEL:16;
end;
A39: for H st H is negative & Th[the_argument_of H] holds Th[H]
proof
let H;
assume
A40: H is negative;
then
A41: Free H = Free the_argument_of H by ZF_MODEL:1;
assume
A42: for f,g st (for x st f.x <> g.x holds not x in Free
the_argument_of H)& E,f |= the_argument_of H holds E,g |= the_argument_of H;
let f,g such that
A43: for x st f.x <> g.x holds not x in Free H and
A44: E,f |= H and
A45: not E,g |= H;
A46: H = 'not' the_argument_of H by A40,ZF_LANG:def 30;
then E,g |= the_argument_of H by A45,ZF_MODEL:14;
then E,f |= the_argument_of H by A41,A42,A43;
hence thesis by A46,A44,ZF_MODEL:14;
end;
thus for H holds Th[H] from ZF_LANG:sch 1(A1,A39,A16,A27);
end;
definition
let H,E;
assume that
A1: Free H c= { x.3,x.4 } and
A2: E |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func(H,E) -> Function of E,E means
:Def2:
for g holds E,g |= H iff it.(g.x.3) = g.x.4;
existence
proof
set f = the Function of VAR,E;
take F = def_func'(H,f);
let g;
set j = f+*(x3,g.x3);
set h = j+*(x4,g.x4);
A3: now
let x such that
A4: h.x <> f.x and
x.0 <> x and
A5: x.3 <> x and
A6: x.4 <> x;
h.x = j.x by A6,FUNCT_7:32
.= f.x by A5,FUNCT_7:32;
hence contradiction by A4;
end;
A7: ( not x0 in Free H)& E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))
) by A1,A2,TARSKI:def 2;
thus E,g |= H implies F.(g.x.3) = g.x.4
proof
set g3 = f+*(x3,g.x3);
set g4 = g3+*(x4,g.x4);
A8: now
let x such that
A9: g4.x <> f.x and
x.0 <> x and
A10: x.3 <> x and
A11: x.4 <> x;
g4.x = g3.x by A11,FUNCT_7:32
.= f.x by A10,FUNCT_7:32;
hence contradiction by A9;
end;
A12: g3.x3 = g.x3 by FUNCT_7:128;
A13: now
let x;
assume g.x <> g4.x;
then x4 <> x & x3 <> x by A12,FUNCT_7:32,128;
hence not x in Free H by A1,TARSKI:def 2;
end;
assume E,g |= H;
then E,g4 |= H by A13,Th13;
then g4.x4 = g.x4 & F.(g4.x.3) = g4.x.4 by A7,A8,Def1,FUNCT_7:128;
hence thesis by A12,FUNCT_7:32;
end;
assume that
A14: F.(g.x.3) = g.x.4 and
A15: not E,g |= H;
A16: j.x3 = g.x3 by FUNCT_7:128;
now
let x;
assume h.x <> g.x;
then x4 <> x & x3 <> x by A16,FUNCT_7:32,128;
hence not x in Free H by A1,TARSKI:def 2;
end;
then not E,h |= H by A15,Th13;
then h.x4 = g.x4 & F.(h.x.3) <> h.x.4 by A7,A3,Def1,FUNCT_7:128;
hence contradiction by A14,A16,FUNCT_7:32;
end;
uniqueness
proof
set f = the Function of VAR,E;
let F1,F2 be Function of E,E such that
A17: for g holds E,g |= H iff F1.(g.x.3) = g.x.4 and
A18: for g holds E,g |= H iff F2.(g.x.3) = g.x.4;
let a be Element of E;
set g = f+*(x3,a);
E |= Ex(x0,All(x4,H <=> x4 '=' x0)) by A2,ZF_MODEL:23;
then E,g |= Ex(x0,All(x4,H <=> x4 '=' x0));
then consider h such that
A19: for x st h.x <> g.x holds x0 = x and
A20: E,h |= All(x4,H <=> x4 '=' x0) by ZF_MODEL:20;
A21: h.x3 = g.x3 by A19;
set j = h+*(x4,h.x0);
A22: g.x3 = a & j.x3 = h.x3 by FUNCT_7:32,128;
j.x4 = h.x0 & j.x0 = h.x0 by FUNCT_7:32,128;
then
A23: E,j |= x4 '=' x0 by ZF_MODEL:12;
for x st j.x <> h.x holds x4 = x by FUNCT_7:32;
then E,j |= H <=> x4 '=' x0 by A20,ZF_MODEL:16;
then
A24: E,j |= H by A23,ZF_MODEL:19;
then F1.(j.x3) = j.x4 by A17;
hence F1.a = F2.a by A18,A24,A22,A21;
end;
end;
definition
let F be Function;
let E;
pred F is_definable_in E means
ex H st Free H c= { x.3,x.4 } & E |= All(x.3,
Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & F = def_func(H,E);
pred F is_parametrically_definable_in E means
:Def4:
ex H,f st { x.0,x.1,x.2
} misses Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & F =
def_func'(H,f);
end;
theorem
for F being Function st F is_definable_in E holds F
is_parametrically_definable_in E
proof
set f = the Function of VAR,E;
let F be Function;
given H such that
A1: Free H c= { x.3,x.4 } and
A2: E |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) and
A3: F = def_func(H,E);
take H,f;
A4: now
let a be object;
assume a in { x.0,x.1,x.2 };
then a <> x3 & a <> x4 by ENUMSET1:def 1;
hence not a in Free H by A1,TARSKI:def 2;
end;
hence { x.0,x.1,x.2 } misses Free H by XBOOLE_0:3;
thus
A5: E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) by A2;
reconsider F1 = F as Function of E,E by A3;
A6: now
assume x.0 in Free H;
then not x.0 in { x.0,x.1,x.2 } by A4;
hence contradiction by ENUMSET1:def 1;
end;
for g st for y st g.y <> f.y holds x.0 = y or x.3 = y or x.4 = y holds
E,g |= H iff F1.(g.x.3) = g.x.4 by A1,A2,A3,Def2;
hence thesis by A6,A5,Def1;
end;
theorem Th15:
E is epsilon-transitive implies ((for H st { x.0,x.1,x.2 }
misses Free H holds E |= the_axiom_of_substitution_for H) iff for H,f st { x.0,
x.1,x.2 } misses Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in E )
proof
assume
A1: X in E implies X c= E;
A2: now
assume
A3: for H st { x.0,x.1,x.2 } misses Free H holds E |=
the_axiom_of_substitution_for H;
let H,f;
assume that
A4: { x.0,x.1,x.2 } misses Free H and
A5: E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
E |= the_axiom_of_substitution_for H by A3,A4;
then E,f |= the_axiom_of_substitution_for H;
then
A6: E,f |= All(x1,Ex(x2, All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H) )
)) by A5,ZF_MODEL:18;
let u;
set g = f+*(x1,u);
x0 in { x0,x1,x2 } by ENUMSET1:def 1;
then
A7: not x0 in Free H by A4,XBOOLE_0:3;
now
let a be object;
assume a in { x1,x2 };
then a = x1 or a = x2 by TARSKI:def 2;
then a in { x0,x1,x2 } by ENUMSET1:def 1;
hence not a in Free H by A4,XBOOLE_0:3;
end;
then
A8: { x1,x2 } misses Free H by XBOOLE_0:3;
for x st g.x <> f.x holds x1 = x by FUNCT_7:32;
then E,g |= Ex(x2,All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H))) by A6,
ZF_MODEL:16;
then consider h such that
A9: for x st h.x <> g.x holds x2 = x and
A10: E,h |= All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H)) by ZF_MODEL:20;
set v = h.x2;
A11: g.x1 = u by FUNCT_7:128;
A12: def_func'(H,f).:u c= v
proof
let a be object;
assume
A13: a in def_func'(H,f).:u;
then consider b being object such that
A14: b in dom def_func'(H,f) and
A15: b in u and
A16: def_func'(H,f).b = a by FUNCT_1:def 6;
reconsider b as Element of E by A14;
reconsider e = a as Element of E by A13;
set i = h+*(x4,e);
set j = i+*(x3,b);
A17: j.x3 = b by FUNCT_7:128;
A18: h.x1 = g.x1 by A9;
j.x1 = i.x1 & i.x1 = h.x1 by FUNCT_7:32;
then
A19: E,j |= x3 'in' x1 by A11,A15,A17,A18,ZF_MODEL:13;
set m1 = f+*(x3,b);
A20: i.x4 = e by FUNCT_7:128;
set m = m1+*(x4,e);
A21: m1.x3 = b by FUNCT_7:128;
set k = m+*(x1,j.x1);
A22: m.x4 = e by FUNCT_7:128;
A23: m.x3 = m1.x3 by FUNCT_7:32;
A24: now
let x;
assume that
A25: j.x <> k.x and
A26: x2 <> x;
A27: x <> x3 by A17,A21,A23,A25,FUNCT_7:32;
k.x4 = m.x4 by FUNCT_7:32;
then
A28: x <> x4 by A20,A22,A25,FUNCT_7:32;
A29: x <> x1 by A25,FUNCT_7:128;
then k.x = m.x by FUNCT_7:32
.= m1.x by A28,FUNCT_7:32
.= f.x by A27,FUNCT_7:32
.= g.x by A29,FUNCT_7:32
.= h.x by A9,A26
.= i.x by A28,FUNCT_7:32
.= j.x by A27,FUNCT_7:32;
hence contradiction by A25;
end;
A30: for x st k.x <> m.x holds x1 = x by FUNCT_7:32;
now
let y;
assume
A31: m.y <> f.y;
assume that
x.0 <> y and
A32: x.3 <> y and
A33: x.4 <> y;
m.y = m1.y by A33,FUNCT_7:32;
hence contradiction by A31,A32,FUNCT_7:32;
end;
then E,m |= H iff def_func'(H,f).(m.x.3) = m.x.4 by A5,A7,Def1;
then E,m |= All(x1,x2,H) by A8,A16,A21,A22,Th11,FUNCT_7:32;
then E,k |= All(x2,H) by A30,ZF_MODEL:16;
then E,j |= H by A24,ZF_MODEL:16;
then
A34: E,j |= x3 'in' x1 '&' H by A19,ZF_MODEL:15;
for x st i.x <> h.x holds x4 = x by FUNCT_7:32;
then
A35: E,i |= x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H) by A10,ZF_MODEL:16;
A36: i.x2 = h.x2 by FUNCT_7:32;
for x st i.x <> j.x holds x3 = x by FUNCT_7:32;
then E,i |= Ex(x3,x3 'in' x1 '&' H) by A34,ZF_MODEL:20;
then E,i |= x4 'in' x2 by A35,ZF_MODEL:19;
hence thesis by A20,A36,ZF_MODEL:13;
end;
v c= def_func'(H,f).:u
proof
let a be object such that
A37: a in v;
v c= E by A1;
then reconsider e = a as Element of E by A37;
set i = h+*(x4,e);
A38: i.x4 = e by FUNCT_7:128;
for x st i.x <> h.x holds x4 = x by FUNCT_7:32;
then
A39: E,i |= x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H) by A10,ZF_MODEL:16;
i.x2 = h.x2 by FUNCT_7:32;
then E,i |= x4 'in' x2 by A37,A38,ZF_MODEL:13;
then E,i |= Ex(x3,x3 'in' x1 '&' H) by A39,ZF_MODEL:19;
then consider j such that
A40: for x st j.x <> i.x holds x3 = x and
A41: E,j |= x3 'in' x1 '&' H by ZF_MODEL:20;
A42: j.x1 = i.x1 by A40;
set m1 = f+*(x3,j.x3);
set m = m1+*(x4,e);
A43: m.x4 = e by FUNCT_7:128;
set k = j+*(x1,m.x1);
A44: m1.x3 = j.x3 by FUNCT_7:128;
A45: now
let x;
assume that
A46: m.x <> k.x and
A47: x2 <> x;
k.x3 = j.x3 by FUNCT_7:32;
then
A48: x3 <> x by A44,A46,FUNCT_7:32;
k.x4 = j.x4 by FUNCT_7:32;
then
A49: x4 <> x by A38,A40,A43,A46;
A50: x1 <> x by A46,FUNCT_7:128;
then k.x = j.x by FUNCT_7:32
.= i.x by A40,A48
.= h.x by A49,FUNCT_7:32
.= g.x by A9,A47
.= f.x by A50,FUNCT_7:32
.= m1.x by A48,FUNCT_7:32
.= m.x by A49,FUNCT_7:32;
hence contradiction by A46;
end;
now
let y;
assume
A51: m.y <> f.y;
assume that
x.0 <> y and
A52: x.3 <> y and
A53: x.4 <> y;
m.y = m1.y by A53,FUNCT_7:32;
hence contradiction by A51,A52,FUNCT_7:32;
end;
then
A54: E,m |= H iff def_func'(H,f).(m.x.3) = m.x.4 by A5,A7,Def1;
E,j |= x3 'in' x1 by A41,ZF_MODEL:15;
then
A55: j.x3 in j.x1 by ZF_MODEL:13;
E,j |= H by A41,ZF_MODEL:15;
then
A56: E,j |= All(x1,x2,H) by A8,Th11;
A57: i.x1 = h.x1 & h.x1 = g.x1 by A9,FUNCT_7:32;
A58: dom def_func'(H,f) = E by FUNCT_2:def 1;
for x st k.x <> j.x holds x1 = x by FUNCT_7:32;
then E,k |= All(x2,H) by A56,ZF_MODEL:16;
then def_func'(H,f).(j.x3) = a by A44,A43,A54,A45,FUNCT_7:32,ZF_MODEL:16;
hence thesis by A11,A55,A42,A57,A58,FUNCT_1:def 6;
end;
then def_func'(H,f).:u = v by A12;
hence def_func'(H,f).:u in E;
end;
now
assume
A59: for H,f st { x.0,x.1,x.2 } misses Free H & E,f |= All(x.3,Ex(x.0
,All(x.4,H <=> x.4 '=' x.0))) for u holds def_func'(H,f).:u in E;
let H;
assume
A60: { x.0,x.1,x.2 } misses Free H;
now
let a be object;
assume a in { x1,x2 };
then a = x1 or a = x2 by TARSKI:def 2;
then a in { x0,x1,x2 } by ENUMSET1:def 1;
hence not a in Free H by A60,XBOOLE_0:3;
end;
then
A61: { x1,x2 } misses Free H by XBOOLE_0:3;
x0 in { x0,x1,x2 } by ENUMSET1:def 1;
then
A62: not x0 in Free H by A60,XBOOLE_0:3;
thus E |= the_axiom_of_substitution_for H
proof
let f;
now
assume
A63: E,f |= All(x3,Ex(x0,All(x4,H <=> x4 '=' x0)));
now
let g such that
A64: for x st g.x <> f.x holds x1 = x;
reconsider v = def_func'(H,f).: (g.x1) as Element of E by A59,A60,A63
;
set h = g+*(x2,v);
A65: h.x2 = v by FUNCT_7:128;
now
let i such that
A66: for x st i.x <> h.x holds x4 = x;
A67: now
assume E,i |= x4 'in' x2;
then
A68: i.x4 in i.x2 by ZF_MODEL:13;
i.x2 = h.x2 by A66;
then consider a being object such that
A69: a in dom def_func'(H,f) and
A70: a in g.x1 and
A71: i.x4 = def_func'(H,f).a by A65,A68,FUNCT_1:def 6;
reconsider a as Element of E by A69;
set j = i+*(x3,a);
A72: j.x3 = a by FUNCT_7:128;
set m1 = f+*(x3,j.x3);
set m = m1+*(x4,i.x4);
A73: m.x4 = i.x4 by FUNCT_7:128;
set k = m+*(x1,j.x1);
A74: m1.x3 = j.x3 by FUNCT_7:128;
A75: now
let x such that
A76: j.x <> k.x and
A77: x2 <> x;
A78: x1 <> x by A76,FUNCT_7:128;
j.x4 = i.x4 by FUNCT_7:32;
then
A79: x4 <> x by A73,A76,FUNCT_7:32;
k.x3 = m.x3 by FUNCT_7:32;
then
A80: x3 <> x by A74,A76,FUNCT_7:32;
then j.x = i.x by FUNCT_7:32
.= h.x by A66,A79
.= g.x by A77,FUNCT_7:32
.= f.x by A64,A78
.= m1.x by A80,FUNCT_7:32
.= m.x by A79,FUNCT_7:32
.= k.x by A78,FUNCT_7:32;
hence contradiction by A76;
end;
A81: for x st k.x <> m.x holds x1 = x by FUNCT_7:32;
now
let x such that
A82: m.x <> f.x and
x.0 <> x and
A83: x.3 <> x and
A84: x.4 <> x;
m.x = m1.x by A84,FUNCT_7:32;
hence contradiction by A82,A83,FUNCT_7:32;
end;
then E,m |= H iff def_func'(H,f).(m.x.3) = m.x.4 by A62,A63,Def1;
then E,m |= All(x1,x2,H) by A61,A71,A72,A74,A73,Th11,FUNCT_7:32;
then E,k |= All(x2,H) by A81,ZF_MODEL:16;
then
A85: E,j |= H by A75,ZF_MODEL:16;
A86: h.x1 = g.x1 by FUNCT_7:32;
j.x1 = i.x1 & i.x1 = h.x1 by A66,FUNCT_7:32;
then E,j |= x3 'in' x1 by A70,A72,A86,ZF_MODEL:13;
then
A87: E,j |= x3 'in' x1 '&' H by A85,ZF_MODEL:15;
for x st j.x <> i.x holds x3 = x by FUNCT_7:32;
hence E,i |= Ex(x3,x3 'in' x1 '&' H) by A87,ZF_MODEL:20;
end;
now
assume E,i |= Ex(x3,x3 'in' x1 '&' H);
then consider j such that
A88: for x st j.x <> i.x holds x3 = x and
A89: E,j |= x3 'in' x1 '&' H by ZF_MODEL:20;
set m1 = f+*(x3,j.x3);
set m = m1+*(x4,i.x4);
A90: m.x4 = i.x4 by FUNCT_7:128;
set k = j+*(x1,m.x1);
A91: m1.x3 = j.x3 by FUNCT_7:128;
A92: now
let x such that
A93: m.x <> k.x and
A94: x2 <> x;
A95: x1 <> x by A93,FUNCT_7:128;
m.x3 = m1.x3 by FUNCT_7:32;
then
A96: x3 <> x by A91,A93,FUNCT_7:32;
k.x4 = j.x4 by FUNCT_7:32;
then
A97: x4 <> x by A88,A90,A93;
then m.x = m1.x by FUNCT_7:32
.= f.x by A96,FUNCT_7:32
.= g.x by A64,A95
.= h.x by A94,FUNCT_7:32
.= i.x by A66,A97
.= j.x by A88,A96
.= k.x by A95,FUNCT_7:32;
hence contradiction by A93;
end;
A98: i.x2 = h.x2 by A66;
A99: h.x1 = g.x1 & dom def_func'(H,f) = E by FUNCT_2:def 1,FUNCT_7:32;
E,j |= x3 'in' x1 by A89,ZF_MODEL:15;
then
A100: j.x3 in j.x1 by ZF_MODEL:13;
A101: now
let x such that
A102: m.x <> f.x and
x.0 <> x and
A103: x.3 <> x and
A104: x.4 <> x;
f.x = m1.x by A103,FUNCT_7:32
.= m.x by A104,FUNCT_7:32;
hence contradiction by A102;
end;
E,j |= H by A89,ZF_MODEL:15;
then
A105: E,j |= All(x1,x2,H) by A61,Th11;
A106: m.x3 = m1.x3 & i.x1 = h.x1 by A66,FUNCT_7:32;
for x st k.x <> j.x holds x1 = x by FUNCT_7:32;
then E,k |= All(x2,H) by A105,ZF_MODEL:16;
then E,m |= H by A92,ZF_MODEL:16;
then
A107: def_func'(H,f).(m.x.3) = m.x.4 by A62,A63,A101,Def1;
j.x1 = i.x1 by A88;
then i.x4 in def_func'(H,f).:(g.x1) by A91,A90,A107,A100,A106,A99
,FUNCT_1:def 6;
hence E,i |= x4 'in' x2 by A65,A98,ZF_MODEL:13;
end;
hence E,i |= x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H) by A67,
ZF_MODEL:19;
end;
then
A108: E,h |= All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H)) by ZF_MODEL:16;
for x st h.x <> g.x holds x2 = x by FUNCT_7:32;
hence
E,g |= Ex(x2,All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H))) by A108,
ZF_MODEL:20;
end;
hence
E,f |= All(x1,Ex(x2,All(x4,x4 'in' x2 <=> Ex(x3,x3 'in' x1 '&' H)
))) by ZF_MODEL:16;
end;
hence thesis by ZF_MODEL:18;
end;
end;
hence thesis by A2;
end;
theorem
E is epsilon-transitive implies ((for H st { x.0,x.1,x.2 } misses Free
H holds E |= the_axiom_of_substitution_for H) iff for F being Function st F
is_parametrically_definable_in E for X st X in E holds F.:X in E )
proof
assume
A1: E is epsilon-transitive;
thus (for H st { x.0,x.1,x.2 } misses Free H holds E |=
the_axiom_of_substitution_for H) implies for F being Function st F
is_parametrically_definable_in E for X st X in E holds F.:X in E
by A1,Th15;
assume
A2: for F being Function st F is_parametrically_definable_in E for X st
X in E holds F.:X in E;
for H,f st { x.0,x.1,x.2 } misses Free H & E,f |= All(x.3,Ex(x.0,All(x.
4,H <=> x.4 '=' x.0))) for u holds def_func'(H,f).:u in E
by Def4,A2;
hence thesis by A1,Th15;
end;
Lm3: E is epsilon-transitive implies for u,v st for w holds w in u iff w in v
holds u = v
proof
assume
A1: X in E implies X c= E;
let u,v such that
A2: for w holds w in u iff w in v;
A3: u c= E by A1;
thus u c= v
by A3,A2;
let a be object;
assume
A4: a in v;
v c= E by A1;
then reconsider e = a as Element of E by A4;
e in u by A2,A4;
hence thesis;
end;
theorem
E is being_a_model_of_ZF implies E is epsilon-transitive & (for u,v st
for w holds w in u iff w in v holds u = v) & (for u,v holds { u,v } in E) & (
for u holds union u in E) & (ex u st u <> {} & for v st v in u ex w st v c< w &
w in u) & (for u holds E /\ bool u in E) & for H,f st { x.0,x.1,x.2 } misses
Free H & E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) for u holds
def_func'(H,f).:u in E
by Lm3,Th2,Th4,Th6,Th8,Th15;
theorem
E is epsilon-transitive & (for u,v holds { u,v } in E) & (for u holds
union u in E) & (ex u st u <> {} & for v st v in u ex w st v c< w & w in u) & (
for u holds E /\ bool u in E) & (for H,f st { x.0,x.1,x.2 } misses Free H & E,f
|= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) for u holds def_func'(H,f).:u in
E ) implies E is being_a_model_of_ZF
by Th2,Th4,Th6,Th8,Th15;