defpred S1[ Ordinal] means InvLexOrder $1 is well-ordering ;
A1:
now for o being Ordinal st ( for n being Ordinal st n in o holds
S1[n] ) holds
S1[o]let o be
Ordinal;
( ( for n being Ordinal st n in o holds
S1[n] ) implies S1[o] )assume A2:
for
n being
Ordinal st
n in o holds
S1[
n]
;
S1[o]set ilo =
InvLexOrder o;
A3:
InvLexOrder o is_strongly_connected_in Bags o
by Def5;
then
InvLexOrder o is_reflexive_in Bags o
;
then A4:
field (InvLexOrder o) = Bags o
by PARTIT_2:9;
A5:
now InvLexOrder o is well_founded assume
not
InvLexOrder o is
well_founded
;
contradictionthen A6:
not
InvLexOrder o is_well_founded_in Bags o
by A4, WELLORD1:3;
set R =
RelStr(#
(Bags o),
(InvLexOrder o) #);
set ir = the
InternalRel of
RelStr(#
(Bags o),
(InvLexOrder o) #);
not
RelStr(#
(Bags o),
(InvLexOrder o) #) is
well_founded
by A6;
then consider f being
sequence of
RelStr(#
(Bags o),
(InvLexOrder o) #)
such that A7:
f is
descending
by WELLFND1:14;
reconsider a =
f . 0 as
bag of
o ;
set s =
SgmX (
(RelIncl o),
(support a));
A8:
field (RelIncl o) = o
by WELLORD2:def 1;
RelIncl o is
being_linear-order
by ORDERS_1:19;
then A9:
RelIncl o linearly_orders support a
by A8, ORDERS_1:37, ORDERS_1:38;
then A10:
rng (SgmX ((RelIncl o),(support a))) = support a
by PRE_POLY:def 2;
then A13:
len (SgmX ((RelIncl o),(support a))) in dom (SgmX ((RelIncl o),(support a)))
by FINSEQ_5:6, RELAT_1:38;
then A14:
(SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) in rng (SgmX ((RelIncl o),(support a)))
by FUNCT_1:3;
then reconsider j =
(SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) as
Ordinal by A10;
defpred S2[
set ,
set ]
means ex
b being
bag of
o st
(
f . $1
= b & $2
= b . j );
consider t being
sequence of
NAT such that A16:
for
i being
Element of
NAT holds
S2[
i,
t . i]
from FUNCT_2:sch 3(A15);
defpred S3[
Nat]
means for
i being
Ordinal for
b being
bag of
o st
j in i &
i in o &
f . $1
= b holds
b . i = 0 ;
A17:
S3[
0 ]
proof
let i be
Ordinal;
for b being bag of o st j in i & i in o & f . 0 = b holds
b . i = 0 let b be
bag of
o;
( j in i & i in o & f . 0 = b implies b . i = 0 )
assume that A18:
j in i
and A19:
i in o
and A20:
f . 0 = b
;
b . i = 0
assume
b . i <> 0
;
contradiction
then
i in support a
by A20, PRE_POLY:def 7;
then consider k being
Nat such that A21:
k in dom (SgmX ((RelIncl o),(support a)))
and A22:
(SgmX ((RelIncl o),(support a))) . k = i
by A10, FINSEQ_2:10;
A23:
k <= len (SgmX ((RelIncl o),(support a)))
by A21, FINSEQ_3:25;
per cases
( k = len (SgmX ((RelIncl o),(support a))) or k < len (SgmX ((RelIncl o),(support a))) )
by A23, XXREAL_0:1;
suppose
k < len (SgmX ((RelIncl o),(support a)))
;
contradictionthen
[((SgmX ((RelIncl o),(support a))) /. k),((SgmX ((RelIncl o),(support a))) /. (len (SgmX ((RelIncl o),(support a)))))] in RelIncl o
by A9, A13, A21, PRE_POLY:def 2;
then
[((SgmX ((RelIncl o),(support a))) . k),((SgmX ((RelIncl o),(support a))) /. (len (SgmX ((RelIncl o),(support a)))))] in RelIncl o
by A21, PARTFUN1:def 6;
then
[((SgmX ((RelIncl o),(support a))) . k),((SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))))] in RelIncl o
by A13, PARTFUN1:def 6;
then
(SgmX ((RelIncl o),(support a))) . k c= (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a))))
by A10, A14, A19, A22, WELLORD2:def 1;
hence
contradiction
by A18, A22, ORDINAL1:5;
verum end; end;
end; A24:
for
n being
Nat st
S3[
n] holds
S3[
n + 1]
A35:
for
n being
Nat holds
S3[
n]
from NAT_1:sch 2(A17, A24);
reconsider t =
t as
sequence of
OrderedNAT by DICKSON:def 15;
A36:
t is
non-increasing
set n =
j;
set iln =
InvLexOrder j;
set S =
RelStr(#
(Bags j),
(InvLexOrder j) #);
InvLexOrder j is_strongly_connected_in Bags j
by Def5;
then
InvLexOrder j is_reflexive_in Bags j
;
then A43:
field (InvLexOrder j) = Bags j
by PARTIT_2:9;
consider p being
Nat such that A44:
for
r being
Nat st
p <= r holds
t . p = t . r
by A36, Th9;
defpred S4[
Nat,
set ]
means ex
b being
bag of
o st
(
b = f . (p + $1) & $2
= b | j );
consider g being
sequence of
(Bags j) such that A46:
for
x being
Element of
NAT holds
S4[
x,
g . x]
from FUNCT_2:sch 3(A45);
reconsider g =
g as
sequence of
RelStr(#
(Bags j),
(InvLexOrder j) #) ;
now for k being Nat holds
( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )let k be
Nat;
( g . (k + 1) <> g . k & [(g . (k + 1)),(g . k)] in InvLexOrder j )reconsider k0 =
k as
Element of
NAT by ORDINAL1:def 12;
consider b being
bag of
o such that A47:
b = f . (p + k)
and A48:
g . k0 = b | j
by A46;
consider b1 being
bag of
o such that A49:
b1 = f . (p + (k + 1))
and A50:
g . (k + 1) = b1 | j
by A46;
p + (k + 1) = (p + k) + 1
;
then A51:
b <> b1
by A7, A47, A49;
A52:
ex
bb being
bag of
o st
(
f . (p + k) = bb &
t . (p + k0) = bb . j )
by A16;
A53:
ex
bb1 being
bag of
o st
(
f . (p + (k + 1)) = bb1 &
t . (p + (k + 1)) = bb1 . j )
by A16;
A54:
t . (p + k) = t . p
by A44, NAT_1:11;
thus
g . (k + 1) <> g . k
[(g . (k + 1)),(g . k)] in InvLexOrder j
[(f . ((p + k) + 1)),(f . (p + k))] in InvLexOrder o
by A7;
then consider i being
Ordinal such that A61:
i in o
and A62:
b1 . i < b . i
and A63:
for
k being
Ordinal st
i in k &
k in o holds
b . k = b1 . k
by A47, A49, A51, Def6;
A64:
now i in jassume A65:
not
i in j
;
contradiction end; reconsider bj =
b | j,
b1j =
b1 | j as
bag of
j by A10, A14, Th17;
A67:
b1j . i = b1 . i
by A64, FUNCT_1:49;
A68:
bj . i = b . i
by A64, FUNCT_1:49;
hence
[(g . (k + 1)),(g . k)] in InvLexOrder j
by A48, A50, A62, A64, A67, A68, Def6;
verum end; then
g is
descending
;
then
not
RelStr(#
(Bags j),
(InvLexOrder j) #) is
well_founded
by WELLFND1:14;
then
not
InvLexOrder j is_well_founded_in the
carrier of
RelStr(#
(Bags j),
(InvLexOrder j) #)
;
then
not
InvLexOrder j well_orders field (InvLexOrder j)
by A43, WELLORD1:def 5;
then
not
InvLexOrder j is
well-ordering
by WELLORD1:4;
hence
contradiction
by A2, A10, A14;
verum end; A72:
field (InvLexOrder o) = Bags o
by ORDERS_1:12;
then A73:
InvLexOrder o is_reflexive_in Bags o
by RELAT_2:def 9;
A74:
InvLexOrder o is_transitive_in Bags o
by A72, RELAT_2:def 16;
A75:
InvLexOrder o is_antisymmetric_in Bags o
by A72, RELAT_2:def 12;
A76:
InvLexOrder o is_connected_in field (InvLexOrder o)
by A3, A4;
InvLexOrder o is_well_founded_in field (InvLexOrder o)
by A5, WELLORD1:3;
then
InvLexOrder o well_orders field (InvLexOrder o)
by A4, A73, A74, A75, A76, WELLORD1:def 5;
hence
S1[
o]
by WELLORD1:4;
verum end;
thus
for o being Ordinal holds S1[o]
from ORDINAL1:sch 2(A1); verum