zf_colla.miz
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 holds ex C st C
in (
dom $1) & d1
in (
union
{($1
. C)}) };
::
ZF_COLLA:def1
func
Collapse (E,A) ->
set means
:
Def1: ex L st it
= { d : for d1 st d1
in d holds 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 holds 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 holds ex B st B
in (
dom L) & d1
in (
union
{(L
. B)}) }, L;
thus x
= { d : for d1 st d1
in d holds 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 holds 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 holds 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 holds 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 holds 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 ::
ZF_COLLA:1
Th1: (
Collapse (E,A))
= { d : for d1 st d1
in d holds 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 holds ex C st C
in (
dom $1) & d1
in (
union
{($1
. C)}) };
deffunc
F(
Ordinal) = (
Collapse (E,$1));
A1: for x be
object st x
in A holds ex y be
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 be
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 holds for x be
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(|) by
Def1;
for B st B
in (
dom L) holds (L
. B)
=
H(|) from
ORDINAL1:sch 5(
A4,
A3);
then
A5: (
Collapse (E,A))
= { d : for d1 st d1
in d holds 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 holds 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 holds ex B st B
in (
dom L) & d1
in (
union
{(L
. B)});
for d1 st d1
in d holds 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 holds 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 holds 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 holds 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 holds ex B st B
in A & d
in (
Collapse (E,B));
for d st d
in d1 holds 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 ::
ZF_COLLA:2
( not ex d1 st d1
in d) iff d
in (
Collapse (E,
{} ))
proof
A1: (
Collapse (E,
{} ))
= { d9 : for d1 st d1
in d9 holds 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 holds 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 holds 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 ::
ZF_COLLA:3
(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 holds 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 be
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 be
Element of E st e1
= d & for d1 st d1
in e1 holds 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 holds 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 holds 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 holds ex B st B
in A & d1
in (
Collapse (E,B)) } by
Th1;
hence thesis by
A7;
end;
theorem ::
ZF_COLLA:4
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 holds 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 holds ex B st B
in A & d1
in (
Collapse (E,B));
for d1 st d1
in d holds 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 holds ex C st C
in B & d1
in (
Collapse (E,C)) } by
A2;
hence thesis by
Th1;
end;
theorem ::
ZF_COLLA:5
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 be
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 be
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 be
object st
R[x, y];
end;
consider f such that
A9: (
dom f)
= (m
/\ E) & for x be
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 be
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 holds 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 holds 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 ::
ZF_COLLA:6
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 holds 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 holds 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 ::
ZF_COLLA:7
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 holds 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 holds ex B st B
in A & d1
in (
Collapse (E,B));
hence thesis;
end;
theorem ::
ZF_COLLA:8
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 be
object st
R[x, y];
end;
consider f such that
A3: (
dom f)
= E & for x be
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 be
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 be
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 ::
ZF_COLLA:9
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 be
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 be
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 be
object holds y
in (f1
.: d) implies y
in (f2
.: d)
proof
let y be
object;
assume y
in (f1
.: d);
then
consider z be
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 be
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 holds ex f st
Q[B, f, E];
defpred
P[
object,
object] means ex d,e be
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 be
object st x
in (
Collapse (E,A)) holds ex y be
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 be
object st
R[x, y] &
R[x, z] holds y
= z
proof
let x,y,z be
object;
given B1 be
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 be
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 be
object holds y
in X iff ex x be
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 be
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 be
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 be
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 be
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 be
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
let f, X, Y;
::
ZF_COLLA:def2
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;
::
ZF_COLLA:def3
pred X,Y
are_epsilon-isomorphic means ex f st f
is_epsilon-isomorphism_of (X,Y);
end
theorem ::
ZF_COLLA:10
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 be
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 be
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 ::
ZF_COLLA:11
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,
ZF_MODEL: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,
ZF_MODEL: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,
ZF_MODEL: 16;
end;
for X,Y be
Element of E st for Z be
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 be
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,
FUNCT_7: 128;
end;
(f
. (
x. 1))
= Y & (f
. (
x.
0 ))
= (g0
. (
x.
0 )) by
A10,
FUNCT_7: 32,
FUNCT_7: 128;
hence thesis by
A3,
A9,
A12;
end;
hence thesis;
end;
::$Notion-Name
theorem ::
ZF_COLLA:12
E
|=
the_axiom_of_extensionality implies ex X st X is
epsilon-transitive & (E,X)
are_epsilon-isomorphic
proof
consider f be
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 be
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 be
Ordinal such that
A7: d1
in (
Collapse (E,A1)) by
Th5;
consider A2 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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;