:: Mostowski's Fundamental Operations - Part II
:: by Grzegorz Bancerek and Andrzej Kondracki
::
:: Received February 15, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, ARYTM_3, CARD_1,
ZF_MODEL, TARSKI, ORDINAL1, BVFUNC_2, XBOOLEAN, ZFMISC_1, CLASSES2,
ZF_REFLE, CARD_3, RELAT_1, ORDINAL2, ZF_LANG1, ZFMODEL1, XXREAL_0,
REALSET1, ZF_FUND1, FUNCT_2, ORDINAL4, NAT_1, ZF_FUND2;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1,
XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ZF_LANG,
ZF_MODEL, ZFMODEL1, ORDINAL2, NUMBERS, CARD_3, ZF_LANG1, CLASSES2,
ORDINAL4, ZF_REFLE, ZF_FUND1, XXREAL_0;
constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, CLASSES1,
ZFMODEL1, ZF_LANG1, ZF_REFLE, ZF_FUND1, ORDINAL4, RELSET_1, ZF_MODEL,
NUMBERS;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, CARD_1, CLASSES2,
ZF_LANG, ORDINAL4, FUNCT_1, ZF_FUND1, ZF_LANG1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ORDINAL1, XBOOLE_0;
equalities ORDINAL1, XBOOLE_0;
expansions TARSKI, ORDINAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ENUMSET1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2,
CARD_1, ZF_MODEL, ZFMODEL1, ZFMODEL2, ZF_LANG1, CARD_3, ZF_REFLE,
ZFREFLE1, CLASSES2, ZFMISC_1, ZF_FUND1, GRFUNC_1, RELAT_1, CLASSES1,
RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, FUNCT_7;
schemes ZF_REFLE, NAT_1;
begin
reserve H for ZF-formula,
M,E for non empty set,
e for Element of E,
m,m0,m3, m4 for Element of M,
v,v1,v2 for Function of VAR,M,
f,f1 for Function of VAR,E,
g for Function,
u,u1,u2 for set,
x,y for Variable,
i,n for Element of NAT,
X for set;
definition
let H,M,v;
func Section(H,v) -> Subset of M equals
: Def1:
{ m : M,v/(x.0,m) |= H } if
x.0 in Free H otherwise {};
coherence
proof
thus x.0 in Free H implies { m where m is Element of M: M,v/(x.0,m) |= H }
is Subset of M
proof
set X = {m where m is Element of M: M,v/(x.0,m) |= H };
assume x.0 in Free H;
X c= M
proof
let u be object;
assume u in X;
then ex m being Element of M st u = m & M,v/(x.0,m) |= H;
hence thesis;
end;
hence thesis;
end;
thus thesis by XBOOLE_1:2;
end;
consistency;
end;
definition
let M;
attr M is predicatively_closed means
for H, E, f st E in M holds Section(H,f) in M;
end;
theorem Th1:
E is epsilon-transitive implies Section(All(x.2,x.2 'in' x.0 =>
x.2 'in' x.1),f/(x.1,e)) = E /\ bool e
proof
set H = All(x.2,x.2 'in' x.0 => x.2 'in' x.1), v = f/(x.1,e);
set S = Section(H,v);
Free H=Free(x.2 'in' x.0 => x.2 'in' x.1)\{x.2} by ZF_LANG1:62
.=(Free(x.2 'in' x.0) \/ Free(x.2 'in' x.1))\{x.2} by ZF_LANG1:64
.=(Free(x.2 'in' x.0) \/ {x.2,x.1})\{x.2} by ZF_LANG1:59
.=({x.2,x.0} \/ {x.2,x.1})\{x.2} by ZF_LANG1:59
.=({x.2,x.0}\{x.2}) \/ ({x.2,x.1}\{x.2}) by XBOOLE_1:42
.=({x.2,x.0}\{x.2}) \/ {x.1} by ZFMISC_1:17,ZF_LANG1:76
.={x.0} \/ {x.1} by ZFMISC_1:17,ZF_LANG1:76
.={x.0,x.1} by ENUMSET1:1;
then x.0 in Free H by TARSKI:def 2;
then
A1: S={m where m is Element of E: E,v/(x.0,m)|= H} by Def1;
assume
A2: X in E implies X c= E;
thus S c= E /\ bool e
proof
let u be object;
assume u in S;
then consider m being Element of E such that
A3: u = m and
A4: E,v/(x.0,m) |= H by A1;
A5: m c= E by A2;
m c= e
proof
let u1 be object;
assume
A6: u1 in m;
then reconsider u1 as Element of E by A5;
A7: v/(x.0,m)/(x.2,u1).(x.2) = u1 by FUNCT_7:128;
A8: E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.0 => x.2 'in' x.1 by A4,ZF_LANG1:71;
A9: v/(x.0,m)/(x.2,u1).(x.1) = v/(x.0,m).(x.1) & v.(x.1) = v/(x.0,m).(
x.1) by FUNCT_7:32,ZF_LANG1:76;
m = v/(x.0,m).(x.0) & v/(x.0,m)/(x.2,u1).(x.0) = v/(x.0,m).(x.0) by
FUNCT_7:32,128,ZF_LANG1:76;
then E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.0 by A6,A7,ZF_MODEL:13;
then v.x.1 = e & E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.1 by A8,FUNCT_7:128
,ZF_MODEL:18;
hence thesis by A7,A9,ZF_MODEL:13;
end;
then u in bool e by A3,ZFMISC_1:def 1;
hence thesis by A3,XBOOLE_0:def 4;
end;
let u be object;
assume
A10: u in E /\ bool e;
then
A11: u in bool e by XBOOLE_0:def 4;
reconsider u as Element of E by A10,XBOOLE_0:def 4;
now
A12: v.x.1 = e by FUNCT_7:128;
let m be Element of E;
A13: v/(x.0,u)/(x.2,m).(x.2) = m by FUNCT_7:128;
A14: u = v/(x.0,u).(x.0) & v/(x.0,u)/(x.2,m).(x.0) = v/(x.0,u).(x.0) by
FUNCT_7:32,128,ZF_LANG1:76;
A15: v/(x.0,u)/(x.2,m).(x.1) = v/(x.0,u).(x.1) & v.(x.1) = v/(x.0,u).(x.1)
by FUNCT_7:32,ZF_LANG1:76;
now
assume E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.0;
then m in u by A13,A14,ZF_MODEL:13;
hence E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.1 by A11,A13,A15,A12,ZF_MODEL:13;
end;
hence E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.0 => x.2 'in' x.1 by ZF_MODEL:18;
end;
then E,v/(x.0,u) |= H by ZF_LANG1:71;
hence thesis by A1;
end;
reserve W for Universe,
w for Element of W,
Y for Subclass of W,
a,a1,b,c for Ordinal of W,
L for DOMAIN-Sequence of W;
Lm1: u1 in Union g implies ex u2 st u2 in dom g & u1 in g.u2
proof
assume u1 in Union g;
then u1 in union rng g by CARD_3:def 4;
then consider X such that
A1: u1 in X and
A2: X in rng g by TARSKI:def 4;
consider u2 being object such that
A3: u2 in dom g & X = g.u2 by A2,FUNCT_1:def 3;
take u2;
thus thesis by A1,A3;
end;
theorem Th2:
(for a,b st a in b holds L.a c= L.b) & (for a holds L.a in Union
L & L.a is epsilon-transitive) & Union L is predicatively_closed implies Union
L |= the_axiom_of_power_sets
proof
assume that
A1: for a,b st a in b holds L.a c= L.b and
A2: for a holds L.a in Union L & L.a is epsilon-transitive and
A3: Union L is predicatively_closed;
set M = Union L;
A4: X in L.a implies L.a /\ bool X in M
proof
set f = the Function of VAR,L.a;
assume X in L.a;
then reconsider e = X as Element of L.a;
L.a in M by A2;
then
A5: Section(All(x.2,x.2 'in' x.0 => x.2 'in' x.1),f/(x.1,e)) in M by A3;
L.a is epsilon-transitive by A2;
hence thesis by A5,Th1;
end;
A6: now
defpred P[set,set] means $1 in L.$2;
let X such that
A7: X in M;
A8: X in bool X by ZFMISC_1:def 1;
then reconsider D = M /\ bool X as non empty set by A7,XBOOLE_0:def 4;
A9: X in M /\ bool X by A7,A8,XBOOLE_0:def 4;
A10: for d being Element of D ex a st P[d,a]
proof
let d be Element of D;
d in M by XBOOLE_0:def 4;
then consider u2 such that
A11: u2 in dom L and
A12: d in L.u2 by Lm1;
u2 in On W by A11,ZF_REFLE:def 2;
then reconsider u2 as Ordinal of W by ZF_REFLE:7;
take u2;
thus thesis by A12;
end;
consider f being Function such that
A13: dom f = D & for d being Element of D ex a st a = f.d & P[d,a] &
for b st P[d,b] holds a c= b from ZF_REFLE:sch 1(A10);
A14: rng f c= W
proof
let u be object;
assume u in rng f;
then consider u1 being object such that
A15: u1 in D and
A16: u = f.u1 by A13,FUNCT_1:def 3;
reconsider u1 as Element of D by A15;
ex a st a = f.u1 & u1 in L.a & for b st u1 in L.b holds a c= b by A13;
hence thesis by A16;
end;
A17: M /\ bool X c= bool X by XBOOLE_1:17;
bool X in W by A7,CLASSES2:59;
then D in W by A17,CLASSES1:def 1;
then rng f = f.:(dom f) & card D in card W by CLASSES2:1,RELAT_1:113;
then card rng f in card W by A13,CARD_1:67,ORDINAL1:12;
then rng f in W by A14,CLASSES1:1;
then reconsider a = sup rng f as Ordinal of W by ZF_REFLE:19;
A18: D c= L.a
proof
let u2 be object;
assume u2 in D;
then reconsider d = u2 as Element of D;
consider c such that
A19: c = f.d and
A20: d in L.c and
for b st d in L.b holds c c= b by A13;
c in rng f by A13,A19,FUNCT_1:def 3;
then L.c c= L.a by A1,ORDINAL2:19;
hence thesis by A20;
end;
A21: L.a /\ bool X c= D by XBOOLE_1:26,ZF_REFLE:16;
D /\ bool X = M /\ (bool X /\ bool X) by XBOOLE_1:16;
then D c= L.a /\ bool X by A18,XBOOLE_1:26;
then D = L.a /\ bool X by A21;
hence M /\ bool X in M by A4,A9,A18;
end;
Union L is epsilon-transitive
proof
let X;
assume X in Union L;
then consider u such that
A22: u in dom L and
A23: X in L.u by Lm1;
reconsider u as Ordinal by A22;
u in On W by A22,ZF_REFLE:def 2;
then reconsider u as Ordinal of W by ZF_REFLE:7;
L.u is epsilon-transitive by A2;
then
A24: X c= L.u by A23;
let u1 be object;
A25: L.u c= Union L by ZF_REFLE:16;
assume u1 in X;
then u1 in L.u by A24;
hence thesis by A25;
end;
hence thesis by A6,ZFMODEL1:9;
end;
Lm2: not x in variables_in H & {x.0,x.1,x.2} misses Free H & M,v |= All(x.3,Ex
(x.0,All(x.4,H <=> x.4 '=' x.0))) implies {x.0,x.1,x.2} misses Free (H/(x.0,x))
& M,v |= All(x.3,Ex(x.0,All(x.4,H/(x.0,x) <=> x.4 '=' x.0))) & def_func'(H,v) =
def_func'(H/(x.0,x),v)
proof
assume that
A1: not x in variables_in H and
A2: {x.0,x.1,x.2} misses Free H and
A3: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
then
A4: not x.0 in Free H by A2,XBOOLE_0:3;
hence {x.0,x.1,x.2} misses Free (H/(x.0,x)) by A1,A2,ZFMODEL2:2;
A5: not x.0 in Free (H/(x.0,x)) by A1,A4,ZFMODEL2:2;
A6: now
let m3 be Element of M;
consider m0 being Element of M such that
A7: M,v/(x.3,m3)/(x.4,m) |= H iff m = m0 by A3,A4,ZFMODEL2:19;
take m0;
let m4 be Element of M;
thus M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x) implies m4 = m0
proof
assume M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x);
then M,v/(x.3,m3)/(x.4,m4)/(x.0,v/(x.3,m3)/(x.4,m4).x) |= H by A1,
ZFMODEL2:12;
then M,v/(x.3,m3)/(x.4,m4) |= H by A4,ZFMODEL2:9;
hence thesis by A7;
end;
assume m4 = m0;
then M,v/(x.3,m3)/(x.4,m4) |= H by A7;
then M,v/(x.3,m3)/(x.4,m4)/(x.0,v/(x.3,m3)/(x.4,m4).x) |= H by A4,
ZFMODEL2:9;
hence M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x) by A1,ZFMODEL2:12;
end;
Free H = Free (H/(x.0,x)) by A1,A4,ZFMODEL2:2;
hence
A8: M,v |= All(x.3,Ex(x.0,All(x.4,H/(x.0,x) <=> x.4 '=' x.0))) by A4,A6,
ZFMODEL2:19;
now
let u be object;
assume u in M;
then reconsider u9 = u as Element of M;
set m = def_func'(H,v).u9;
M,v/(x.3,u9)/(x.4,m) |= H by A3,A4,ZFMODEL2:10;
then M,v/(x.3,u9)/(x.4,m)/(x.0,v/(x.3,u9)/(x.4,m).x) |= H by A4,ZFMODEL2:9;
then M,v/(x.3,u9)/(x.4,m) |= H/(x.0,x) by A1,ZFMODEL2:12;
hence def_func'(H,v).u = def_func'(H/(x.0,x),v).u by A5,A8,ZFMODEL2:10;
end;
hence thesis by FUNCT_2:12;
end;
Lm3: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & not x.4 in Free H
implies for m holds def_func'(H,v).:m={}
proof
set m3 = the Element of M;
assume that
A1: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) and
A2: not x.4 in Free H;
M,v/(x.3,m3) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by A1,ZF_LANG1:71;
then consider m0 such that
A3: M,v/(x.3,m3)/(x.0,m0) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:73;
let m;
set u = the Element of def_func'(H,v).:m;
assume def_func'(H,v).:m<>{};
then consider u1 being object such that
A4: u1 in dom def_func'(H,v) and
A5: u1 in m and
u=def_func'(H,v).u1 by FUNCT_1:def 6;
set f=v/(x.3,m3)/(x.0,m0);
reconsider u1 as Element of M by A4;
A6: now
let m4;
M,f/(x.4,m4) |= H <=> x.4 '=' x.0 by A3,ZF_LANG1:71;
then M,f/(x.4,m4) |= H iff M,f/(x.4,m4) |= x.4 '=' x.0 by ZF_MODEL:19;
then
A7: M,f |= H iff f/(x.4,m4).x.4=f/(x.4,m4).x.0 by A2,ZFMODEL2:9,ZF_MODEL:12;
f/(x.4,m4).x.4=m4 & f.x.0=m0 by FUNCT_7:128;
hence M,f |= H iff m4=m0 by A7,FUNCT_7:32,ZF_LANG1:76;
end;
then M,f |= H;
then A: u1=m0 & m=m0 by A6;
reconsider uu1 = u1 as set;
not uu1 in uu1;
hence contradiction by A5,A;
end;
Lm4: not y in variables_in H & x<>x.0 & y<>x.0 & y<>x.4 implies (x.4 in Free H
iff x.0 in Free(Ex(x.3,x.3 'in' x '&' (H/(x.0,y)/(x.4,x.0)))))
proof
A1: x.0<>x.3 by ZF_LANG1:76;
assume that
A2: not y in variables_in H and
A3: x<>x.0 and
A4: y<>x.0 and
A5: y<>x.4;
set G=H/(x.0,y)/(x.4,x.0);
A6: Free(Ex(x.3,x.3 'in' x '&' G))= Free(x.3 'in' x '&' G)\{x.3} by ZF_LANG1:66
.=(Free(x.3 'in' x) \/ Free(G))\{x.3} by ZF_LANG1:61
.=({x.3,x} \/ Free(G))\{x.3} by ZF_LANG1:59
.=({x.3,x}\{x.3}) \/ (Free(G)\{x.3}) by XBOOLE_1:42;
A7: x.0<>x.4 by ZF_LANG1:76;
A8: now
assume
A9: x.4 in Free H;
A10: x.4 in Free(H/(x.0,y))
proof
now
per cases;
suppose
A11: x.0 in Free H;
not x.4 in {x.0} by A7,TARSKI:def 1;
then
A12: x.4 in Free H \ {x.0} by A9,XBOOLE_0:def 5;
Free(H/(x.0,y))=(Free H \{x.0}) \/ {y} by A2,A11,ZFMODEL2:2;
hence thesis by A12,XBOOLE_0:def 3;
end;
suppose
not x.0 in Free H;
hence thesis by A2,A9,ZFMODEL2:2;
end;
end;
hence thesis;
end;
A13: x.0 in {x.0} by TARSKI:def 1;
not x.0 in variables_in(H/(x.0,y)) by A4,ZF_LANG1:184;
then Free G=(Free(H/(x.0,y))\{x.4}) \/ {x.0} by A10,ZFMODEL2:2;
then
A14: x.0 in Free G by A13,XBOOLE_0:def 3;
not x.0 in {x.3} by A1,TARSKI:def 1;
then x.0 in Free(G)\{x.3} by A14,XBOOLE_0:def 5;
hence x.0 in Free(Ex(x.3,x.3 'in' x '&' G)) by A6,XBOOLE_0:def 3;
end;
now
assume x.0 in Free(Ex(x.3,x.3 'in' x '&' G));
then x.0 in {x.3,x}\{x.3} or x.0 in Free(G)\{x.3} by A6,XBOOLE_0:def 3;
then
A15: x.0 in {x.3,x} or x.0 in Free G by XBOOLE_0:def 5;
A16: not x.0 in variables_in(H/(x.0,y)) by A4,ZF_LANG1:184;
A17: now
assume not x.4 in Free(H/(x.0,y));
then
A18: x.0 in Free(H/(x.0,y)) by A3,A1,A15,A16,TARSKI:def 2,ZFMODEL2:2;
Free(H/(x.0,y)) c= variables_in(H/(x.0,y)) by ZF_LANG1:151;
hence contradiction by A4,A18,ZF_LANG1:184;
end;
Free(H/(x.0,y)) c= (Free H \ {x.0}) \/ {y} by ZFMODEL2:1;
then x.4 in Free H \ {x.0} or x.4 in {y} by A17,XBOOLE_0:def 3;
hence x.4 in Free H by A5,TARSKI:def 1,XBOOLE_0:def 5;
end;
hence thesis by A8;
end;
theorem Th3:
omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a
<> {} & a is limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union
L & L.a is epsilon-transitive) & Union L is predicatively_closed implies for H
st {x.0,x.1,x.2} misses Free H holds Union L |= the_axiom_of_substitution_for H
proof
assume that
A1: omega in W and
A2: for a,b st a in b holds L.a c= L.b and
A3: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a) and
A4: for a holds L.a in Union L & L.a is epsilon-transitive and
A5: Union L is predicatively_closed;
set M = Union L;
A6: now
defpred P[set,set] means $1 in L.$2;
let H;
let f be Function of VAR,M such that
A7: {x.0,x.1,x.2} misses Free H and
A8: M,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
consider k being Element of NAT such that
A9: for i st x.i in variables_in H holds i < k by ZFMODEL2:3;
set p = H/(x.0,x.(k+5));
k+0 = k;
then
A10: not x.(k+5) in variables_in H by A9,XREAL_1:7;
then
A11: M,f |= All(x.3,Ex(x.0,All(x.4,p <=> x.4 '=' x.0))) & def_func'(H,f) =
def_func'(p,f) by A7,A8,Lm2;
set F = def_func'(H,f);
A12: for d being Element of M qua non empty set ex a st P[d,a]
proof
let d be Element of M qua non empty set;
consider u such that
A13: u in dom L and
A14: d in L.u by Lm1;
u in On W by A13,ZF_REFLE:def 2;
then reconsider u as Ordinal of W by ZF_REFLE:7;
take u;
thus thesis by A14;
end;
consider g being Function such that
A15: dom g = M & for d being Element of M qua non empty set ex a st a
= g.d & P[d,a] & for b st P[d,b] holds a c= b from ZF_REFLE:sch 1(A12);
A16: rng g c= W
proof
let u1 be object;
assume u1 in rng g;
then consider u2 being object such that
A17: u2 in dom g and
A18: u1 = g.u2 by FUNCT_1:def 3;
reconsider d = u2 as Element of M by A15,A17;
ex a st a = g.d & d in L.a & for b st d in L.b holds a c= b by A15;
hence thesis by A18;
end;
card VAR = omega & omega in card W by A1,CARD_1:5,47,CLASSES2:1,ZF_REFLE:17
;
then
A19: card dom f in card W by FUNCT_2:def 1;
rng f = f.: dom f by RELAT_1:113;
then card (rng f) in card W by A19,CARD_1:67,ORDINAL1:12;
then
A20: card (g.:(rng f)) in card W by CARD_1:67,ORDINAL1:12;
g.:(rng f) c= rng g by RELAT_1:111;
then g.:(rng f) c= W by A16;
then g.:(rng f) in W by A20,CLASSES1:1;
then reconsider b2 = sup (g.:(rng f)) as Ordinal of W by ZF_REFLE:19;
A21: x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
{x.0,x.1,x.2} misses Free p by A7,A8,A10,Lm2;
then
A22: not x.0 in Free p by A21,XBOOLE_0:3;
A23: X c= M & sup (g.:X) c= a implies X c= L.a
proof
assume that
A24: X c= M and
A25: sup (g.:X) c= a;
let u1 be object;
assume
A26: u1 in X;
then reconsider d = u1 as Element of M by A24;
consider b such that
A27: b = g.d and
A28: d in L.b and
for a st d in L.a holds b c= a by A15;
b in g.:X by A15,A26,A27,FUNCT_1:def 6;
then b in sup (g.:X) by ORDINAL2:19;
then L.b c= L.a by A2,A25;
hence thesis by A28;
end;
let u be Element of M;
consider b0 being Ordinal of W such that
b0 = g.u and
A29: u in L.b0 and
for b st u in L.b holds b0 c= b by A15;
A30: card u in card W by CLASSES2:1;
k+0 = k;
then
A31: 0 <= k & k < k+5 by NAT_1:2,XREAL_1:6;
then
A32: not x.0 in variables_in p by ZF_LANG1:76,184;
g.:(F.:u) c= rng g by RELAT_1:111;
then
A33: g.:(F.:u) c= W by A16;
card (g.:(F.:u)) c= card (F.:u) & card (F.:u) c= card u by CARD_1:67;
then card (g.:(F.:u)) in card W by A30,ORDINAL1:12,XBOOLE_1:1;
then g.:(F.:u) in W by A33,CLASSES1:1;
then reconsider b1 = sup (g.:(F.:u)) as Ordinal of W by ZF_REFLE:19;
set b = b0 \/ b1;
set a = b \/ b2;
A34: F.:u c= L.b by A23,XBOOLE_1:7;
consider phi being Ordinal-Sequence of W such that
A35: phi is increasing & phi is continuous and
A36: for a st phi.a = a & {} <> a for v being Function of VAR,L.a
holds M,M!v |= p/(x.4,x.0) iff L.a,v |= p/(x.4,x.0) by A1,A2,A3,ZF_REFLE:20;
consider a1 such that
A37: a in a1 and
A38: phi.a1 = a1 by A1,A35,ZFREFLE1:28;
A39: rng f c= L.a1
proof
let u be object;
A40: b2 c= a by XBOOLE_1:7;
assume
A41: u in rng f;
then consider u1 being object such that
A42: u1 in dom f and
A43: u = f.u1 by FUNCT_1:def 3;
reconsider u1 as Variable by A42;
consider a2 being Ordinal of W such that
A44: a2 = g.(f.u1) and
A45: f.u1 in L.a2 and
for b st f.u1 in L.b holds a2 c= b by A15;
a2 in g.:rng f by A15,A41,A43,A44,FUNCT_1:def 6;
then a2 in b2 by ORDINAL2:19;
then L.a2 c= L.a1 by A2,A37,A40,ORDINAL1:10;
hence thesis by A43,A45;
end;
set x = x.(k+10);
k+0 = k;
then not k+10 < k by XREAL_1:6;
then not x in variables_in H by A9;
then
A46: not x in variables_in H \ {x.0} by XBOOLE_0:def 5;
set q = Ex(x.3,x.3 'in' x '&' (p/(x.4,x.0)));
A47: 10 <= 10+k by NAT_1:11;
b0 c= b & b c= a by XBOOLE_1:7;
then b0 c= a;
then
A48: L.b0 c= L.a1 by A2,A37,ORDINAL1:12;
then reconsider mu = u as Element of L.a1 by A29;
dom f = VAR by FUNCT_2:def 1;
then reconsider v = f as Function of VAR,L.a1 by A39,FUNCT_2:def 1
,RELSET_1:4;
set w = v/(x.0,v.x.4)/(x,mu);
A49: x <> x.(k+5) implies not x in {x.(k+5)} by TARSKI:def 1;
variables_in p c= (variables_in H \ {x.0}) \/ {x.(k+5)} & k+5 <> k+
10 by ZF_LANG1:187;
then not x in variables_in p by A46,A49,XBOOLE_0:def 3,ZF_LANG1:76;
then
A50: variables_in (p/(x.4,x.0)) c= (variables_in p \ {x.4}) \/ {x.0} &
not x in variables_in p \ {x.4} by XBOOLE_0:def 5,ZF_LANG1:187;
A51: 10 > 0;
then
A52: x <> x.0 by A47,ZF_LANG1:76;
then not x in {x.0} by TARSKI:def 1;
then
A53: not x in variables_in (p/(x.4,x.0)) by A50,XBOOLE_0:def 3;
A54: 10 > 3;
then
A55: x.0 <> x.3 & x <> x.3 by A47,ZF_LANG1:76;
b in a1 by A37,ORDINAL1:12,XBOOLE_1:7;
then L.b c= L.a1 by A2;
then
A56: F.:u c= L.a1 by A34;
A57: F.:u = Section(q,w)
proof
now
per cases;
suppose
A58: x.4 in Free H;
4<>k+5 by NAT_1:11;
then
A59: x.(k+5)<>x.4 by ZF_LANG1:76;
A60: x.(k+10)<>x.0 by A51,A47,ZF_LANG1:76;
( not x.(k+5) in variables_in H)& x.(k+5)<>x.0 by A9,A31,ZF_LANG1:76;
then
A61: x.0 in Free q by A58,A60,A59,Lm4;
A62: F.:u c= Section(q,w)
proof
let u1 be object;
assume
A63: u1 in F.:u;
then consider u2 being object such that
A64: u2 in dom F and
A65: u2 in u and
A66: u1 = F.u2 by FUNCT_1:def 6;
reconsider m1 = u1 as Element of L.a1 by A56,A63;
reconsider u2 as Element of M by A64;
L.a1 is epsilon-transitive by A4;
then u c= L.a1 by A29,A48;
then reconsider m2 = u2 as Element of L.a1 by A65;
A67: f/(x.3,u2)/(x.0,F.u2) = M!(v/(x.3,m2)/(x.0,m1)) by A66,
ZF_LANG1:def 1,ZF_REFLE:16;
M,f/(x.3,u2)/(x.4,F.u2) |= p & f/(x.3,u2)/(x.4,F.u2).(x.4)=F
. u2 by A11,A22,FUNCT_7:128,ZFMODEL2:10;
then M,f/(x.3,u2)/(x.4,F.u2)/(x.0,F.u2) |= p/(x.4,x.0) by A32,
ZFMODEL2:13;
then
A68: M,f/(x.3,u2)/(x.0,F.u2)/(x.4,F.u2) |= p/(x.4,x.0) by FUNCT_7:33
,ZF_LANG1:76;
not x.4 in variables_in (p/(x.4,x.0)) by ZF_LANG1:76,184;
then M,f/(x.3,u2)/(x.0,F.u2) |= p/(x.4,x.0) by A68,ZFMODEL2:5;
then L.a1,v/(x.3,m2)/(x.0,m1) |= p/(x.4,x.0) by A36,A37,A38,A67;
then
A69: L.a1,v/(x.3,m2)/(x.0,m1)/(x,mu) |= p/(x.4,x.0) by A53,ZFMODEL2:5;
A70: w.x = w/(x.0,m1).x & w.x = mu by A51,A47,FUNCT_7:32,128,ZF_LANG1:76
;
w/(x.0,m1)/(x.3,m2).(x.3) = m2 & w/(x.0,m1)/(x.3,m2).x = w/(
x.0,m1).x by A54,A47,FUNCT_7:32,128,ZF_LANG1:76;
then
A71: L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x by A65,A70,ZF_MODEL:13;
w/(x.0,m1) = v/(x,mu)/(x.0,m1) by ZFMODEL2:8;
then L.a1,w/(x.0,m1)/(x.3,m2) |= p/(x.4,x.0) by A52,A55,A69,
ZFMODEL2:6;
then L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x '&' (p/(x.4,x.0)) by
A71,ZF_MODEL:15;
then L.a1,w/(x.0,m1) |= q by ZF_LANG1:73;
then u1 in { m where m is Element of L.a1: L.a1,w/(x.0,m) |= q };
hence thesis by A61,Def1;
end;
Section(q,w) c= F.:u
proof
let u1 be object;
A72: L.a1 c= M by ZF_REFLE:16;
assume u1 in Section(q,w);
then u1 in { m where m is Element of L.a1: L.a1,w/(x.0,m) |= q }
by A61,Def1;
then consider m1 being Element of L.a1 such that
A73: u1 = m1 and
A74: L.a1,w/(x.0,m1) |= q;
consider m2 being Element of L.a1 such that
A75: L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x '&' (p/(x.4,x.0))
by A74,ZF_LANG1:73;
reconsider u9 = m1, u2 = m2 as Element of M by A72;
A76: w/(x.0,m1) = v/(x,mu)/(x.0,m1) by ZFMODEL2:8;
L.a1,w/(x.0,m1)/(x.3,m2) |= p/(x.4,x.0) by A75,ZF_MODEL:15;
then L.a1,v/(x.3,m2)/(x.0,m1)/(x,mu) |= p/(x.4,x.0) by A52,A55,A76,
ZFMODEL2:6;
then
A77: L.a1,v/(x.3,m2)/(x.0,m1) |= p/(x.4,x.0) by A53,ZFMODEL2:5;
A78: f/(x.3,u2)/(x.0,u9)/(x.4,u9) = f/(x.3,u2)/(x.4,u9)/(x.0,u9)
& f/(x.3,u2)/(x. 0,u9).(x.0) = u9 by FUNCT_7:33,128,ZF_LANG1:76;
f/(x.3,u2)/(x.0,u9) = M!(v/(x.3,m2)/(x.0,m1)) by ZF_LANG1:def 1
,ZF_REFLE:16;
then M,f/(x.3,u2)/(x.0,u9) |= p/(x.4,x.0) by A36,A37,A38,A77;
then M,f/(x.3,u2)/(x.4,u9)/(x.0,u9) |= p by A32,A78,ZFMODEL2:12;
then M,f/(x.3,u2)/(x.4,u9) |= p by A32,ZFMODEL2:5;
then
A79: F.u2 = u9 by A11,A22,ZFMODEL2:10;
A80: w.x = w/(x.0,m1).x & w.x = mu by A51,A47,FUNCT_7:32,128,ZF_LANG1:76
;
A81: L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x by A75,ZF_MODEL:15;
A82: dom F = M by FUNCT_2:def 1;
w/(x.0,m1)/(x.3,m2).(x.3) = m2 & w/(x.0,m1)/(x.3,m2).x = w/(
x.0,m1).x by A54,A47,FUNCT_7:32,128,ZF_LANG1:76;
then m2 in u by A81,A80,ZF_MODEL:13;
hence thesis by A73,A79,A82,FUNCT_1:def 6;
end;
hence thesis by A62;
end;
suppose
A83: not x.4 in Free H;
4<>k+5 by NAT_1:11;
then
A84: x.(k+5)<>x.4 by ZF_LANG1:76;
A85: x.(k+10)<>x.0 by A51,A47,ZF_LANG1:76;
( not x.(k+5) in variables_in H)& x.(k+5)<>x.0 by A9,A31,ZF_LANG1:76;
then not x.0 in Free q by A83,A85,A84,Lm4;
then Section(q,w)={} by Def1;
hence thesis by A8,A83,Lm3;
end;
end;
hence thesis;
end;
L.a1 in M by A4;
hence def_func'(H,f).:u in M by A5,A57;
end;
Union L is epsilon-transitive
proof
let X;
assume X in Union L;
then consider u such that
A86: u in dom L and
A87: X in L.u by Lm1;
reconsider u as Ordinal by A86;
u in On W by A86,ZF_REFLE:def 2;
then reconsider u as Ordinal of W by ZF_REFLE:7;
L.u is epsilon-transitive by A4;
then
A88: X c= L.u by A87;
let u1 be object;
A89: L.u c= Union L by ZF_REFLE:16;
assume u1 in X;
then u1 in L.u by A88;
hence thesis by A89;
end;
hence thesis by A6,ZFMODEL1:15;
end;
Lm5: x.i in Free H implies {[i,m]} \/ (v*decode)|((code Free H)\{i})=(v/(x.i,m
)*decode)|code Free H
proof
set e=v/(x.i,m)*decode;
set f=v*decode;
set b=f|((code Free H)\{i});
A1: i in {i} by TARSKI:def 1;
A2: dom(e|{i})=(dom e) /\ {i} by RELAT_1:61
.=omega /\ {i} by ZF_FUND1:31
.={i} by ZFMISC_1:46;
then
A3: (e|{i})={[i,(e|{i}).i]} by GRFUNC_1:7
.={[i,e.i]} by A1,A2,FUNCT_1:47
.={[i,e.x".x.i]} by ZF_FUND1:def 3
.={[i,(v/(x.i,m)).x.i]} by ZF_FUND1:32
.={[i,m]} by FUNCT_7:128;
A4: dom b=(dom f) /\ ((code Free H)\{i}) by RELAT_1:61
.=omega /\ ((code Free H)\{i}) by ZF_FUND1:31
.=dom e /\ ((code Free H)\{i}) by ZF_FUND1:31
.=dom(e|((code Free H)\{i})) by RELAT_1:61;
now
let u be object;
assume
A5: u in dom b;
then u in (dom f) /\ ((code Free H)\{i}) by RELAT_1:61;
then
A6: u in (code Free H) \ {i} by XBOOLE_0:def 4;
then u in code Free H by XBOOLE_0:def 5;
then consider x such that
x in Free H and
A7: u=x".x by ZF_FUND1:33;
not u in {i} by A6,XBOOLE_0:def 5;
then i<>x".x by A7,TARSKI:def 1;
then
A8: x<>x.i by ZF_FUND1:def 3;
thus b.u = f.u by A5,FUNCT_1:47
.=v.x by A7,ZF_FUND1:32
.=(v/(x.i,m)).x by A8,FUNCT_7:32
.=e.u by A7,ZF_FUND1:32
.=(e|((code Free H)\{i})).u by A4,A5,FUNCT_1:47;
end;
then
A9: b=e|((code Free H)\{i}) by A4,FUNCT_1:2;
assume x.i in Free H;
then x".x.i in code Free H by ZF_FUND1:33;
then i in code Free H by ZF_FUND1:def 3;
then {i} c= code Free H by ZFMISC_1:31;
then e|code Free H=(e|({i} \/ ((code Free H)\{i}))) by XBOOLE_1:45
.={[i,m]} \/ b by A3,A9,RELAT_1:78;
hence thesis;
end;
theorem Th4:
Section(H,v)= {m : {[{},m]} \/ (v*decode)|((code Free H)\{{}}) in
Diagram(H,M)}
proof
set S=Section(H,v);
set D={m:{[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M)};
now
per cases;
suppose
A1: x.0 in Free H;
then
A2: S={m: M,v/(x.0,m) |= H} by Def1;
A3: D c= S
proof
let u be object;
assume u in D;
then consider m such that
A4: m=u and
A5: {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M);
(v/(x.0,m)*decode)|code Free H in Diagram(H,M) by A1,A5,Lm5;
then
ex v1 st (v/(x.0,m)*decode)|code Free H=(v1*decode)|code Free H &
v1 in St(H,M) by ZF_FUND1:def 5;
then v/(x.0,m) in St(H,M) by ZF_FUND1:36;
then M,v/(x.0,m) |= H by ZF_MODEL:def 4;
hence thesis by A2,A4;
end;
S c= D
proof
let u be object;
assume u in S;
then consider m such that
A6: m=u and
A7: M,v/(x.0,m) |= H by A2;
v/(x.0,m) in St(H,M) by A7,ZF_MODEL:def 4;
then (v/(x.0,m)*decode)|code Free H in Diagram(H,M) by ZF_FUND1:def 5;
then {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M) by A1
,Lm5;
hence thesis by A6;
end;
hence thesis by A3;
end;
suppose
A8: not x.0 in Free H;
now
set u = the Element of D;
assume D<>{};
then u in D;
then consider m such that
m=u and
A9: {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M);
consider v2 such that
A10: ({[{},m]}\/(v*decode)|((code Free H)\{{}})) =(v2*decode)|code
Free H and
v2 in St(H,M) by A9,ZF_FUND1:def 5;
reconsider w={[{},m]}\/(v*decode)|((code Free H)\{{}}) as Function by
A10;
[{},m]in{[{},m]} by TARSKI:def 1;
then [{},m] in w by XBOOLE_0:def 3;
then {} in dom w by FUNCT_1:1;
then {} in dom(v2*decode)/\(code Free H) by A10,RELAT_1:61;
then {} in code Free H by XBOOLE_0:def 4;
then ex y st y in Free H & {}=x".y by ZF_FUND1:33;
hence contradiction by A8,ZF_FUND1:def 3;
end;
hence thesis by A8,Def1;
end;
end;
hence thesis;
end;
theorem Th5:
Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is
predicatively_closed
proof
assume that
A1: Y is closed_wrt_A1-A7 and
A2: Y is epsilon-transitive;
let H,E,f such that
A3: E in Y;
now
per cases;
suppose
not x.0 in Free H;
then Section(H,f)={} by Def1;
hence thesis by A1,ZF_FUND1:3;
end;
suppose
A4: x.0 in Free H;
reconsider a=E as Element of W by A3;
reconsider n={} as Element of omega by ORDINAL1:def 11;
set fs=(code Free H)\{n};
A5: Diagram(H,E) in Y by A1,A3,ZF_FUND1:22;
then reconsider b=Diagram(H,E) as Element of W;
A6: b c= Funcs(fs \/ {n},a)
proof
let u be object;
assume u in b;
then ex f1 st u=(f1*decode)|code Free H & f1 in St(H,E) by
ZF_FUND1:def 5;
then
A7: u in Funcs(code Free H,a) by ZF_FUND1:31;
x".x.0 in code Free H by A4,ZF_FUND1:33;
then n in code Free H by ZF_FUND1:def 3;
then {n} c= code Free H by ZFMISC_1:31;
hence thesis by A7,XBOOLE_1:45;
end;
n in {n} by TARSKI:def 1;
then
A8: not n in fs by XBOOLE_0:def 5;
A9: (f*decode)|fs in Funcs(fs,a) by ZF_FUND1:31;
Funcs(fs,a) in Y by A1,A3,ZF_FUND1:9;
then reconsider y=(f*decode)|fs as Element of W by A9,ZF_FUND1:1;
set B={e: {[n,e]} \/ y in b};
set A={w: w in a & {[n,w]} \/ y in b};
A10: A=B
proof
thus A c= B
proof
let u be object;
assume u in A;
then ex w st u=w & w in a & {[n,w]} \/ y in b;
hence thesis;
end;
let u be object;
assume u in B;
then consider e such that
A11: u=e and
A12: {[n,e]} \/ y in b;
reconsider e as Element of W by A3,ZF_FUND1:1;
e in A by A12;
hence thesis by A11;
end;
a c= Y by A2,A3;
then A in Y by A1,A3,A5,A9,A8,A6,ZF_FUND1:16;
hence thesis by A10,Th4;
end;
end;
hence thesis;
end;
theorem
omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {}
& a is limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union L & L
.a is epsilon-transitive) & Union L is closed_wrt_A1-A7 implies Union L is
being_a_model_of_ZF
proof
assume that
A1: omega in W and
A2: for a,b st a in b holds L.a c= L.b and
A3: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a) and
A4: for a holds L.a in Union L & L.a is epsilon-transitive and
A5: Union L is closed_wrt_A1-A7;
A6: Union L is epsilon-transitive
proof
let X;
assume X in Union L;
then consider u such that
A7: u in dom L and
A8: X in L.u by Lm1;
reconsider u as Ordinal by A7;
u in On W by A7,ZF_REFLE:def 2;
then reconsider u as Ordinal of W by ZF_REFLE:7;
L.u is epsilon-transitive by A4;
then
A9: X c= L.u by A8;
let u1 be object;
A10: L.u c= Union L by ZF_REFLE:16;
assume u1 in X;
then u1 in L.u by A9;
hence thesis by A10;
end;
then Union L is predicatively_closed by A5,Th5;
then
A11: Union L |= the_axiom_of_power_sets & for H st {x.0,x.1,x.2} misses
Free H holds Union L |= the_axiom_of_substitution_for H by A1,A2,A3,A4,Th2
,Th3;
for u st u in Union L holds union u in Union L by A5,ZF_FUND1:2;
then
A12: Union L |= the_axiom_of_unions by A6,ZFMODEL1:5;
for u1,u2 st u1 in Union L & u2 in Union L holds {u1,u2} in Union L by A5,
ZF_FUND1:6;
then
A13: Union L |= the_axiom_of_pairs by A6,ZFMODEL1:3;
ex u st u in Union L & u<>{} & for u1 st u1 in u ex u2 st u1 c< u2 & u2 in u
proof
A14: card omega in card W by A1,CLASSES2:1;
deffunc G(set,set) = inf {w: L.$2 in L.w};
consider ksi being Function such that
A15: dom ksi=NAT & ksi.0=0-element_of(W) & for i being Nat holds ksi.(
i+1)=G(i,ksi.i) from NAT_1:sch 11;
card rng ksi c= card NAT by A15,CARD_1:12;
then
A16: card rng ksi in card W by A14,ORDINAL1:12;
set lambda=sup rng ksi;
A17: for i being Nat holds ksi.i in On W & ksi.i is Ordinal of W
proof
defpred P[Nat] means ksi.$1 in On W & ksi.$1 is Ordinal of W;
A18: now
let i be Nat;
assume P[i];
then reconsider a=ksi.i as Ordinal of W;
A19: ksi.(i+1)=inf {w: L.a in L.w} by A15;
consider u such that
A20: u in dom L and
A21: L.a in L.u by A4,Lm1;
dom L=On W by ZF_REFLE:def 2;
then reconsider b=u as Ordinal of W by A20,ZF_REFLE:7;
b in {w: L.a in L.w} by A21;
then inf {w: L.a in L.w} c= b by ORDINAL2:14;
then ksi.(i+1) in W by A19,CLASSES1:def 1;
hence P[i+1] by A19,ORDINAL1:def 9;
end;
A22: P[0] by A15,ZF_REFLE:7;
thus for i being Nat holds P[i] from NAT_1:sch 2(A22,A18);
end;
rng ksi c= W
proof
let a be object;
assume a in rng ksi;
then consider i being object such that
A23: i in dom ksi and
A24: a=ksi.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A15,A23;
ksi.i in On W by A17;
hence thesis by A24,ORDINAL1:def 9;
end;
then rng ksi in W by A16,CLASSES1:1;
then reconsider l=lambda as Ordinal of W by ZF_REFLE:19;
A25: for i holds L.(ksi.i) in L.(ksi.(i+1))
proof
let i;
reconsider a=ksi.i as Ordinal of W by A17;
consider b being set such that
A26: b in dom L and
A27: L.a in L.b by A4,Lm1;
b in On W by A26,ZF_REFLE:def 2;
then reconsider b as Ordinal of W by ZF_REFLE:7;
A28: b in {w: L.a in L.w} by A27;
ksi.(i+1)=inf {w: L.(ksi.i) in L.w} by A15;
then ksi.(i+1) in {w: L.(ksi.i) in L.w} by A28,ORDINAL2:17;
then ex w st w=ksi.(i+1) & L.a in L.w;
hence thesis;
end;
A29: for i holds ksi.i in ksi.(i+1)
proof
let i;
reconsider b=ksi.(i+1) as Ordinal of W by A17;
reconsider a=ksi.i as Ordinal of W by A17;
assume not ksi.i in ksi.(i+1);
then b=a or b in a by ORDINAL1:14;
then L.b c= L.a by A2;
hence contradiction by A25,ORDINAL1:5;
end;
A30: l c= union l
proof
let u1 be Ordinal;
assume u1 in l;
then consider u2 being Ordinal such that
A31: u2 in rng ksi and
A32: u1 c= u2 by ORDINAL2:21;
consider i being object such that
A33: i in dom ksi and
A34: u2=ksi.i by A31,FUNCT_1:def 3;
reconsider i as Element of NAT by A15,A33;
reconsider u3=ksi.(i+1) as Ordinal of W by A17;
u3 in rng ksi by A15,FUNCT_1:def 3;
then
A35: u3 in l by ORDINAL2:19;
u1 in u3 by A29,A32,A34,ORDINAL1:12;
hence thesis by A35,TARSKI:def 4;
end;
union l c= l by ORDINAL2:5;
then l=union l by A30;
then
A36: l is limit_ordinal;
A37: union the set of all L.(ksi.n)=L.l
proof
set A=the set of all L.(ksi.n);
thus union A c= L.l
proof
let u1 be object;
assume u1 in union A;
then consider X such that
A38: u1 in X and
A39: X in A by TARSKI:def 4;
consider n such that
A40: X=L.(ksi.n) by A39;
reconsider a=ksi.n as Ordinal of W by A17;
a in rng ksi by A15,FUNCT_1:def 3;
then L.a c= L.l by A2,ORDINAL2:19;
hence thesis by A38,A40;
end;
0-element_of W in rng ksi by A15,FUNCT_1:def 3;
then l<>{} by ORDINAL2:19;
then
A41: L.l=Union(L|l) by A3,A36;
let u1 be object;
assume u1 in L.l;
then consider u2 such that
A42: u2 in dom(L|l) and
A43: u1 in (L|l).u2 by A41,Lm1;
A44: u1 in L.u2 by A42,A43,FUNCT_1:47;
A45: u2 in (dom L) /\ l by A42,RELAT_1:61;
then
A46: u2 in l by XBOOLE_0:def 4;
u2 in dom L by A45,XBOOLE_0:def 4;
then u2 in On W by ZF_REFLE:def 2;
then reconsider u2 as Ordinal of W by ZF_REFLE:7;
consider b being Ordinal such that
A47: b in rng ksi and
A48: u2 c= b by A46,ORDINAL2:21;
consider i being object such that
A49: i in dom ksi and
A50: b=ksi.i by A47,FUNCT_1:def 3;
reconsider i as Element of NAT by A15,A49;
b=ksi.i by A50;
then reconsider b as Ordinal of W by A17;
u2 c< b iff u2 c= b & u2 <> b;
then
A51: L.u2 c= L.b by A2,A48,ORDINAL1:11;
L.(ksi.i) in A;
hence thesis by A44,A50,A51,TARSKI:def 4;
end;
take u = L.lambda;
L.l in Union L by A4;
hence u in Union L & u<>{};
let u1;
assume u1 in u;
then consider u2 such that
A52: u1 in u2 & u2 in the set of all L.(ksi.n) by A37,TARSKI:def 4;
take u2;
consider i such that
A53: u2=L.(ksi.i) by A52;
A54: u1<>u2 by A52;
reconsider a=ksi.i as Ordinal of W by A17;
L.a is epsilon-transitive by A4;
then u1 c= u2 by A52,A53;
hence u1 c< u2 by A54;
A55: L.(ksi.(i+1)) in the set of all L.(ksi.n);
L.(ksi.i) in L.(ksi.(i+1)) by A25;
hence u2 in u by A37,A53,A55,TARSKI:def 4;
end;
then Union L |= the_axiom_of_infinity by A6,ZFMODEL1:7;
hence thesis by A6,A13,A12,A11,ZF_MODEL:def 12;
end;