let L1 be lower-bounded continuous sup-Semilattice; ( L1 is infinite implies for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1 )
assume A1:
L1 is infinite
; for B1 being with_bottom CLbasis of L1 holds card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
let B1 be with_bottom CLbasis of L1; card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
consider a1 being object such that
A2:
a1 in B1
by XBOOLE_0:def 1;
reconsider a1 = a1 as Element of L1 by A2;
{} L1 c= B1
;
then
Way_Up (a1,({} L1)) in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) }
by A2;
then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as non empty set ;
defpred S1[ Element of B1 * , set ] means ex y being Element of L1 ex z being Subset of L1 st
( y = $1 /. 1 & z = rng (Del ($1,1)) & $2 = Way_Up (y,z) );
A3:
for x being Element of B1 * ex u being Element of WU st S1[x,u]
proof
let x be
Element of
B1 * ;
ex u being Element of WU st S1[x,u]
reconsider y =
x /. 1 as
Element of
L1 by TARSKI:def 3;
rng (Del (x,1)) c= rng x
by FINSEQ_3:106;
then A4:
rng (Del (x,1)) c= B1
by XBOOLE_1:1;
then reconsider z =
rng (Del (x,1)) as
Subset of
L1 by XBOOLE_1:1;
Way_Up (
y,
z)
in { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) }
by A4;
then reconsider u =
Way_Up (
y,
z) as
Element of
WU ;
take
u
;
S1[x,u]
take
y
;
ex z being Subset of L1 st
( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) )
take
z
;
( y = x /. 1 & z = rng (Del (x,1)) & u = Way_Up (y,z) )
thus
(
y = x /. 1 &
z = rng (Del (x,1)) &
u = Way_Up (
y,
z) )
;
verum
end;
consider f being Function of (B1 *),WU such that
A5:
for x being Element of B1 * holds S1[x,f . x]
from FUNCT_2:sch 3(A3);
A6:
dom f = B1 *
by FUNCT_2:def 1;
A7:
WU c= rng f
proof
let z be
object ;
TARSKI:def 3 ( not z in WU or z in rng f )
assume
z in WU
;
z in rng f
then consider a being
Element of
L1,
A being
finite Subset of
L1 such that A8:
z = Way_Up (
a,
A)
and A9:
a in B1
and A10:
A c= B1
;
reconsider a1 =
a as
Element of
B1 by A9;
consider p being
FinSequence such that A11:
A = rng p
by FINSEQ_1:52;
reconsider p =
p as
FinSequence of
B1 by A10, A11, FINSEQ_1:def 4;
set q =
<*a1*> ^ p;
A12:
<*a1*> ^ p in B1 *
by FINSEQ_1:def 11;
then consider y being
Element of
L1,
v being
Subset of
L1 such that A13:
y = (<*a1*> ^ p) /. 1
and A14:
v = rng (Del ((<*a1*> ^ p),1))
and A15:
f . (<*a1*> ^ p) = Way_Up (
y,
v)
by A5;
A16:
a = y
by A13, FINSEQ_5:15;
A = v
by A11, A14, WSIERP_1:40;
hence
z in rng f
by A6, A8, A12, A15, A16, FUNCT_1:def 3;
verum
end;
B1 is infinite
by A1, Th17;
then
card B1 = card (B1 *)
by CARD_4:24;
hence
card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= card B1
by A6, A7, CARD_1:12; verum