let X be set ; for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
let Y be Subset-Family of X; ( Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y implies ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) ) )
assume that
A1:
( Y is finite & Y is with_non-empty_elements & Y is c=-linear )
and
A2:
X in Y
; ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
defpred S1[ object , object ] means ex A being set st
( A = $2 & $1 in A & $2 in Y & ( for y being set st y in Y & $1 in y holds
A c= y ) );
A3:
for x being object st x in X holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in X implies ex y being object st S1[x,y] )
set U =
{ A where A is Subset of X : ( x in A & A in Y ) } ;
A4:
{ A where A is Subset of X : ( x in A & A in Y ) } c= Y
then reconsider U =
{ A where A is Subset of X : ( x in A & A in Y ) } as
Subset-Family of
X by XBOOLE_1:1;
assume
x in X
;
ex y being object st S1[x,y]
then
X in U
by A2;
then consider m being
set such that A5:
m in U
and A6:
for
y being
set st
y in U holds
m c= y
by A1, A4, FINSET_1:11;
take
m
;
S1[x,m]
consider A being
Subset of
X such that A7:
(
m = A &
x in A &
A in Y )
by A5;
take
A
;
( A = m & x in A & m in Y & ( for y being set st y in Y & x in y holds
A c= y ) )
thus
A = m
by A7;
( x in A & m in Y & ( for y being set st y in Y & x in y holds
A c= y ) )
thus
(
x in A &
m in Y )
by A7;
for y being set st y in Y & x in y holds
A c= y
let y be
set ;
( y in Y & x in y implies A c= y )
assume
(
y in Y &
x in y )
;
A c= y
then
y in U
;
hence
A c= y
by A6, A7;
verum
end;
consider f being Function such that
A8:
( dom f = X & ( for x being object st x in X holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A3);
defpred S2[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & ( D2 in Y or D2 is empty ) & D2 c< D1 & ( for x being set st x in Y & x c< D1 holds
x c= D2 ) & ( for x being set st x in Y & D2 c= x & x c= D1 & not x = D1 holds
x = D2 ) );
A9:
for x being object st x in Y holds
ex y being object st
( y in bool X & S2[x,y] )
proof
let x be
object ;
( x in Y implies ex y being object st
( y in bool X & S2[x,y] ) )
reconsider xx =
x as
set by TARSKI:1;
assume A10:
x in Y
;
ex y being object st
( y in bool X & S2[x,y] )
set U =
{ A where A is Subset of X : ( A c< xx & A in Y ) } ;
A11:
{ A where A is Subset of X : ( A c< xx & A in Y ) } c= Y
then reconsider U =
{ A where A is Subset of X : ( A c< xx & A in Y ) } as
Subset-Family of
X by XBOOLE_1:1;
take u =
union U;
( u in bool X & S2[x,u] )
thus
u in bool X
;
S2[x,u]
A12:
for
y being
set st
y in Y &
y c< xx holds
y c= u
per cases
( U is empty or not U is empty )
;
suppose A15:
U is
empty
;
S2[x,u]take
xx
;
ex D2 being set st
( xx = x & D2 = u & ( D2 in Y or D2 is empty ) & D2 c< xx & ( for x being set st x in Y & x c< xx holds
x c= D2 ) & ( for x being set st x in Y & D2 c= x & x c= xx & not x = xx holds
x = D2 ) )take
u
;
( xx = x & u = u & ( u in Y or u is empty ) & u c< xx & ( for x being set st x in Y & x c< xx holds
x c= u ) & ( for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = u ) )thus
(
xx = x &
u = u )
;
( ( u in Y or u is empty ) & u c< xx & ( for x being set st x in Y & x c< xx holds
x c= u ) & ( for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = u ) )thus
( (
u in Y or
u is
empty ) &
u c< xx & ( for
y being
set st
y in Y &
y c< xx holds
y c= u ) )
by A1, A10, A12, A15, XBOOLE_1:61, ZFMISC_1:2;
for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = ulet y be
set ;
( y in Y & u c= y & y c= xx & not y = xx implies y = u )assume that A16:
y in Y
and A17:
u c= y
and A18:
y c= xx
;
( y = xx or y = u )assume
y <> xx
;
y = uthen
y c< xx
by A18;
then
y c= u
by A12, A16;
hence
y = u
by A17;
verum end; suppose
not
U is
empty
;
S2[x,u]then
u in U
by A1, A11, Th9;
then A19:
ex
A being
Subset of
X st
(
A = u &
A c< xx &
A in Y )
;
take
xx
;
ex D2 being set st
( xx = x & D2 = u & ( D2 in Y or D2 is empty ) & D2 c< xx & ( for x being set st x in Y & x c< xx holds
x c= D2 ) & ( for x being set st x in Y & D2 c= x & x c= xx & not x = xx holds
x = D2 ) )take
u
;
( xx = x & u = u & ( u in Y or u is empty ) & u c< xx & ( for x being set st x in Y & x c< xx holds
x c= u ) & ( for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = u ) )thus
(
xx = x &
u = u )
;
( ( u in Y or u is empty ) & u c< xx & ( for x being set st x in Y & x c< xx holds
x c= u ) & ( for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = u ) )thus
( (
u in Y or
u is
empty ) &
u c< xx & ( for
y being
set st
y in Y &
y c< xx holds
y c= u ) )
by A12, A19;
for x being set st x in Y & u c= x & x c= xx & not x = xx holds
x = ulet y be
set ;
( y in Y & u c= y & y c= xx & not y = xx implies y = u )assume that A20:
y in Y
and A21:
u c= y
and A22:
y c= xx
;
( y = xx or y = u )assume
y <> xx
;
y = uthen
y c< xx
by A22;
then
y c= u
by A12, A20;
hence
y = u
by A21;
verum end; end;
end;
consider g being Function of Y,(bool X) such that
A23:
for x being object st x in Y holds
S2[x,g . x]
from FUNCT_2:sch 1(A9);
defpred S3[ object , object ] means ex A being set ex h being Function of (A \ (g . A)),(bool (A \ (g . A))) st
( A = $1 & $2 = h & h is one-to-one & rng h is with_non-empty_elements & rng h is c=-linear & dom h in rng h & ( for Z being set st Z in rng h & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng h ) ) );
A24:
for x being object st x in Y holds
ex y being object st S3[x,y]
proof
let y be
object ;
( y in Y implies ex y being object st S3[y,y] )
assume A25:
y in Y
;
ex y being object st S3[y,y]
reconsider y =
y as
set by TARSKI:1;
S2[
y,
g . y]
by A23, A25;
then
g . y c< y
;
then
y \ (g . y) <> {}
by XBOOLE_1:105;
then consider Z being
Subset-Family of
(y \ (g . y)) such that A26:
(
Z is
with_non-empty_elements &
Z is
c=-linear &
y \ (g . y) in Z )
and A27:
card (y \ (g . y)) = card Z
and A28:
for
z being
set st
z in Z &
card z <> 1 holds
ex
x being
set st
(
x in z &
z \ {x} in Z )
by Th12;
y \ (g . y),
Z are_equipotent
by A27, CARD_1:5;
then consider h being
Function such that A29:
h is
one-to-one
and A30:
(
dom h = y \ (g . y) &
rng h = Z )
by WELLORD2:def 4;
reconsider h =
h as
Function of
(y \ (g . y)),
(bool (y \ (g . y))) by A30, FUNCT_2:2;
take
h
;
S3[y,h]
thus
S3[
y,
h]
by A26, A28, A29, A30;
verum
end;
consider h being Function such that
A31:
( dom h = Y & ( for x being object st x in Y holds
S3[x,h . x] ) )
from CLASSES1:sch 1(A24);
then reconsider h = h as Function-yielding Function by FUNCOP_1:def 6;
deffunc H1( object ) -> set = (g . (f . $1)) \/ ((h . (f . $1)) . $1);
A32:
for x being set st x in X holds
x in (f . x) \ (g . (f . x))
A39:
for x being object st x in X holds
H1(x) in bool X
proof
let x be
object ;
( x in X implies H1(x) in bool X )
set fx =
f . x;
assume A40:
x in X
;
H1(x) in bool X
then
S1[
x,
f . x]
by A8;
then A41:
f . x in Y
;
then
S3[
f . x,
h . (f . x)]
by A31;
then consider A being
set ,
H being
Function of
((f . x) \ (g . (f . x))),
(bool ((f . x) \ (g . (f . x)))) such that A42:
h . (f . x) = H
and
H is
one-to-one
and
(
rng H is
with_non-empty_elements &
rng H is
c=-linear )
and
dom H in rng H
and
for
Z being
set st
Z in rng H &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H )
;
A43:
x in (f . x) \ (g . (f . x))
by A32, A40;
dom H = (f . x) \ (g . (f . x))
by FUNCT_2:def 1;
then
H . x in rng H
by A43, FUNCT_1:def 3;
then
H . x c= f . x
by XBOOLE_1:1;
then A44:
H . x c= X
by A41, XBOOLE_1:1;
S2[
f . x,
g . (f . x)]
by A23, A41;
then
(
g . (f . x) in Y or
g . (f . x) is
empty )
;
then
H1(
x)
c= X
by A42, A44, XBOOLE_1:8;
hence
H1(
x)
in bool X
;
verum
end;
consider z being Function of X,(bool X) such that
A45:
for x being object st x in X holds
z . x = H1(x)
from FUNCT_2:sch 2(A39);
A46:
dom z = X
by FUNCT_2:def 1;
A47:
Y c= rng z
proof
let y be
object ;
TARSKI:def 3 ( not y in Y or y in rng z )
reconsider yy =
y as
set by TARSKI:1;
assume A48:
y in Y
;
y in rng z
then
S3[
y,
h . y]
by A31;
then consider H being
Function of
(yy \ (g . y)),
(bool (yy \ (g . y))) such that A49:
h . y = H
and
H is
one-to-one
and
(
rng H is
with_non-empty_elements &
rng H is
c=-linear )
and A50:
dom H in rng H
and
for
Z being
set st
Z in rng H &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H )
;
consider x being
object such that A51:
x in dom H
and A52:
H . x = dom H
by A50, FUNCT_1:def 3;
A53:
dom H = yy \ (g . yy)
by FUNCT_2:def 1;
then A54:
x in yy
by A51;
then A55:
S1[
x,
f . x]
by A8, A48;
then A56:
x in f . x
;
S2[
y,
g . y]
by A23, A48;
then
g . y c< yy
;
then A57:
g . y c= yy
;
A58:
f . x c= yy
by A48, A54, A55;
A59:
f . x in Y
by A55;
f . x = y
then z . x =
(g . y) \/ (yy \ (g . y))
by A45, A48, A49, A52, A53, A54
.=
y
by A57, XBOOLE_1:45
;
hence
y in rng z
by A46, A48, A54, FUNCT_1:def 3;
verum
end;
A61:
for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z )
proof
let Z be
set ;
( Z in rng z & card Z <> 1 implies ex x being set st
( x in Z & Z \ {x} in rng z ) )
assume that A62:
Z in rng z
and A63:
card Z <> 1
;
ex x being set st
( x in Z & Z \ {x} in rng z )
consider x being
object such that A64:
x in dom z
and A65:
z . x = Z
by A62, FUNCT_1:def 3;
set fx =
f . x;
S1[
x,
f . x]
by A8, A64;
then A66:
f . x in Y
;
then
S3[
f . x,
h . (f . x)]
by A31;
then consider H being
Function of
((f . x) \ (g . (f . x))),
(bool ((f . x) \ (g . (f . x)))) such that A67:
h . (f . x) = H
and
H is
one-to-one
and
(
rng H is
with_non-empty_elements &
rng H is
c=-linear )
and
dom H in rng H
and A68:
for
Z being
set st
Z in rng H &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H )
;
A69:
z . x = (g . (f . x)) \/ (H . x)
by A45, A64, A67;
A70:
dom H = (f . x) \ (g . (f . x))
by FUNCT_2:def 1;
x in (f . x) \ (g . (f . x))
by A32, A64;
then A71:
H . x in rng H
by A70, FUNCT_1:def 3;
per cases
( card (H . x) = 1 or card (H . x) <> 1 )
;
suppose A72:
card (H . x) = 1
;
ex x being set st
( x in Z & Z \ {x} in rng z )then A73:
g . (f . x) <> {}
by A63, A65, A69;
S2[
f . x,
g . (f . x)]
by A23, A66;
then A74:
g . (f . x) in Y
by A73;
consider a being
object such that A75:
H . x = {a}
by A72, CARD_2:42;
reconsider a =
a as
set by TARSKI:1;
take
a
;
( a in Z & Z \ {a} in rng z )A76:
a in H . x
by A75, TARSKI:def 1;
then A77:
not
a in g . (f . x)
by A71, XBOOLE_0:def 5;
thus
a in Z
by A65, A69, A76, XBOOLE_0:def 3;
Z \ {a} in rng zZ \ {a} =
((g . (f . x)) \/ (H . x)) \ (H . x)
by A45, A64, A65, A67, A75
.=
(g . (f . x)) \ (H . x)
by XBOOLE_1:40
.=
g . (f . x)
by A75, A77, ZFMISC_1:57
;
hence
Z \ {a} in rng z
by A47, A74;
verum end; suppose
card (H . x) <> 1
;
ex x being set st
( x in Z & Z \ {x} in rng z )then consider a being
set such that A78:
a in H . x
and A79:
(H . x) \ {a} in rng H
by A68, A71;
A80:
not
a in g . (f . x)
by A71, A78, XBOOLE_0:def 5;
take
a
;
( a in Z & Z \ {a} in rng z )thus
a in Z
by A65, A69, A78, XBOOLE_0:def 3;
Z \ {a} in rng zconsider b being
object such that A81:
b in dom H
and A82:
H . b = (H . x) \ {a}
by A79, FUNCT_1:def 3;
A83:
b in f . x
by A70, A81;
then A84:
S1[
b,
f . b]
by A8, A66;
then A85:
b in f . b
;
A86:
f . b in Y
by A84;
A87:
f . b c= f . x
by A66, A83, A84;
f . x = f . b
then z . b =
(g . (f . x)) \/ ((H . x) \ {a})
by A45, A66, A67, A82, A83
.=
((g . (f . x)) \/ (H . x)) \ {a}
by A80, XBOOLE_1:87, ZFMISC_1:50
.=
Z \ {a}
by A65, A45, A64, A67
;
hence
Z \ {a} in rng z
by A46, A66, A83, FUNCT_1:def 3;
verum end; end;
end;
A89:
rng z is c=-linear
proof
let y1,
y2 be
set ;
ORDINAL1:def 8 ( not y1 in rng z or not y2 in rng z or y1,y2 are_c=-comparable )
assume that A90:
y1 in rng z
and A91:
y2 in rng z
;
y1,y2 are_c=-comparable
consider x1 being
object such that A92:
x1 in dom z
and A93:
z . x1 = y1
by A90, FUNCT_1:def 3;
consider x2 being
object such that A94:
x2 in dom z
and A95:
z . x2 = y2
by A91, FUNCT_1:def 3;
set fx1 =
f . x1;
set fx2 =
f . x2;
A96:
x1 in (f . x1) \ (g . (f . x1))
by A32, A92;
S1[
x1,
f . x1]
by A8, A92;
then A97:
f . x1 in Y
;
then
S3[
f . x1,
h . (f . x1)]
by A31;
then consider H1 being
Function of
((f . x1) \ (g . (f . x1))),
(bool ((f . x1) \ (g . (f . x1)))) such that A98:
h . (f . x1) = H1
and
H1 is
one-to-one
and
(
rng H1 is
with_non-empty_elements &
rng H1 is
c=-linear )
and
dom H1 in rng H1
and
for
Z being
set st
Z in rng H1 &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H1 )
;
A99:
z . x1 = (g . (f . x1)) \/ (H1 . x1)
by A45, A92, A98;
dom H1 = (f . x1) \ (g . (f . x1))
by FUNCT_2:def 1;
then A100:
H1 . x1 in rng H1
by A96, FUNCT_1:def 3;
A101:
x2 in (f . x2) \ (g . (f . x2))
by A32, A94;
S1[
x2,
f . x2]
by A8, A94;
then A102:
f . x2 in Y
;
then
S3[
f . x2,
h . (f . x2)]
by A31;
then consider H2 being
Function of
((f . x2) \ (g . (f . x2))),
(bool ((f . x2) \ (g . (f . x2)))) such that A103:
h . (f . x2) = H2
and
H2 is
one-to-one
and A104:
(
rng H2 is
with_non-empty_elements &
rng H2 is
c=-linear )
and
dom H2 in rng H2
and
for
Z being
set st
Z in rng H2 &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H2 )
;
A105:
z . x2 = (g . (f . x2)) \/ (H2 . x2)
by A45, A94, A103;
dom H2 = (f . x2) \ (g . (f . x2))
by FUNCT_2:def 1;
then A106:
H2 . x2 in rng H2
by A101, FUNCT_1:def 3;
A107:
f . x1,
f . x2 are_c=-comparable
by A1, A97, A102;
per cases
( f . x1 = f . x2 or ( f . x1 c= f . x2 & f . x1 <> f . x2 ) or ( f . x2 c= f . x1 & f . x1 <> f . x2 ) )
by A107;
suppose A108:
f . x1 = f . x2
;
y1,y2 are_c=-comparable then
H1 . x1,
H1 . x2 are_c=-comparable
by A98, A100, A103, A104, A106;
then
(
H1 . x1 c= H1 . x2 or
H1 . x2 c= H1 . x1 )
;
then
(
z . x1 c= z . x2 or
z . x2 c= z . x1 )
by A98, A99, A103, A105, A108, XBOOLE_1:9;
hence
y1,
y2 are_c=-comparable
by A93, A95;
verum end; suppose
(
f . x1 c= f . x2 &
f . x1 <> f . x2 )
;
y1,y2 are_c=-comparable then A109:
f . x1 c< f . x2
;
S2[
f . x2,
g . (f . x2)]
by A23, A102;
then A110:
f . x1 c= g . (f . x2)
by A97, A109;
g . (f . x2) c= z . x2
by A105, XBOOLE_1:7;
then A111:
f . x1 c= z . x2
by A110;
S2[
f . x1,
g . (f . x1)]
by A23, A97;
then
g . (f . x1) c< f . x1
;
then
g . (f . x1) c= f . x1
;
then A112:
(g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1
by XBOOLE_1:45;
z . x1 c= (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1)))
by A99, A100, XBOOLE_1:9;
then
z . x1 c= z . x2
by A111, A112;
hence
y1,
y2 are_c=-comparable
by A93, A95;
verum end; suppose
(
f . x2 c= f . x1 &
f . x1 <> f . x2 )
;
y1,y2 are_c=-comparable then A113:
f . x2 c< f . x1
;
S2[
f . x1,
g . (f . x1)]
by A23, A97;
then A114:
f . x2 c= g . (f . x1)
by A102, A113;
g . (f . x1) c= z . x1
by A99, XBOOLE_1:7;
then A115:
f . x2 c= z . x1
by A114;
S2[
f . x2,
g . (f . x2)]
by A23, A102;
then
g . (f . x2) c< f . x2
;
then
g . (f . x2) c= f . x2
;
then A116:
(g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2
by XBOOLE_1:45;
z . x2 c= (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2)))
by A105, A106, XBOOLE_1:9;
then
z . x2 c= z . x1
by A115, A116;
hence
y1,
y2 are_c=-comparable
by A93, A95;
verum end; end;
end;
A117:
rng z is with_non-empty_elements
proof
assume
not
rng z is
with_non-empty_elements
;
contradiction
then
{} in rng z
;
then consider x being
object such that A118:
x in dom z
and A119:
z . x = {}
by FUNCT_1:def 3;
set fx =
f . x;
A120:
x in (f . x) \ (g . (f . x))
by A32, A118;
S1[
x,
f . x]
by A8, A118;
then
f . x in Y
;
then
S3[
f . x,
h . (f . x)]
by A31;
then consider H being
Function of
((f . x) \ (g . (f . x))),
(bool ((f . x) \ (g . (f . x)))) such that A121:
h . (f . x) = H
and
H is
one-to-one
and A122:
(
rng H is
with_non-empty_elements &
rng H is
c=-linear )
and
dom H in rng H
and
for
Z being
set st
Z in rng H &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H )
;
dom H = (f . x) \ (g . (f . x))
by FUNCT_2:def 1;
then A123:
H . x in rng H
by A120, FUNCT_1:def 3;
z . x = (g . (f . x)) \/ (H . x)
by A45, A118, A121;
hence
contradiction
by A119, A122, A123;
verum
end;
take
rng z
; ( Y c= rng z & rng z is with_non-empty_elements & rng z is c=-linear & card X = card (rng z) & ( for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z ) ) )
for x1, x2 being object st x1 in dom z & x2 in dom z & z . x1 = z . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom z & x2 in dom z & z . x1 = z . x2 implies x1 = x2 )
set f1 =
f . x1;
set f2 =
f . x2;
assume that A124:
x1 in dom z
and A125:
x2 in dom z
and A126:
z . x1 = z . x2
;
x1 = x2
A127:
(
z . x1 = H1(
x1) &
z . x2 = H1(
x2) )
by A45, A124, A125;
S1[
x2,
f . x2]
by A8, A125;
then A128:
f . x2 in Y
;
then
S3[
f . x2,
h . (f . x2)]
by A31;
then consider H2 being
Function of
((f . x2) \ (g . (f . x2))),
(bool ((f . x2) \ (g . (f . x2)))) such that A129:
h . (f . x2) = H2
and A130:
H2 is
one-to-one
and A131:
(
rng H2 is
with_non-empty_elements &
rng H2 is
c=-linear )
and
dom H2 in rng H2
and
for
Z being
set st
Z in rng H2 &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H2 )
;
dom H2 = (f . x2) \ (g . (f . x2))
by FUNCT_2:def 1;
then A132:
x2 in dom H2
by A32, A125;
then A133:
H2 . x2 in rng H2
by FUNCT_1:def 3;
then A134:
g . (f . x2) misses H2 . x2
by XBOOLE_1:63, XBOOLE_1:79;
S1[
x1,
f . x1]
by A8, A124;
then A135:
f . x1 in Y
;
then
S3[
f . x1,
h . (f . x1)]
by A31;
then consider H1 being
Function of
((f . x1) \ (g . (f . x1))),
(bool ((f . x1) \ (g . (f . x1)))) such that A136:
h . (f . x1) = H1
and
H1 is
one-to-one
and A137:
(
rng H1 is
with_non-empty_elements &
rng H1 is
c=-linear )
and
dom H1 in rng H1
and
for
Z being
set st
Z in rng H1 &
card Z <> 1 holds
ex
x being
set st
(
x in Z &
Z \ {x} in rng H1 )
;
dom H1 = (f . x1) \ (g . (f . x1))
by FUNCT_2:def 1;
then A138:
x1 in dom H1
by A32, A124;
then A139:
H1 . x1 in rng H1
by FUNCT_1:def 3;
then A140:
g . (f . x1) misses H1 . x1
by XBOOLE_1:63, XBOOLE_1:79;
A141:
f . x1,
f . x2 are_c=-comparable
by A1, A128, A135;
per cases
( f . x1 = f . x2 or ( f . x1 c= f . x2 & f . x1 <> f . x2 ) or ( f . x2 c= f . x1 & f . x1 <> f . x2 ) )
by A141;
suppose A142:
f . x1 = f . x2
;
x1 = x2then
H1 . x1 = H1 . x2
by A126, A127, A129, A134, A136, A140, XBOOLE_1:71;
hence
x1 = x2
by A129, A130, A132, A136, A138, A142, FUNCT_1:def 4;
verum end; suppose A143:
(
f . x1 c= f . x2 &
f . x1 <> f . x2 )
;
x1 = x2
S2[
f . x1,
g . (f . x1)]
by A23, A135;
then
g . (f . x1) c< f . x1
;
then
g . (f . x1) c= f . x1
;
then
(g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1
by XBOOLE_1:45;
then A144:
H1(
x2)
c= f . x1
by A126, A127, A136, A139, XBOOLE_1:9;
A145:
f . x1 c< f . x2
by A143;
S2[
f . x2,
g . (f . x2)]
by A23, A128;
then
f . x1 c= g . (f . x2)
by A135, A145;
then
H1(
x2)
c= g . (f . x2)
by A144;
then
H2 . x2 c= g . (f . x2)
by A129, XBOOLE_1:11;
hence
x1 = x2
by A131, A133, XBOOLE_1:67, XBOOLE_1:79;
verum end; suppose A146:
(
f . x2 c= f . x1 &
f . x1 <> f . x2 )
;
x1 = x2
S2[
f . x2,
g . (f . x2)]
by A23, A128;
then
g . (f . x2) c< f . x2
;
then
g . (f . x2) c= f . x2
;
then
(g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2
by XBOOLE_1:45;
then A147:
H1(
x1)
c= f . x2
by A126, A127, A129, A133, XBOOLE_1:9;
A148:
f . x2 c< f . x1
by A146;
S2[
f . x1,
g . (f . x1)]
by A23, A135;
then
f . x2 c= g . (f . x1)
by A128, A148;
then
H1(
x1)
c= g . (f . x1)
by A147;
then
H1 . x1 c= g . (f . x1)
by A136, XBOOLE_1:11;
hence
x1 = x2
by A137, A139, XBOOLE_1:67, XBOOLE_1:79;
verum end; end;
end;
then
z is one-to-one
by FUNCT_1:def 4;
then
X, rng z are_equipotent
by A46, WELLORD2:def 4;
hence
( Y c= rng z & rng z is with_non-empty_elements & rng z is c=-linear & card X = card (rng z) & ( for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z ) ) )
by A47, A61, A89, A117, CARD_1:5; verum