:: The Contraction Lemma
:: by Grzegorz Bancerek
::
:: Received April 14, 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 XBOOLE_0, ORDINAL1, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, ZF_LANG,
ZF_MODEL, BVFUNC_2, CARD_1, XBOOLEAN, FUNCT_4, ARYTM_3, ZF_COLLA;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ZF_LANG,
ORDINAL1, NUMBERS, FUNCT_2, FUNCT_7, ZF_MODEL;
constructors NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, MEMBERED, ZF_LANG, RELSET_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ORDINAL1, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems FUNCT_1, ZF_LANG, ZF_MODEL, ORDINAL1, ZFMISC_1, RELAT_1, XBOOLE_0,
FUNCT_7, XREGULAR;
schemes TARSKI, CLASSES1, ORDINAL1, XBOOLE_0;
begin
reserve X,Y,Z for set,
x,y,z for object,
E for non empty set,
A,B,C for Ordinal ,
L,L1 for Sequence,
f,f1,f2,h for Function,
d,d1,d2,d9 for Element of E;
definition
let E,A;
deffunc H(Sequence) = { d : for d1 st d1 in d ex C st C in dom($1) & d1 in
union { $1.C } };
func Collapse (E,A) -> set means
:Def1:
ex L st it = { d : for d1 st d1 in d
ex B st B in dom L & d1 in union { L.B } } & dom L = A & for B st B in A holds
L.B = { d1 : for d st d in d1 ex C st C in dom(L|B) & d in union { L|B.C } };
existence
proof
consider L such that
A1: dom L = A and
A2: for B,L1 st B in A & L1 = L|B holds L.B = H(L1) from ORDINAL1:sch
4;
take x = { d : for d1 st d1 in d ex B st B in dom L & d1 in union { L.B }
}, L;
thus x = { d : for d1 st d1 in d ex B st B in dom L & d1 in union { L.B }
};
thus dom L = A by A1;
let B;
assume B in A;
hence thesis by A2;
end;
uniqueness
proof
let X1,X2 be set;
given L such that
A3: X1 = { d : for d1 st d1 in d ex B st B in dom L & d1 in union { L.
B } } & dom L = A & for B st B in A holds L.B = { d1 : for d st d in d1 ex C st
C in dom(L|B) & d in union { L|B.C } };
A4: dom L = A & for B,L1 st B in A & L1 = L|B holds L.B = H(L1) by A3;
given L1 such that
A5: X2 = {d: for d1 st d1 in d ex B st B in dom L1 & d1 in union { L1.
B }} & dom L1 = A & for B st B in A holds L1.B = {d1: for d st d in d1 ex C st
C in dom(L1|B) & d in union { L1|B.C }};
A6: dom L1 = A & for B,L st B in A & L = L1|B holds L1.B = H(L) by A5;
L = L1 from ORDINAL1:sch 3(A4,A6);
hence thesis by A3,A5;
end;
end;
theorem Th1:
Collapse (E,A) = { d : for d1 st d1 in d ex B st B in A & d1 in
Collapse (E,B) }
proof
defpred P[object,object] means ex B st B = $1 & $2 = Collapse (E,B);
deffunc H(Sequence) = { d : for d1 st d1 in d ex C st C in dom($1) & d1 in
union { $1.C } };
deffunc F(Ordinal) = Collapse(E,$1);
A1: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume x in A;
then reconsider B = x as Ordinal;
take Collapse (E,B) , B;
thus thesis;
end;
consider f such that
A2: dom f = A & for x being object st x in A holds P[x,f.x]
from CLASSES1:sch 1(A1);
reconsider L = f as Sequence by A2,ORDINAL1:def 7;
A3: now
let A;
assume A in dom L;
then ex B st B = A & L.A = Collapse (E,B) by A2;
hence L.A = F(A);
end;
A4: for A for x being object
holds x = F(A) iff ex L st x = H(L) & dom L = A & for B st B in
A holds L.B = H(L|B) by Def1;
for B st B in dom L holds L.B = H(L|B) from ORDINAL1:sch 5(A4,A3);
then
A5: Collapse (E,A) = { d : for d1 st d1 in d ex B st B in dom L & d1 in
union { L.B } } by A2,Def1;
now
let x be object;
assume
x in { d : for d1 st d1 in d ex B st B in dom L & d1 in union { L .B } };
then consider d such that
A6: x = d and
A7: for d1 st d1 in d ex B st B in dom L & d1 in union { L.B };
for d1 st d1 in d ex B st B in A & d1 in Collapse (E,B)
proof
let d1;
assume d1 in d;
then consider B such that
A8: B in dom L and
A9: d1 in union { L.B } by A7;
take B;
thus B in A by A2,A8;
L.B = Collapse (E,B) by A3,A8;
hence thesis by A9,ZFMISC_1:25;
end;
hence x in { d1 : for d st d in d1 ex B st B in A & d in Collapse (E,B) }
by A6;
end;
hence Collapse (E,A) c= { d : for d1 st d1 in d ex B st B in A & d1 in
Collapse (E,B) } by A5;
let x be object;
assume x in { d1 : for d st d in d1 ex B st B in A & d in Collapse (E,B) };
then consider d1 such that
A10: x = d1 and
A11: for d st d in d1 ex B st B in A & d in Collapse (E,B);
for d st d in d1 ex B st B in dom L & d in union { L.B }
proof
let d;
assume d in d1;
then consider B such that
A12: B in A and
A13: d in Collapse (E,B) by A11;
take B;
thus B in dom L by A2,A12;
L.B = Collapse (E,B) by A2,A3,A12;
hence thesis by A13,ZFMISC_1:25;
end;
hence thesis by A5,A10;
end;
theorem
(not ex d1 st d1 in d) iff d in Collapse (E,{})
proof
A1: Collapse (E,{}) = { d9 : for d1 st d1 in d9 ex B st B in {} & d1 in
Collapse (E,B) } by Th1;
thus (not ex d1 st d1 in d) implies d in Collapse (E,{})
proof
assume not ex d1 st d1 in d;
then for d1 st d1 in d ex B st B in {} & d1 in Collapse (E,B);
hence thesis by A1;
end;
assume d in Collapse (E,{});
then
A2: ex d9 st d9 = d & for d1 st d1 in d9 ex B st B in {} & d1 in Collapse (E
,B) by A1;
given d1 such that
A3: d1 in d;
ex B st B in {} & d1 in Collapse (E,B) by A3,A2;
hence contradiction;
end;
theorem
d /\ E c= Collapse (E,A) iff d in Collapse (E,succ A)
proof
A1: Collapse (E,succ A) = { d9 : for d1 st d1 in d9 ex B st B in succ A & d1
in Collapse (E,B) } by Th1;
thus d /\ E c= Collapse (E,A) implies d in Collapse (E,succ A)
proof
assume
A2: for a being object st a in d /\ E holds a in Collapse (E,A);
now
let d1;
assume d1 in d;
then d1 in d /\ E by XBOOLE_0:def 4;
then d1 in Collapse (E,A) by A2;
hence ex B st B in succ A & d1 in Collapse (E,B) by ORDINAL1:6;
end;
hence thesis by A1;
end;
assume d in Collapse (E,succ A);
then
A3: ex e1 being Element of E st e1 = d & for d1 st d1 in e1 ex B st B in
succ A & d1 in Collapse (E,B) by A1;
let a be object;
assume
A4: a in d /\ E;
then reconsider e = a as Element of E by XBOOLE_0:def 4;
a in d by A4,XBOOLE_0:def 4;
then consider B such that
A5: B in succ A and
A6: e in Collapse (E,B) by A3;
A7: now
Collapse (E,B) = { d9 : for d1 st d1 in d9 ex C st C in B & d1 in
Collapse (E,C) } by Th1;
then
A8: ex d9 st d9 = e & for d1 st d1 in d9 ex C st C in B & d1 in Collapse
(E,C) by A6;
let d1;
assume d1 in e;
then consider C such that
A9: C in B & d1 in Collapse (E,C) by A8;
take C;
B c= A by A5,ORDINAL1:22;
hence C in A & d1 in Collapse (E,C) by A9;
end;
Collapse (E,A) = { d9 : for d1 st d1 in d9 ex B st B in A & d1 in
Collapse (E,B) } by Th1;
hence thesis by A7;
end;
theorem Th4:
A c= B implies Collapse (E,A) c= Collapse (E,B)
proof
assume
A1: A c= B;
let x be object;
assume x in Collapse (E,A);
then
x in { d : for d1 st d1 in d ex B st B in A & d1 in Collapse (E,B) } by Th1;
then consider d such that
A2: d = x and
A3: for d1 st d1 in d ex B st B in A & d1 in Collapse (E,B);
for d1 st d1 in d ex C st C in B & d1 in Collapse (E,C)
proof
let d1;
assume d1 in d;
then consider C such that
A4: C in A & d1 in Collapse (E,C) by A3;
take C;
thus thesis by A1,A4;
end;
then x in { d9 : for d1 st d1 in d9 ex C st C in B & d1 in Collapse (E,C) }
by A2;
hence thesis by Th1;
end;
theorem Th5:
ex A st d in Collapse (E,A)
proof
defpred P[object] means not ex A st $1 in Collapse (E,A);
defpred R[object,object] means
ex A st $2 = A & $1 in Collapse(E,A) & for B st $1
in Collapse(E,B) holds A c= B;
consider X such that
A1: for x being object holds x in X iff x in E & P[x] from XBOOLE_0:sch 1;
now
given x such that
A2: x in X;
consider m being set such that
A3: m in X and
A4: X misses m by A2,XREGULAR:1;
reconsider m as Element of E by A1,A3;
A5: now
let x be object;
defpred Q[Ordinal] means x in Collapse(E,$1);
assume
A6: x in m /\ E;
then x in m by XBOOLE_0:def 4;
then
A7: not x in X by A4,XBOOLE_0:3;
x in E by A6,XBOOLE_0:def 4;
then
A8: ex A st Q[A] by A1,A7;
ex A st Q[A] & for B st Q[B] holds A c= B from ORDINAL1:sch 1(A8 );
hence ex y being object st R[x,y];
end;
consider f such that
A9: dom f = m /\ E & for x being object st x in m /\ E holds R[x,f.x] from
CLASSES1:sch 1(A5);
y in rng f implies y is Ordinal
proof
assume y in rng f;
then consider x being object such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 3;
ex A st f.x = A & x in Collapse (E,A) & for B st x in Collapse (E,B
) holds A c= B by A9,A10;
hence thesis by A11;
end;
then consider A such that
A12: rng f c= A by ORDINAL1:24;
for d st d in m ex B st B in A & d in Collapse (E,B)
proof
let d;
assume d in m;
then
A13: d in m /\ E by XBOOLE_0:def 4;
then consider B such that
A14: f.d = B and
A15: d in Collapse (E,B) and
for C st d in Collapse (E,C) holds B c= C by A9;
take B;
B in rng f by A9,A13,A14,FUNCT_1:def 3;
hence thesis by A12,A15;
end;
then m in { d9 : for d st d in d9 ex B st B in A & d in Collapse (E,B) };
then m in Collapse (E,A) by Th1;
hence contradiction by A1,A3;
end;
hence thesis by A1;
end;
theorem Th6:
d9 in d & d in Collapse (E,A) implies d9 in Collapse (E,A) & ex B
st B in A & d9 in Collapse (E,B)
proof
assume that
A1: d9 in d and
A2: d in Collapse (E,A);
d in { d1 : for d st d in d1 ex B st B in A & d in Collapse (E,B) } by A2,Th1
;
then
ex d1 st d = d1 & for d st d in d1 ex B st B in A & d in Collapse (E,B);
then consider B such that
A3: B in A and
A4: d9 in Collapse (E,B) by A1;
Collapse (E,B) c= Collapse (E,A) by Th4,A3,ORDINAL1:def 2;
hence d9 in Collapse (E,A) by A4;
thus thesis by A3,A4;
end;
theorem Th7:
Collapse (E,A) c= E
proof
let x be object;
assume x in Collapse (E,A);
then
x in { d : for d1 st d1 in d ex B st B in A & d1 in Collapse (E,B) } by Th1;
then
ex d st x = d & for d1 st d1 in d ex B st B in A & d1 in Collapse (E,B);
hence thesis;
end;
theorem Th8:
ex A st E = Collapse (E,A)
proof
defpred R[object,object] means
ex A st $2 = A & $1 in Collapse(E,A) & for B st $1
in Collapse(E,B) holds A c= B;
A1: now
let x be object;
assume x in E;
then reconsider d = x as Element of E;
defpred Q[Ordinal] means d in Collapse(E,$1);
A2: ex A st Q[A] by Th5;
ex A st Q[A] & for B st Q[B] holds A c= B from ORDINAL1:sch 1 (A2);
hence ex y being object st R[x,y];
end;
consider f such that
A3: dom f = E &
for x being object st x in E holds R[x,f.x] from CLASSES1:sch 1(A1);
x in rng f implies x is Ordinal
proof
assume x in rng f;
then consider y being object such that
A4: y in dom f and
A5: x = f.y by FUNCT_1:def 3;
ex A st f.y = A & y in Collapse (E,A) & for C st y in Collapse (E,C)
holds A c= C by A3,A4;
hence thesis by A5;
end;
then consider A such that
A6: rng f c= A by ORDINAL1:24;
take A;
thus for x being object holds x in E implies x in Collapse (E,A)
proof let x be object;
assume
A7: x in E;
then consider B such that
A8: f.x = B and
A9: x in Collapse (E,B) and
for C st x in Collapse (E,C) holds B c= C by A3;
B in rng f by A3,A7,A8,FUNCT_1:def 3;
then Collapse (E,B) c= Collapse (E,A) by Th4,A6,ORDINAL1:def 2;
hence thesis by A9;
end;
thus thesis by Th7;
end;
theorem Th9:
ex f st dom f = E & for d holds f.d = f.:d
proof
defpred Q[Ordinal,Function,non empty set] means dom $2 = Collapse ($3,$1) &
for d st d in Collapse ($3,$1) holds $2.d = $2.:d;
defpred TI[Ordinal] means for f1,f2 st Q[$1,f1,E] & Q[$1,f2,E] holds f1 = f2;
defpred MAIN[Ordinal] means ex f st Q[$1,f,E];
A1: A c= B & Q[B,f,E] implies Q[A,f|Collapse (E,A),E]
proof
assume that
A2: A c= B and
A3: dom f = Collapse (E,B) and
A4: for d st d in Collapse (E,B) holds f.d = f.:d;
A5: Collapse (E,A) c= Collapse (E,B) by A2,Th4;
thus dom(f|Collapse (E,A)) = Collapse (E,A) by A2,A3,Th4,RELAT_1:62;
let d such that
A6: d in Collapse (E,A);
for x being object holds x in f.:d implies x in f|Collapse (E,A).:d
proof let x be object;
A7: dom(f|Collapse (E,A)) = Collapse (E,A) by A2,A3,Th4,RELAT_1:62;
assume x in f.:d;
then consider z being object such that
A8: z in dom f and
A9: z in d and
A10: x = f.z by FUNCT_1:def 6;
dom f c= E by A3,Th7;
then reconsider d1 = z as Element of E by A8;
A11: d1 in Collapse (E,A) by A6,A9,Th6;
then f|Collapse (E,A).z = f.z by FUNCT_1:49;
hence thesis by A9,A10,A11,A7,FUNCT_1:def 6;
end;
then
A12: f.:d c= f|Collapse (E,A).:d;
f|Collapse (E,A).:d c= f.:d by RELAT_1:128;
then
A13: f.:d = f|Collapse (E,A).:d by A12;
thus f|Collapse (E,A).d = f.d by A6,FUNCT_1:49
.= f|Collapse (E,A).:d by A4,A5,A6,A13;
end;
A14: now
let A such that
A15: for B st B in A holds TI[B];
thus TI[A]
proof
let f1,f2 such that
A16: Q[A,f1,E] and
A17: Q[A,f2,E];
now
let x be object such that
A18: x in Collapse (E,A);
Collapse (E,A) c= E by Th7;
then reconsider d = x as Element of E by A18;
A19: f1.:d = f2.:d
proof
thus for y being object holds y in f1.:d implies y in f2.:d
proof let y be object;
assume y in f1.:d;
then consider z being object such that
A20: z in dom f1 and
A21: z in d and
A22: y = f1.z by FUNCT_1:def 6;
dom f1 c= E by A16,Th7;
then reconsider d1 = z as Element of E by A20;
consider B such that
A23: B in A and
A24: d1 in Collapse (E,B) by A18,A21,Th6;
B c= A by A23,ORDINAL1:def 2;
then ( Q[B,f1|Collapse (E,B),E])& Q[B,f2|Collapse (E,B),E] by A1
,A16,A17;
then
A25: f1|Collapse (E,B) = f2|Collapse (E,B) by A15,A23;
f1.d1 = f1|Collapse (E,B).d1 by A24,FUNCT_1:49
.= f2.d1 by A24,A25,FUNCT_1:49;
hence thesis by A16,A17,A20,A21,A22,FUNCT_1:def 6;
end;
let y be object;
assume y in f2.:d;
then consider z being object such that
A26: z in dom f2 and
A27: z in d and
A28: y = f2.z by FUNCT_1:def 6;
dom f2 c= E by A17,Th7;
then reconsider d1 = z as Element of E by A26;
consider B such that
A29: B in A and
A30: d1 in Collapse (E,B) by A18,A27,Th6;
B c= A by A29,ORDINAL1:def 2;
then
( Q[B,f1|Collapse (E,B),E])& Q[B,f2|Collapse (E,B),E] by A1,A16,A17;
then
A31: f1|Collapse (E,B) = f2|Collapse (E,B) by A15,A29;
f1.d1 = f1|Collapse (E,B).d1 by A30,FUNCT_1:49
.= f2.d1 by A30,A31,FUNCT_1:49;
hence thesis by A16,A17,A26,A27,A28,FUNCT_1:def 6;
end;
f1.d = f1.:d by A16,A18;
hence f1.x = f2.x by A17,A18,A19;
end;
hence thesis by A16,A17,FUNCT_1:2;
end;
end;
A32: for A holds TI[A] from ORDINAL1:sch 2(A14);
A33: for A st for B st B in A holds MAIN[B] holds MAIN[A]
proof
let A;
assume for B st B in A ex f st Q[B,f,E];
defpred P[object,object] means
ex d,e being set st d = $1 & e = $2 & for x holds x in e
iff ex d1,B,f st d1 in d & B in A & d1 in Collapse (E,B) & Q[B,f,E] & x = f.d1;
A34: for x being object st x in Collapse (E,A) ex y being object st P[x,y]
proof
A35: Collapse (E,A) c= E by Th7;
let x be object;
assume x in Collapse (E,A);
then reconsider d = x as Element of E by A35;
defpred R[object,object] means
ex B,f st B in A & $1 in Collapse (E,B) & Q[B,f,E] & $2 = f.$1;
A36: for x,y,z being object st R[x,y] & R[x,z] holds y = z
proof
let x,y,z be object;
given B1 being Ordinal, f1 such that
B1 in A and
A37: x in Collapse (E,B1) and
A38: Q[B1,f1,E] and
A39: y = f1.x;
given B2 being Ordinal, f2 such that
B2 in A and
A40: x in Collapse (E,B2) and
A41: Q[B2,f2,E] and
A42: z = f2.x;
A43: now
assume B2 c= B1;
then Q[B2,f1|Collapse (E,B2),E] by A1,A38;
then f1|Collapse (E,B2) = f2 by A32,A41;
hence thesis by A39,A40,A42,FUNCT_1:49;
end;
now
assume B1 c= B2;
then Q[B1,f2|Collapse (E,B1),E] by A1,A41;
then f2|Collapse (E,B1) = f1 by A32,A38;
hence thesis by A37,A39,A42,FUNCT_1:49;
end;
hence thesis by A43;
end;
consider X such that
A44: for y being object holds y in X iff
ex x being object st x in d & R[x,y] from TARSKI:sch 1(A36);
take y = X,d,X;
thus d = x;
thus y = X;
let x;
thus x in X implies ex d1,B,f st d1 in d & B in A & d1 in Collapse (E,B)
& Q[B,f,E] & x = f.d1
proof
assume x in X;
then consider y being object such that
A45: y in d and
A46: ex B,f st B in A & y in Collapse (E,B) & Q[B,f,E] & x = f.y by A44;
consider B,f such that
A47: B in A and
A48: y in Collapse (E,B) and
A49: ( Q[B,f,E])& x = f.y by A46;
Collapse (E,B) c= E by Th7;
then reconsider d1 = y as Element of E by A48;
take d1,B,f;
thus thesis by A45,A47,A48,A49;
end;
given d1,B,f such that
A50: d1 in d & B in A & d1 in Collapse (E,B) & Q[B,f,E] & x = f.d1;
thus thesis by A44,A50;
end;
consider f such that
A51: dom f = Collapse (E,A) &
for x being object st x in Collapse (E,A) holds P[x,f.x]
from CLASSES1:sch 1(A34);
defpred TI[Ordinal] means $1 c= A implies Q[$1,f|Collapse(E,$1),E];
A52: for B st for C st C in B holds TI[C] holds TI[B]
proof
let B such that
A53: for C st C in B holds TI[C];
assume
A54: B c= A;
then
A55: Collapse (E,B) c= Collapse (E,A) by Th4;
thus
A56: dom(f|Collapse (E,B)) = Collapse (E,B) by A51,A54,Th4,RELAT_1:62;
let d;
assume
A57: d in Collapse (E,B);
then f|Collapse (E,B).d = f.d by FUNCT_1:49;
then consider d9,e being set such that
A58: d9 = d and
A59: e = f|Collapse (E,B).d and
A60: for x holds x in e iff ex d1,B,f st d1 in d9 & B in A &
d1 in Collapse (E,B) & Q[B,f,E] & x = f.d1 by A51,A55,A57;
set X = f|Collapse (E,B).d;
A61: X c= f|Collapse (E,B).:d
proof
let x be object;
assume x in X;
then consider d1,C,h such that
A62: d1 in d9 and
C in A and
A63: d1 in Collapse (E,C) and
A64: Q[C,h,E] and
A65: x = h.d1 by A60,A59;
consider C9 being Ordinal such that
A66: C9 in B and
A67: d1 in Collapse (E,C9) by A57,A58,A62,Th6;
A68: for C,h st C c= C9 & Q[C,h,E] & d1 in Collapse (E,C) & x = h.d1
holds thesis
proof
let C,h;
assume that
A69: C c= C9 and
A70: Q[C,h,E] and
A71: d1 in Collapse (E,C) and
A72: x = h.d1;
A73: C in B by A66,A69,ORDINAL1:12;
then C c= A by A54,ORDINAL1:def 2;
then Q[C,f|Collapse (E,C),E] by A53,A73;
then
A74: f|Collapse (E,C) = h by A32,A70;
A75: Collapse (E,C) c= Collapse (E,B) by Th4,A73,ORDINAL1:def 2;
then f|Collapse (E,C) = f|Collapse (E,B)|Collapse (E,C) by FUNCT_1:51
;
then h.d1 = f|Collapse (E,B).d1 by A71,A74,FUNCT_1:49;
hence thesis by A56,A58,A62,A71,A72,A75,FUNCT_1:def 6;
end;
C9 c= C implies thesis
proof
assume C9 c= C;
then
A76: Q[C9,h|Collapse (E,C9),E] by A1,A64;
h.d1 = h|Collapse (E,C9).d1 by A67,FUNCT_1:49;
hence thesis by A65,A67,A68,A76;
end;
hence thesis by A63,A64,A65,A68;
end;
f|Collapse (E,B).:d c= X
proof
let x be object;
assume x in f|Collapse (E,B).:d;
then consider y being object such that
A77: y in dom(f|Collapse (E,B)) and
A78: y in d and
A79: x = f|Collapse (E,B).y by FUNCT_1:def 6;
Collapse (E,B) c= E by Th7;
then reconsider d1 = y as Element of E by A56,A77;
consider C such that
A80: C in B and
A81: d1 in Collapse (E,C) by A57,A78,Th6;
Collapse (E,C) c= Collapse (E,B) by Th4,A80,ORDINAL1:def 2;
then f|Collapse (E,B)|Collapse (E,C) = f|Collapse (E,C) by FUNCT_1:51;
then
A82: f|Collapse (E,C).y = f|Collapse (E,B).y by A81,FUNCT_1:49;
C c= A by A54,A80,ORDINAL1:def 2;
then Q[C,f|Collapse (E,C),E] by A53,A80;
hence thesis by A54,A58,A60,A78,A79,A80,A81,A82,A59;
end;
hence thesis by A61;
end;
A83: for B holds TI[B] from ORDINAL1:sch 2(A52);
take f;
f|dom f = f by RELAT_1:68;
hence thesis by A51,A83;
end;
A84: MAIN[A] from ORDINAL1:sch 2 (A33);
consider A such that
A85: E = Collapse (E,A) by Th8;
consider f such that
A86: Q[A,f,E] by A84;
take f;
thus dom f = E by A85,A86;
let d;
thus thesis by A85,A86;
end;
:: Definition of epsilon-isomorphism of two sets
definition
let f,X,Y;
pred f is_epsilon-isomorphism_of X,Y means
dom f = X & rng f = Y & f is
one-to-one & for x,y st x in X & y in X holds (ex Z st Z = y & x in Z) iff ex Z
st f.y = Z & f.x in Z;
end;
definition
let X,Y;
pred X,Y are_epsilon-isomorphic means
ex f st f is_epsilon-isomorphism_of X, Y;
end;
theorem Th10:
(dom f = E & for d holds f.d = f.:d) implies rng f is epsilon-transitive
proof
assume that
A1: dom f = E and
A2: for d holds f.d = f.:d;
let Y;
assume Y in rng f;
then consider b being object such that
A3: b in dom f and
A4: Y = f.b by FUNCT_1:def 3;
reconsider d = b as Element of E by A1,A3;
A5: f.d = f.:d by A2;
let a be object;
assume a in Y;
then ex c being object st c in dom f & c in d & a = f.c
by A4,A5,FUNCT_1:def 6;
hence thesis by FUNCT_1:def 3;
end;
reserve f,g,h for (Function of VAR,E),
u,v,w for (Element of E),
x for Variable,
a,b,c for object;
theorem Th11:
E |= the_axiom_of_extensionality implies for u,v st for w holds
w in u iff w in v holds u = v
proof
assume
A1: E |= the_axiom_of_extensionality;
All(x.0,All(x.1,All(x.2,x.2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1))
= All(x.0,x.1,All(x.2,x.2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1) by
ZF_LANG:7;
then
A2: E |= All(x.1,All(x.2,x.2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1) by A1,
ZF_MODEL:23,def 6;
A3: for f st for g st for x st g.x <> f.x holds x.2 = x holds g.x.2 in g.x.0
iff g.x.2 in g.x.1 holds f.x.0 = f.x.1
proof
let f such that
A4: for g st for x st g.x <> f.x holds x.2 = x holds g.x.2 in g.x.0
iff g.x.2 in g.x.1;
A5: now
let g such that
A6: for x st g.x <> f.x holds x.2 = x;
A7: g.x.2 in g.x.1 iff E,g |= x.2 'in' x.1 by ZF_MODEL:13;
g.x.2 in g.x.0 iff E,g |= x.2 'in' x.0 by ZF_MODEL:13;
hence E,g |= x.2 'in' x.0 <=> x.2 'in' x.1 by A4,A6,A7,ZF_MODEL:19;
end;
E,f |= All(x.2,x.2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1
by A2,ZF_MODEL:23,def 5;
then E,f |= All(x.2,x.2 'in' x.0 <=> x.2 'in' x.1) implies E,f |= x.0 '='
x.1 by ZF_MODEL:18;
hence thesis by A5,ZF_MODEL:12,16;
end;
for X,Y being Element of E st for Z being Element of E holds Z in X iff
Z in Y holds X = Y
proof
set g = the (Function of VAR,E);
let X,Y be Element of E such that
A8: for Z being Element of E holds Z in X iff Z in Y;
set g0 = g+*(x.0,X);
A9: g0.x.0 = X by FUNCT_7:128;
A10: x.0 = 5+0 & x.1 = 5+1 by ZF_LANG:def 2;
set f = g0+*(x.1,Y);
A11: x.2 = 5+2 by ZF_LANG:def 2;
A12: for h st for x st h.x <> f.x holds x.2 = x holds h.x.2 in h.x.0 iff h
.x.2 in h.x.1
proof
let h;
assume for x st h.x <> f.x holds x.2 = x;
then
A13: h.x.0 = f.x.0 & h.x.1 = f.x.1 by A10,A11;
h.x.2 in X iff h.x.2 in Y by A8;
hence thesis by A9,A13,FUNCT_7:32,128;
end;
f.x.1 = Y & f.x.0 = g0.x.0 by A10,FUNCT_7:32,128;
hence thesis by A3,A9,A12;
end;
hence thesis;
end;
::$N Contraction Lemma
theorem
E |= the_axiom_of_extensionality implies ex X st X is
epsilon-transitive & E,X are_epsilon-isomorphic
proof
consider f being Function such that
A1: dom f = E and
A2: for d holds f.d = f.:d by Th9;
assume
A3: E |= the_axiom_of_extensionality;
A4: now
defpred P[Ordinal] means ex d1,d2 st d1 in Collapse(E,$1) & d2 in Collapse
(E,$1) & f.d1 = f.d2 & d1 <> d2;
given a,b being object such that
A5: a in dom f & b in dom f and
A6: f.a = f.b & a <> b;
reconsider d1 = a, d2 = b as Element of E by A1,A5;
consider A1 being Ordinal such that
A7: d1 in Collapse (E,A1) by Th5;
consider A2 being Ordinal such that
A8: d2 in Collapse (E,A2) by Th5;
A1 c= A2 or A2 c= A1;
then
Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (E,
A1) by Th4;
then
A9: ex A st P[A] by A6,A7,A8;
consider A such that
A10: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1 (A9);
consider d1,d2 such that
A11: d1 in Collapse (E,A) and
A12: d2 in Collapse (E,A) and
A13: f.d1 = f.d2 and
A14: d1 <> d2 by A10;
consider w such that
A15: not(w in d1 iff w in d2) by A3,A14,Th11;
A16: f.d1 = f.:d1 & f.d2 = f.:d2 by A2;
A17: now
assume that
A18: w in d2 and
A19: not w in d1;
consider A1 being Ordinal such that
A20: A1 in A & w in Collapse(E,A1) by A12,A18,Th6;
f.w in f.:d2 by A1,A18,FUNCT_1:def 6;
then consider a being object such that
A21: a in dom f and
A22: a in d1 and
A23: f.w = f.a by A13,A16,FUNCT_1:def 6;
reconsider v = a as Element of E by A1,A21;
consider A2 being Ordinal such that
A24: A2 in A & v in Collapse(E,A2) by A11,A22,Th6;
A1 c= A2 or A2 c= A1;
then
Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (
E,A1) by Th4;
hence contradiction by A10,A19,A22,A23,A20,A24,ORDINAL1:5;
end;
now
assume that
A25: w in d1 and
A26: not w in d2;
consider A1 being Ordinal such that
A27: A1 in A & w in Collapse(E,A1) by A11,A25,Th6;
f.w in f.:d1 by A1,A25,FUNCT_1:def 6;
then consider a being object such that
A28: a in dom f and
A29: a in d2 and
A30: f.w = f.a by A13,A16,FUNCT_1:def 6;
reconsider v = a as Element of E by A1,A28;
consider A2 being Ordinal such that
A31: A2 in A & v in Collapse(E,A2) by A12,A29,Th6;
A1 c= A2 or A2 c= A1;
then
Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (
E,A1) by Th4;
hence contradiction by A10,A26,A29,A30,A27,A31,ORDINAL1:5;
end;
hence contradiction by A15,A17;
end;
take X = rng f;
thus X is epsilon-transitive by A1,A2,Th10;
take f;
thus dom f = E & rng f = X by A1;
thus f is one-to-one by A4,FUNCT_1:def 4;
let a,b;
assume that
A32: a in E and
A33: b in E;
reconsider d2 = b as Element of E by A33;
thus (ex Z st Z = b & a in Z) implies ex Z st Z = f.b & f.a in Z
proof
given Z such that
A34: Z = b & a in Z;
A35: f.d2 = f.: d2 by A2;
f.a in f.:d2 by A1,A32,A34,FUNCT_1:def 6;
hence thesis by A35;
end;
given Z such that
A36: Z = f.b & f.a in Z;
f.d2 = f.:d2 by A2;
then consider c being object such that
A37: c in dom f and
A38: c in d2 and
A39: f.a = f.c by A36,FUNCT_1:def 6;
a = c by A1,A4,A32,A37,A39;
hence thesis by A38;
end;