let X be set ; :: thesis: for L being non empty complete continuous Poset

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: (f -extension_to_hom) | (FixedUltraFilters X) = f

set FUF = FixedUltraFilters X;

set BP = BoolePoset X;

set IP = InclPoset (Filt (BoolePoset X));

A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;

set F = f -extension_to_hom ;

A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2

.= bool X by LATTICE3:def 1 ;

for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f

let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: (f -extension_to_hom) | (FixedUltraFilters X) = f

set FUF = FixedUltraFilters X;

set BP = BoolePoset X;

set IP = InclPoset (Filt (BoolePoset X));

A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;

set F = f -extension_to_hom ;

A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2

.= bool X by LATTICE3:def 1 ;

now :: thesis: ( FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) & FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds

((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )

hence
(f -extension_to_hom) | (FixedUltraFilters X) = f
; :: thesis: verum((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )

A3:
dom (f -extension_to_hom) = the carrier of (InclPoset (Filt (BoolePoset X)))
by FUNCT_2:def 1;

hence FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) by A1, Th9, RELAT_1:62; :: thesis: ( FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds

((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )

thus FixedUltraFilters X = dom f by FUNCT_2:def 1; :: thesis: for xf being object st xf in FixedUltraFilters X holds

((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf

let xf be object ; :: thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )

assume A4: xf in FixedUltraFilters X ; :: thesis: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf

then reconsider FUF9 = FixedUltraFilters X as non empty Subset-Family of (BoolePoset X) ;

A5: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf by A4, FUNCT_1:49;

FixedUltraFilters X c= dom (f -extension_to_hom) by A1, A3, Th9;

then reconsider x9 = xf as Element of (InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def 1;

reconsider xf9 = xf as Element of FUF9 by A4;

set 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 x9 } ;

reconsider f9 = f as Function of FUF9, the carrier of L ;

f9 . xf9 is Element of L ;

then reconsider fxf = f . xf9 as Element of L ;

consider xx being Element of (BoolePoset X) such that

A6: xf = uparrow xx and

A7: ex y being Element of X st xx = {y} by A4;

A8: { ("/\" ( { (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 x9 } is_<=_than fxf

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a holds

fxf <= a

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,L by YELLOW_0:17;

then f . xf = "\/" ( { ("/\" ( { (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 x9 } ,L) by A8, A13, YELLOW_0:def 9;

hence ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf by A5, Def3; :: thesis: verum

end;hence FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) by A1, Th9, RELAT_1:62; :: thesis: ( FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds

((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )

thus FixedUltraFilters X = dom f by FUNCT_2:def 1; :: thesis: for xf being object st xf in FixedUltraFilters X holds

((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf

let xf be object ; :: thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )

assume A4: xf in FixedUltraFilters X ; :: thesis: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf

then reconsider FUF9 = FixedUltraFilters X as non empty Subset-Family of (BoolePoset X) ;

A5: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf by A4, FUNCT_1:49;

FixedUltraFilters X c= dom (f -extension_to_hom) by A1, A3, Th9;

then reconsider x9 = xf as Element of (InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def 1;

reconsider xf9 = xf as Element of FUF9 by A4;

set 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 x9 } ;

reconsider f9 = f as Function of FUF9, the carrier of L ;

f9 . xf9 is Element of L ;

then reconsider fxf = f . xf9 as Element of L ;

consider xx being Element of (BoolePoset X) such that

A6: xf = uparrow xx and

A7: ex y being Element of X st xx = {y} by A4;

A8: { ("/\" ( { (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 x9 } is_<=_than fxf

proof

A13:
for a being Element of L st { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b 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 x9 } or b <= fxf )

assume b 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 x9 } ; :: thesis: b <= fxf

then consider Y being Subset of X such that

A9: b = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) and

A10: Y in x9 ;

set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L by YELLOW_0:17;

then A11: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } is_>=_than b by A9, YELLOW_0:def 10;

reconsider Y = Y as Element of (BoolePoset X) by A6, A10;

consider y being Element of X such that

A12: xx = {y} by A7;

xx <= Y by A6, A10, WAYBEL_0:18;

then xx c= Y by YELLOW_1:2;

then y in Y by A12, ZFMISC_1:31;

then fxf in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A6, A12;

hence b <= fxf by A11; :: thesis: verum

end;( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } or b <= fxf )

assume b 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 x9 } ; :: thesis: b <= fxf

then consider Y being Subset of X such that

A9: b = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) and

A10: Y in x9 ;

set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L by YELLOW_0:17;

then A11: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } is_>=_than b by A9, YELLOW_0:def 10;

reconsider Y = Y as Element of (BoolePoset X) by A6, A10;

consider y being Element of X such that

A12: xx = {y} by A7;

xx <= Y by A6, A10, WAYBEL_0:18;

then xx c= Y by YELLOW_1:2;

then y in Y by A12, ZFMISC_1:31;

then fxf in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A6, A12;

hence b <= fxf by A11; :: thesis: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a holds

fxf <= a

proof

ex_sup_of { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
xx <= xx
;

then reconsider Y = xx as Element of x9 by A6, WAYBEL_0:18;

set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

consider y being Element of X such that

A14: xx = {y} by A7;

( x = {z} & z in Y ) } = {fxf} by TARSKI:2;

then fxf = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) by YELLOW_0:39;

then A18: fxf 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 x9 } by A2;

let a be Element of L; :: thesis: ( { ("/\" ( { (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 x9 } is_<=_than a implies fxf <= a )

assume { ("/\" ( { (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 x9 } is_<=_than a ; :: thesis: fxf <= a

hence fxf <= a by A18; :: thesis: verum

end;then reconsider Y = xx as Element of x9 by A6, WAYBEL_0:18;

set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ;

consider y being Element of X such that

A14: xx = {y} by A7;

now :: thesis: for p being object holds

( ( p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) )

then
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( ( p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) )

let p be object ; :: thesis: ( ( p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) )

( x = {z} & z in Y ) }

then A17: p = fxf by TARSKI:def 1;

y in Y by A14, TARSKI:def 1;

hence p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A6, A14, A17; :: thesis: verum

end;( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ) )

hereby :: thesis: ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } )

assume
p in {fxf}
; :: thesis: p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st ( x = {z} & z in Y ) } )

assume
p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ; :: thesis: p in {fxf}

then consider r being Element of (BoolePoset X) such that

A15: p = f . (uparrow r) and

A16: ex z being Element of X st

( r = {z} & z in Y ) ;

xx = r by A14, A16, TARSKI:def 1;

hence p in {fxf} by A6, A15, TARSKI:def 1; :: thesis: verum

end;( x = {z} & z in Y ) } ; :: thesis: p in {fxf}

then consider r being Element of (BoolePoset X) such that

A15: p = f . (uparrow r) and

A16: ex z being Element of X st

( r = {z} & z in Y ) ;

xx = r by A14, A16, TARSKI:def 1;

hence p in {fxf} by A6, A15, TARSKI:def 1; :: thesis: verum

( x = {z} & z in Y ) }

then A17: p = fxf by TARSKI:def 1;

y in Y by A14, TARSKI:def 1;

hence p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } by A6, A14, A17; :: thesis: verum

( x = {z} & z in Y ) } = {fxf} by TARSKI:2;

then fxf = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st

( x = {z} & z in Y ) } ,L) by YELLOW_0:39;

then A18: fxf 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 x9 } by A2;

let a be Element of L; :: thesis: ( { ("/\" ( { (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 x9 } is_<=_than a implies fxf <= a )

assume { ("/\" ( { (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 x9 } is_<=_than a ; :: thesis: fxf <= a

hence fxf <= a by A18; :: thesis: verum

( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,L by YELLOW_0:17;

then f . xf = "\/" ( { ("/\" ( { (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 x9 } ,L) by A8, A13, YELLOW_0:def 9;

hence ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf by A5, Def3; :: thesis: verum