let A be Ordinal; ex B being Ordinal st
( B c= card A & A is_cofinal_with B )
set M = card A;
card A,A are_equipotent
by CARD_1:def 2;
then consider f being Function such that
A1:
f is one-to-one
and
A2:
dom f = card A
and
A3:
rng f = A
by WELLORD2:def 4;
defpred S1[ set ] means not f . $1 in Union (f | $1);
reconsider f = f as Sequence by A2, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A3, ORDINAL2:def 4;
consider X being set such that
A4:
for x being set holds
( x in X iff ( x in card A & S1[x] ) )
from XFAMILY:sch 1();
set R = RelIncl X;
set B = order_type_of (RelIncl X);
take
order_type_of (RelIncl X)
; ( order_type_of (RelIncl X) c= card A & A is_cofinal_with order_type_of (RelIncl X) )
A5:
X c= card A
by A4;
hence
order_type_of (RelIncl X) c= card A
by WELLORD2:14; A is_cofinal_with order_type_of (RelIncl X)
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
RelIncl X is well-ordering
by A5, WELLORD2:8;
then
RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic
by WELLORD2:def 2;
then
( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic )
by WELLORD1:40, WELLORD2:8;
then A6:
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X
by WELLORD1:def 9;
then A7:
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one
by WELLORD1:def 7;
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X)
by WELLORD2:def 1;
then A8:
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X)
by A6, WELLORD1:def 7;
field (RelIncl X) = X
by WELLORD2:def 1;
then A9:
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X
by A6, WELLORD1:def 7;
reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as Sequence by A8, ORDINAL1:def 7;
reconsider phi = phi as Ordinal-Sequence by A5, A9, ORDINAL2:def 4;
A10:
dom (f * phi) = order_type_of (RelIncl X)
by A2, A5, A8, A9, RELAT_1:27;
then reconsider xi = f * phi as Sequence by ORDINAL1:def 7;
rng (f * phi) c= A
by A3, RELAT_1:26;
then reconsider xi = xi as Ordinal-Sequence by ORDINAL2:def 4;
take
xi
; ORDINAL2:def 17 ( dom xi = order_type_of (RelIncl X) & rng xi c= A & xi is increasing & A = sup xi )
thus
( dom xi = order_type_of (RelIncl X) & rng xi c= A )
by A2, A3, A5, A8, A9, RELAT_1:26, RELAT_1:27; ( xi is increasing & A = sup xi )
thus
xi is increasing
A = sup xiproof
let a,
b be
Ordinal;
ORDINAL2:def 12 ( not a in b or not b in dom xi or xi . a in xi . b )
assume that A11:
a in b
and A12:
b in dom xi
;
xi . a in xi . b
A13:
a in dom xi
by A11, A12, ORDINAL1:10;
then A14:
phi . a in X
by A8, A9, A10, FUNCT_1:def 3;
a <> b
by A11;
then A15:
phi . a <> phi . b
by A8, A7, A10, A12, A13;
reconsider a9 =
phi . a,
b9 =
phi . b as
Ordinal ;
reconsider a99 =
f . a9,
b99 =
f . b9 as
Ordinal ;
A16:
phi . b in X
by A8, A9, A10, A12, FUNCT_1:def 3;
then
not
b99 in Union (f | b9)
by A4;
then A17:
Union (f | b9) c= b99
by ORDINAL1:16;
a c= b
by A11, ORDINAL1:def 2;
then
[a,b] in RelIncl (order_type_of (RelIncl X))
by A10, A12, A13, WELLORD2:def 1;
then
[(phi . a),(phi . b)] in RelIncl X
by A6, WELLORD1:def 7;
then
a9 c= b9
by A14, A16, WELLORD2:def 1;
then
a9 c< b9
by A15;
then
a9 in b9
by ORDINAL1:11;
then
a99 c= Union (f | b9)
by A2, A5, A14, FUNCT_1:50, ZFMISC_1:74;
then A18:
a99 c= b99
by A17;
a99 <> b99
by A1, A2, A5, A15, A14, A16;
then A19:
a99 c< b99
by A18;
(
a99 = xi . a &
b99 = xi . b )
by A11, A12, FUNCT_1:12, ORDINAL1:10;
hence
xi . a in xi . b
by A19, ORDINAL1:11;
verum
end;
thus
A c= sup xi
XBOOLE_0:def 10 sup xi c= Aproof
let x be
Ordinal;
ORDINAL1:def 5 ( not x in A or x in sup xi )
assume
x in A
;
x in sup xi
then consider y being
object such that A20:
y in dom f
and A21:
x = f . y
by A3, FUNCT_1:def 3;
reconsider x9 =
x,
y =
y as
Ordinal by A20;
now x in sup xiper cases
( not f . y in Union (f | y) or f . y in Union (f | y) )
;
suppose A23:
f . y in Union (f | y)
;
x in sup xidefpred S2[
Ordinal]
means ( $1
in y &
f . y in f . $1 );
consider z being
object such that A24:
z in dom (f | y)
and A25:
f . y in (f | y) . z
by A23, Th2;
reconsider z =
z as
Ordinal by A24;
A26:
(f | y) . z = f . z
by A24, FUNCT_1:47;
dom (f | y) = (dom f) /\ y
by RELAT_1:61;
then
z in y
by A24, XBOOLE_0:def 4;
then A27:
ex
C being
Ordinal st
S2[
C]
by A25, A26;
consider C being
Ordinal such that A28:
(
S2[
C] & ( for
B being
Ordinal st
S2[
B] holds
C c= B ) )
from ORDINAL1:sch 1(A27);
now ( C in card A & not f . C in Union (f | C) )thus
C in card A
by A2, A20, A28, ORDINAL1:10;
not f . C in Union (f | C)assume
f . C in Union (f | C)
;
contradictionthen consider a being
object such that A29:
a in dom (f | C)
and A30:
f . C in (f | C) . a
by Th2;
reconsider a =
a as
Ordinal by A29;
reconsider fa =
(f | C) . a,
fy =
f . y as
Ordinal ;
f . a = fa
by A29, FUNCT_1:47;
then A31:
fy in f . a
by A28, A30, ORDINAL1:10;
dom (f | C) = (dom f) /\ C
by RELAT_1:61;
then A32:
a in C
by A29, XBOOLE_0:def 4;
then
a in y
by A28, ORDINAL1:10;
hence
contradiction
by A28, A32, A31, ORDINAL1:5;
verum end; then
C in X
by A4;
then consider z being
object such that A33:
z in order_type_of (RelIncl X)
and A34:
C = phi . z
by A8, A9, FUNCT_1:def 3;
reconsider z =
z as
Ordinal by A33;
reconsider xz =
xi . z as
Ordinal ;
xz in rng xi
by A10, A33, FUNCT_1:def 3;
then A35:
xz in sup xi
by ORDINAL2:19;
x9 in xz
by A10, A21, A28, A33, A34, FUNCT_1:12;
hence
x in sup xi
by A35, ORDINAL1:10;
verum end; end; end;
hence
x in sup xi
;
verum
end;
sup A = A
by ORDINAL2:18;
hence
sup xi c= A
by A3, ORDINAL2:22, RELAT_1:26; verum