let X be set ; for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
let L be non empty complete continuous Poset; for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
let f be Function of (FixedUltraFilters X), the carrier of L; f -extension_to_hom is monotone
let F1, F2 be Element of (InclPoset (Filt (BoolePoset X))); ORDERS_3:def 5 ( not F1 <= F2 or for b1, b2 being Element of the carrier of L holds
( not b1 = (f -extension_to_hom) . F1 or not b2 = (f -extension_to_hom) . F2 or b1 <= b2 ) )
set F = f -extension_to_hom ;
set F1s = { ("/\" ( { (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 F1 } ;
set F2s = { ("/\" ( { (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 F2 } ;
A1:
( ex_sup_of { ("/\" ( { (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 F1 } ,L & ex_sup_of { ("/\" ( { (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 F2 } ,L )
by YELLOW_0:17;
A2:
(f -extension_to_hom) . F1 = "\/" ( { ("/\" ( { (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 F1 } ,L)
by Def3;
assume
F1 <= F2
; for b1, b2 being Element of the carrier of L holds
( not b1 = (f -extension_to_hom) . F1 or not b2 = (f -extension_to_hom) . F2 or b1 <= b2 )
then A3:
F1 c= F2
by YELLOW_1:3;
A4:
{ ("/\" ( { (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 F1 } c= { ("/\" ( { (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 F2 }
A5:
(f -extension_to_hom) . F2 = "\/" ( { ("/\" ( { (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 F2 } ,L)
by Def3;
let FF1, FF2 be Element of L; ( not FF1 = (f -extension_to_hom) . F1 or not FF2 = (f -extension_to_hom) . F2 or FF1 <= FF2 )
assume
( FF1 = (f -extension_to_hom) . F1 & FF2 = (f -extension_to_hom) . F2 )
; FF1 <= FF2
hence
FF1 <= FF2
by A2, A5, A1, A4, YELLOW_0:34; verum