let X be non empty set ; ex Y being Subset-Family of X st
( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
consider R being Relation such that
A1:
R well_orders X
by WELLORD2:17;
set RX = R |_2 X;
deffunc H1( object ) -> Element of bool X = X \ ((R |_2 X) -Seg $1);
A2:
for x being object st x in X holds
H1(x) in bool X
;
consider f being Function of X,(bool X) such that
A3:
for x being object st x in X holds
f . x = H1(x)
from FUNCT_2:sch 2(A2);
take Y = rng f; ( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
A4:
dom f = X
by FUNCT_2:def 1;
thus
Y is with_non-empty_elements
( Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
thus
Y is c=-linear
( X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )proof
let x be
set ;
ORDINAL1:def 8 for b1 being set holds
( not x in Y or not b1 in Y or x,b1 are_c=-comparable )let y be
set ;
( not x in Y or not y in Y or x,y are_c=-comparable )
assume that A7:
x in Y
and A8:
y in Y
;
x,y are_c=-comparable
consider a being
object such that A9:
(
a in dom f &
f . a = x )
by A7, FUNCT_1:def 3;
consider b being
object such that A10:
(
b in dom f &
f . b = y )
by A8, FUNCT_1:def 3;
(R |_2 X) -Seg a,
(R |_2 X) -Seg b are_c=-comparable
by A1, WELLORD1:26, WELLORD2:16;
then
(
(R |_2 X) -Seg a c= (R |_2 X) -Seg b or
(R |_2 X) -Seg b c= (R |_2 X) -Seg a )
;
then
(
H1(
b)
c= H1(
a) or
H1(
a)
c= H1(
b) )
by XBOOLE_1:34;
then A11:
H1(
a),
H1(
b)
are_c=-comparable
;
x = H1(
a)
by A3, A9;
hence
x,
y are_c=-comparable
by A3, A10, A11;
verum
end;
A12:
field (R |_2 X) = X
by A1, WELLORD2:16;
then consider x being object such that
A13:
x in X
and
A14:
for y being object st y in X holds
[x,y] in R |_2 X
by A1, WELLORD1:7, WELLORD2:16;
A15:
R |_2 X is well-ordering
by A1, WELLORD2:16;
then A16:
R |_2 X is well_founded
by WELLORD1:def 4;
R |_2 X is antisymmetric
by A15, WELLORD1:def 4;
then A17:
R |_2 X is_antisymmetric_in X
by A12, RELAT_2:def 12;
A18:
(R |_2 X) -Seg x = {}
proof
assume
(R |_2 X) -Seg x <> {}
;
contradiction
then consider y being
object such that A19:
y in (R |_2 X) -Seg x
by XBOOLE_0:def 1;
A20:
y <> x
by A19, WELLORD1:1;
A21:
[y,x] in R |_2 X
by A19, WELLORD1:1;
then A22:
x in X
by A12, RELAT_1:15;
A23:
y in X
by A12, A21, RELAT_1:15;
then
[x,y] in R |_2 X
by A14;
hence
contradiction
by A17, A20, A21, A22, A23, RELAT_2:def 4;
verum
end;
f . x = H1(x)
by A3, A13;
hence
X in Y
by A4, A13, A18, FUNCT_1:def 3; ( card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
now for x1, x2 being object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in X & x2 in X & f . x1 = f . x2 implies x1 = x2 )reconsider R1 =
(R |_2 X) -Seg x1,
R2 =
(R |_2 X) -Seg x2 as
Subset of
X by A12, WELLORD1:9;
assume that A24:
(
x1 in X &
x2 in X )
and A25:
f . x1 = f . x2
;
x1 = x2
(
R1 ` = f . x1 &
f . x2 = R2 ` )
by A3, A24;
then
R1 = R2
by A25, SUBSET_1:42;
then
(
[x1,x2] in R |_2 X &
[x2,x1] in R |_2 X )
by A12, A15, A24, WELLORD1:29;
hence
x1 = x2
by A17, A24, RELAT_2:def 4;
verum end;
then
f is one-to-one
by FUNCT_2:19;
then
X,Y are_equipotent
by A4, WELLORD2:def 4;
hence
card X = card Y
by CARD_1:5; for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y )
let Z be set ; ( Z in Y & card Z <> 1 implies ex x being set st
( x in Z & Z \ {x} in Y ) )
assume that
A26:
Z in Y
and
A27:
card Z <> 1
; ex x being set st
( x in Z & Z \ {x} in Y )
consider x being object such that
A28:
x in dom f
and
A29:
f . x = Z
by A26, FUNCT_1:def 3;
A30:
{x} c= X
by A28, ZFMISC_1:31;
reconsider x = x as set by TARSKI:1;
take
x
; ( x in Z & Z \ {x} in Y )
A31:
not x in (R |_2 X) -Seg x
by WELLORD1:1;
A32:
Z = X \ ((R |_2 X) -Seg x)
by A3, A28, A29;
hence
x in Z
by A28, A31, XBOOLE_0:def 5; Z \ {x} in Y
(R |_2 X) -Seg x c= X
by A12, WELLORD1:9;
then reconsider Rxx = ((R |_2 X) -Seg x) \/ {x} as Subset of X by A30, XBOOLE_1:8;
X \ Rxx <> {}
then consider a being object such that
A33:
a in Rxx `
and
A34:
(R |_2 X) -Seg a misses Rxx `
by A12, A16, WELLORD1:def 2;
A35:
not a in Rxx
by A33, XBOOLE_0:def 5;
x in {x}
by TARSKI:def 1;
then A36:
x <> a
by A35, XBOOLE_0:def 3;
R |_2 X is connected
by A15, WELLORD1:def 4;
then
R |_2 X is_connected_in X
by A12, RELAT_2:def 14;
then A37:
( [x,a] in R |_2 X or [a,x] in R |_2 X )
by A28, A33, A36, RELAT_2:def 6;
A38:
not a in (R |_2 X) -Seg x
by A35, XBOOLE_0:def 3;
then
x in (R |_2 X) -Seg a
by A36, A37, WELLORD1:1;
then A39:
{x} c= (R |_2 X) -Seg a
by ZFMISC_1:31;
(R |_2 X) -Seg a c= X
by A12, WELLORD1:9;
then A40:
(R |_2 X) -Seg a c= Rxx
by A34, SUBSET_1:24;
(R |_2 X) -Seg x c= (R |_2 X) -Seg a
by A12, A15, A28, A33, A37, A38, WELLORD1:1, WELLORD1:29;
then
Rxx c= (R |_2 X) -Seg a
by A39, XBOOLE_1:8;
then
Rxx = (R |_2 X) -Seg a
by A40;
then f . a =
X \ Rxx
by A3, A33
.=
(X \ ((R |_2 X) -Seg x)) \ {x}
by XBOOLE_1:41
.=
Z \ {x}
by A3, A28, A29
;
hence
Z \ {x} in Y
by A4, A33, FUNCT_1:def 3; verum