let R be non empty RelStr ; :: thesis: ( 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 )
; :: thesis: 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 IR' = the InternalRel of (R \~ );
A3:
R is transitive
by A1, Def3;
let N be non empty Subset of R; :: thesis: ( 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 )
; :: thesis: 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
;
:: thesis: 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 A10:
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 A11:
i < j
and A12:
g . i <= g . j
by A2;
reconsider gi =
g . i,
gj =
g . j as
Element of
(R \~ ) ;
A13:
[gi,gj] in the
InternalRel of
R
by A12, ORDERS_2:def 9;
A14:
f . i in MCN
;
then A15:
not
f . i is
empty
by A1, Th23;
A16:
f . j in MCN
;
then A17:
not
f . j is
empty
by A1, Th23;
A18:
g . j = choose (f . j)
by A10;
A19:
g . i = choose (f . i)
by A10;
A20:
gj is_minimal_wrt N,the
InternalRel of
(R \~ )
by A1, A16, A17, A18, Th20;
gi is_minimal_wrt N,the
InternalRel of
(R \~ )
by A1, A14, A15, A19, Th20;
then A21:
gi in N
by WAYBEL_4:def 26;
[gi,gj] in the
InternalRel of
R
by A12, ORDERS_2:def 9;
then
[gi,gj] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by A22, XBOOLE_0:def 4;
then
[gi,gj] in EqRel R
by A1, Def4;
then
gi in Class (EqRel R),
gj
by EQREL_1:27;
then A24:
Class (EqRel R),
gj = Class (EqRel R),
gi
by EQREL_1:31;
consider mj being
Element of
(R \~ ) such that
mj is_minimal_wrt N,the
InternalRel of
(R \~ )
and A25:
f . j = (Class (EqRel R),mj) /\ N
by A16, Def8;
consider mi being
Element of
(R \~ ) such that
mi is_minimal_wrt N,the
InternalRel of
(R \~ )
and A26:
f . i = (Class (EqRel R),mi) /\ N
by A14, Def8;
gj in Class (EqRel R),
mj
by A17, A18, A25, XBOOLE_0:def 4;
then A27:
Class (EqRel R),
gj = Class (EqRel R),
mj
by EQREL_1:31;
gi in Class (EqRel R),
mi
by A15, A19, A26, XBOOLE_0:def 4;
then
f . i = f . j
by A24, A25, A26, A27, EQREL_1:31;
hence
contradiction
by A5, A6, A11, FUNCT_2:25;
:: thesis: verum end; suppose A28:
min-classes N is
empty
;
:: thesis: 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 A29:
dom f = NAT
and A30:
f . 0 = choose N
and A31:
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;
A32:
S1[
0 ]
by A30;
A36:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A32, A33);
then reconsider f =
f as
sequence of
R by A29, FUNCT_2:5;
A48:
now let i be
Element of
NAT ;
:: thesis: for j being Element of NAT holds S2[j]defpred S2[
Element of
NAT ]
means (
i < $1 implies not
f . i <= f . $1 );
A49:
S2[
0 ]
by NAT_1:2;
A50:
for
j being
Element of
NAT st
S2[
j] holds
S2[
j + 1]
proof
let j be
Element of
NAT ;
:: thesis: ( S2[j] implies S2[j + 1] )
assume that
(
i < j implies not
f . i <= f . j )
and A51:
i < j + 1
;
:: thesis: not f . i <= f . (j + 1)
A52:
i <= j
by A51, NAT_1:13;
reconsider fj =
f . j,
fj1 =
f . (j + 1) as
Element of
(R \~ ) ;
A53:
fj in N
by A36;
per cases
( i < j or i = j )
by A52, XXREAL_0:1;
suppose A54:
i < j
;
:: thesis: not f . i <= f . (j + 1)assume A55:
f . i <= f . (j + 1)
;
:: thesis: contradiction
j < j + 1
by NAT_1:13;
then A56:
f . j >= f . (j + 1)
by A38;
f . i >= f . j
by A38, A54;
then
f . j <= f . (j + 1)
by A3, A55, ORDERS_2:26;
then A57:
fj1 in Class (EqRel R),
fj
by A1, A56, Th9;
set IC =
((the InternalRel of R -Seg fj) /\ N) \ (Class (EqRel R),fj);
A58:
fj1 = choose (((the InternalRel of R -Seg fj) /\ N) \ (Class (EqRel R),fj))
by A31;
hence
contradiction
by A57, A58, XBOOLE_0:def 5;
:: thesis: verum end;
end; thus
for
j being
Element of
NAT holds
S2[
j]
from NAT_1:sch 1(A49, A50); :: thesis: verum end; consider i,
j being
Element of
NAT such that A63:
(
i < j &
f . i <= f . j )
by A2;
thus
contradiction
by A48, A63;
:: thesis: verum end;