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) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
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) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
set IP = InclPoset (Filt (BoolePoset X));
set F = f -extension_to_hom ;
reconsider T = Top (InclPoset (Filt (BoolePoset X))) as Element of (InclPoset (Filt (BoolePoset X))) ;
reconsider E = {} as Subset of X by XBOOLE_1:2;
set Z = { ("/\" ( { (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 T } ;
A1: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {}
proof
assume not { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {} ; :: thesis: contradiction
then consider r being object such that
A2: r in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } by XBOOLE_0:def 1;
ex x being Element of (BoolePoset X) st
( r = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in E ) ) by A2;
hence contradiction ; :: thesis: verum
end;
A3: (f -extension_to_hom) . T = "\/" ( { ("/\" ( { (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 T } ,L) by Def3;
T = bool X by WAYBEL16:15;
then A4: "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } ,L) 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 T } ;
{ ("/\" ( { (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 T } is_<=_than "\/" ( { ("/\" ( { (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 T } ,L) by YELLOW_0:32;
then Top L <= "\/" ( { ("/\" ( { (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 T } ,L) by A4, A1;
hence (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:3; :: thesis: verum