let R be non empty RelStr ; ( R is quasi_ordered & ( for f being sequence of R ex i, j being Element of NAT st
( i < j & f . i <= f . j ) ) implies for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty ) )
assume that
A1:
R is quasi_ordered
and
A2:
for f being sequence of R ex i, j being Element of NAT st
( i < j & f . i <= f . j )
; for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty )
set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~);
A3:
R is transitive
by A1, Def3;
let N be non empty Subset of R; ( min-classes N is finite & not min-classes N is empty )
assume A4:
( not min-classes N is finite or min-classes N is empty )
; contradiction
per cases
( not min-classes N is finite or min-classes N is empty )
by A4;
suppose A5:
not
min-classes N is
finite
;
contradictionthen reconsider MCN =
min-classes N as
infinite set ;
consider f being
Function of
NAT,
(min-classes N) such that A6:
f is
one-to-one
by A5, Th3;
deffunc H1(
set )
-> Element of
f . $1 =
choose (f . $1);
consider g being
Function of
NAT, the
carrier of
R such that A9:
for
x being
set st
x in NAT holds
g . x = H1(
x)
from FUNCT_2:sch 2(A7);
reconsider g =
g as
sequence of
R ;
consider i,
j being
Element of
NAT such that A10:
i < j
and A11:
g . i <= g . j
by A2;
reconsider gi =
g . i,
gj =
g . j as
Element of
(R \~) ;
A12:
[gi,gj] in the
InternalRel of
R
by A11, ORDERS_2:def 5;
A13:
f . i in MCN
;
then A14:
not
f . i is
empty
by Th23;
A15:
f . j in MCN
;
then A16:
not
f . j is
empty
by Th23;
A17:
g . j = choose (f . j)
by A9;
A18:
g . i = choose (f . i)
by A9;
A19:
gj is_minimal_wrt N, the
InternalRel of
(R \~)
by A1, A15, A16, A17, Th20;
gi is_minimal_wrt N, the
InternalRel of
(R \~)
by A1, A13, A14, A18, Th20;
then A20:
gi in N
by WAYBEL_4:def 25;
[gi,gj] in the
InternalRel of
R
by A11, ORDERS_2:def 5;
then
[gi,gj] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A21, XBOOLE_0:def 4;
then
[gi,gj] in EqRel R
by A1, Def4;
then
gi in Class (
(EqRel R),
gj)
by EQREL_1:19;
then A23:
Class (
(EqRel R),
gj)
= Class (
(EqRel R),
gi)
by EQREL_1:23;
consider mj being
Element of
(R \~) such that
mj is_minimal_wrt N, the
InternalRel of
(R \~)
and A24:
f . j = (Class ((EqRel R),mj)) /\ N
by A15, Def8;
consider mi being
Element of
(R \~) such that
mi is_minimal_wrt N, the
InternalRel of
(R \~)
and A25:
f . i = (Class ((EqRel R),mi)) /\ N
by A13, Def8;
gj in Class (
(EqRel R),
mj)
by A16, A17, A24, XBOOLE_0:def 4;
then A26:
Class (
(EqRel R),
gj)
= Class (
(EqRel R),
mj)
by EQREL_1:23;
gi in Class (
(EqRel R),
mi)
by A14, A18, A25, XBOOLE_0:def 4;
then
f . i = f . j
by A23, A24, A25, A26, EQREL_1:23;
hence
contradiction
by A5, A6, A10, FUNCT_2:19;
verum end; suppose A27:
min-classes N is
empty
;
contradictiondeffunc H1(
set ,
set )
-> Element of
(( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2)) =
choose ((( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2)));
consider f being
Function such that A28:
dom f = NAT
and A29:
f . 0 = choose N
and A30:
for
n being
Nat holds
f . (n + 1) = H1(
n,
f . n)
from NAT_1:sch 11();
defpred S1[
Nat]
means f . $1
in N;
A31:
S1[
0 ]
by A29;
A35:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A31, A32);
then reconsider f =
f as
sequence of
R by A28, FUNCT_2:3;
now let i be
Element of
NAT ;
for j being Element of NAT holds S2[j]defpred S2[
Element of
NAT ]
means (
i < $1 implies not
f . i <= f . $1 );
A46:
S2[
0 ]
by NAT_1:2;
A47:
for
j being
Element of
NAT st
S2[
j] holds
S2[
j + 1]
proof
let j be
Element of
NAT ;
( S2[j] implies S2[j + 1] )
assume that
(
i < j implies not
f . i <= f . j )
and A48:
i < j + 1
;
not f . i <= f . (j + 1)
A49:
i <= j
by A48, NAT_1:13;
reconsider fj =
f . j,
fj1 =
f . (j + 1) as
Element of
(R \~) ;
A50:
fj in N
by A35;
per cases
( i < j or i = j )
by A49, XXREAL_0:1;
suppose A51:
i < j
;
not f . i <= f . (j + 1)assume A52:
f . i <= f . (j + 1)
;
contradiction
j < j + 1
by NAT_1:13;
then A53:
f . j >= f . (j + 1)
by A36;
f . i >= f . j
by A36, A51;
then
f . j <= f . (j + 1)
by A3, A52, ORDERS_2:3;
then A54:
fj1 in Class (
(EqRel R),
fj)
by A1, A53, Th9;
set IC =
(( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj));
A55:
fj1 = choose ((( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj)))
by A30;
hence
contradiction
by A54, A55, XBOOLE_0:def 5;
verum end;
end; thus
for
j being
Element of
NAT holds
S2[
j]
from NAT_1:sch 1(A46, A47); verum end; hence
contradiction
by A2;
verum end;