let R be non empty RelStr ; ( R is quasi_ordered & ( for f being sequence of R ex i, j being 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 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;
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
( min-classes N is infinite or min-classes N is empty )
by A4;
suppose A5:
min-classes N is
infinite
;
contradictionthen reconsider MCN =
min-classes N as
infinite set ;
consider f being
sequence of
(min-classes N) such that A6:
f is
one-to-one
by A5, Th2;
deffunc H1(
object )
-> Element of
f . $1 = the
Element of
f . $1;
consider g being
sequence of the
carrier of
R such that A9:
for
x being
object 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
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;
A13:
f . i in MCN
;
then A14:
not
f . i is
empty
by Th21;
A15:
f . j in MCN
;
then A16:
not
f . j is
empty
by Th21;
j in NAT
by ORDINAL1:def 12;
then A17:
g . j = the
Element of
f . j
by A9;
i in NAT
by ORDINAL1:def 12;
then A18:
g . i = the
Element of
f . i
by A9;
A19:
gj is_minimal_wrt N, the
InternalRel of
(R \~)
by A1, A15, A16, A17, Th18;
gi is_minimal_wrt N, the
InternalRel of
(R \~)
by A1, A13, A14, A18, Th18;
then A20:
gi in N
by WAYBEL_4:def 25;
[gi,gj] in the
InternalRel of
R
by A11;
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;
A27:
i in NAT
by ORDINAL1:def 12;
A28:
j in NAT
by ORDINAL1:def 12;
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, A27, A28;
verum end; suppose A29:
min-classes N is
empty
;
contradictiondeffunc H1(
set ,
set )
-> Element of
(( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2)) = the
Element of
(( the InternalRel of R -Seg $2) /\ N) \ (Class ((EqRel R),$2));
consider f being
Function such that A30:
dom f = NAT
and A31:
f . 0 = the
Element of
N
and A32:
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;
A33:
S1[
0 ]
by A31;
A34:
now for i being Nat st S1[i] holds
S1[i + 1]end; A37:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A33, A34);
then reconsider f =
f as
sequence of
R by A30, FUNCT_2:3;
A38:
now for i, j being Nat holds S2[j]let i be
Nat;
for j being Nat holds S2[j]defpred S2[
Nat]
means (
i < $1 implies
f . i >= f . $1 );
A39:
S2[
0 ]
by NAT_1:2;
A40:
for
j being
Nat st
S2[
j] holds
S2[
j + 1]
thus
for
j being
Nat holds
S2[
j]
from NAT_1:sch 2(A39, A40); verum end; now for i, j being Nat holds S2[j]let i be
Nat;
for j being Nat holds S2[j]defpred S2[
Nat]
means (
i < $1 implies not
f . i <= f . $1 );
A48:
S2[
0 ]
by NAT_1:2;
A49:
for
j being
Nat st
S2[
j] holds
S2[
j + 1]
proof
let j be
Nat;
( S2[j] implies S2[j + 1] )
assume that
(
i < j implies not
f . i <= f . j )
and A50:
i < j + 1
;
not f . i <= f . (j + 1)
A51:
i <= j
by A50, NAT_1:13;
reconsider fj =
f . j,
fj1 =
f . (j + 1) as
Element of
(R \~) ;
A52:
fj in N
by A37;
per cases
( i < j or i = j )
by A51, XXREAL_0:1;
suppose A53:
i < j
;
not f . i <= f . (j + 1)assume A54:
f . i <= f . (j + 1)
;
contradiction
j < j + 1
by NAT_1:13;
then A55:
f . j >= f . (j + 1)
by A38;
f . i >= f . j
by A38, A53;
then
f . j <= f . (j + 1)
by A3, A54, ORDERS_2:3;
then A56:
fj1 in Class (
(EqRel R),
fj)
by A1, A55, Th7;
set IC =
(( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj));
A57:
fj1 = the
Element of
(( the InternalRel of R -Seg fj) /\ N) \ (Class ((EqRel R),fj))
by A32;
hence
contradiction
by A56, A57, XBOOLE_0:def 5;
verum end;
end; thus
for
j being
Nat holds
S2[
j]
from NAT_1:sch 2(A48, A49); verum end; hence
contradiction
by A2;
verum end;