let X be set ; :: thesis: for L being non empty complete continuous Poset
for f being Function of FixedUltraFilters X,the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let L be non empty complete continuous Poset; :: thesis: for f being Function of FixedUltraFilters X,the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let f be Function of FixedUltraFilters X,the carrier of L; :: thesis: for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; :: thesis: ( h | (FixedUltraFilters X) = f implies h = f -extension_to_hom )
assume A1:
h | (FixedUltraFilters X) = f
; :: thesis: h = f -extension_to_hom
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
set cL = the carrier of L;
set F = f -extension_to_hom ;
A2:
InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #)
by YELLOW_1:def 1;
A3: the carrier of (BoolePoset X) =
the carrier of (LattPOSet (BooleLatt X))
by YELLOW_1:def 2
.=
bool X
by LATTICE3:def 1
;
reconsider h' = h as Function of the carrier of (InclPoset (Filt (BoolePoset X))),the carrier of L ;
reconsider F' = f -extension_to_hom as Function of the carrier of (InclPoset (Filt (BoolePoset X))),the carrier of L ;
now let Fi be
Element of the
carrier of
(InclPoset (Filt (BoolePoset X)));
:: thesis: h' . Fi = F' . Fi
Fi in Filt (BoolePoset X)
by A2;
then consider FF being
Filter of
(BoolePoset X) such that A4:
Fi = FF
;
A5:
FF = "\/" { ("/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) where Y is Subset of X : Y in FF } ,
(InclPoset (Filt (BoolePoset X)))
by Th11;
set Xs =
{ ("/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) where Y is Subset of X : Y in FF } ;
A6:
(
h is
infs-preserving &
h is
directed-sups-preserving )
by WAYBEL16:def 1;
A7:
{ ("/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) where Y is Subset of X : Y in FF } c= the
carrier of
(InclPoset (Filt (BoolePoset X)))
then reconsider Xs =
{ ("/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) where Y is Subset of X : Y in FF } as non
empty Subset of
(InclPoset (Filt (BoolePoset X))) by A7;
Xs is
directed
proof
let a,
b be
Element of
(InclPoset (Filt (BoolePoset X)));
:: according to WAYBEL_0:def 1 :: thesis: ( not a in Xs or not b in Xs or ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 ) )
assume A10:
(
a in Xs &
b in Xs )
;
:: thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
then consider Ya being
Subset of
X such that A11:
a = "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ,
(InclPoset (Filt (BoolePoset X)))
and A12:
Ya in FF
;
reconsider Ya' =
Ya as
Element of
FF by A12;
consider Yb being
Subset of
X such that A13:
b = "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ,
(InclPoset (Filt (BoolePoset X)))
and A14:
Yb in FF
by A10;
reconsider Yb' =
Yb as
Element of
FF by A14;
set Xsa =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ;
set Xsb =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ;
per cases
( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty or { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty or ( not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty & not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty ) )
;
suppose A17:
( not
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is
empty & not
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is
empty )
;
:: thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } c= the
carrier of
(InclPoset (Filt (BoolePoset X)))
then reconsider Xsa =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } as non
empty Subset of
(InclPoset (Filt (BoolePoset X))) by A17;
A19:
"/\" Xsa,
(InclPoset (Filt (BoolePoset X))) = meet Xsa
by WAYBEL16:10;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } c= the
carrier of
(InclPoset (Filt (BoolePoset X)))
then reconsider Xsb =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } as non
empty Subset of
(InclPoset (Filt (BoolePoset X))) by A17;
A21:
"/\" Xsb,
(InclPoset (Filt (BoolePoset X))) = meet Xsb
by WAYBEL16:10;
consider Yab being
Element of
(BoolePoset X) such that A22:
Yab in FF
and A23:
Yab <= Ya'
and A24:
Yab <= Yb'
by WAYBEL_0:def 2;
reconsider Yab =
Yab as
Element of
FF by A22;
set c =
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)));
set Xsc =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ;
thus
ex
b1 being
Element of the
carrier of
(InclPoset (Filt (BoolePoset X))) st
(
b1 in Xs &
a <= b1 &
b <= b1 )
:: thesis: verumproof
per cases
( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty or not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty )
;
suppose
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is
empty
;
:: thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )then A25:
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X))) = Top (InclPoset (Filt (BoolePoset X)))
;
take
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
;
:: thesis: ( "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) in Xs & a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) & b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) )thus
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X))) in Xs
by A3;
:: thesis: ( a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) & b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) )thus
a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
by A25, YELLOW_0:45;
:: thesis: b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))thus
b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
by A25, YELLOW_0:45;
:: thesis: verum end; suppose A26:
not
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is
empty
;
:: thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } c= the
carrier of
(InclPoset (Filt (BoolePoset X)))
then reconsider Xsc =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } as non
empty Subset of
(InclPoset (Filt (BoolePoset X))) by A26;
A28:
"/\" Xsc,
(InclPoset (Filt (BoolePoset X))) = meet Xsc
by WAYBEL16:10;
take
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
;
:: thesis: ( "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) in Xs & a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) & b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) )thus
"/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X))) in Xs
by A3;
:: thesis: ( a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) & b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))) )
a c= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
hence
a <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
by YELLOW_1:3;
:: thesis: b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))
b c= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
hence
b <= "/\" { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,
(InclPoset (Filt (BoolePoset X)))
by YELLOW_1:3;
:: thesis: verum end;
end; end;
end; then A39:
h preserves_sup_of Xs
by A6, WAYBEL_0:def 37;
A40:
ex_sup_of Xs,
InclPoset (Filt (BoolePoset X))
by YELLOW_0:17;
set Xsf =
{ ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in FF } ;
set FUF =
FixedUltraFilters X;
now let s be
set ;
:: thesis: ( ( s in h .: Xs implies s in { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in FF } ) & ( s in { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in FF } implies s in h .: Xs ) )assume
s in { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in FF }
;
:: thesis: s in h .: Xsthen consider Y being
Subset of
X such that A57:
s = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
and A58:
Y in FF
;
set Xsi =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the
carrier of
(InclPoset (Filt (BoolePoset X)))
then reconsider Xsi =
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as
Subset of
(InclPoset (Filt (BoolePoset X))) ;
A60:
h preserves_inf_of Xsi
by A6, WAYBEL_0:def 32;
ex_inf_of Xsi,
InclPoset (Filt (BoolePoset X))
by YELLOW_0:17;
then A61:
inf (h .: Xsi) = h . (inf Xsi)
by A60, WAYBEL_0:def 30;
set Xsif =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
A62:
inf Xsi in Xs
by A58;
then
h .: Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
by TARSKI:2;
hence
s in h .: Xs
by A57, A61, A62, FUNCT_2:43;
:: thesis: verum end; then A72:
h .: Xs = { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in FF }
by TARSKI:2;
thus h' . Fi =
sup (h .: Xs)
by A4, A5, A39, A40, WAYBEL_0:def 31
.=
F' . Fi
by A4, A72, Def3
;
:: thesis: verum end;
hence
h = f -extension_to_hom
by FUNCT_2:113; :: thesis: verum