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 is monotone
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 is monotone
let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: f -extension_to_hom is monotone
let F1, F2 be Element of (InclPoset (Filt (BoolePoset X))); :: according to ORDERS_3:def 5 :: thesis: ( 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 ; :: thesis: 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 }
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 F1 } or 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 F2 } )
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 F1 } ; :: thesis: 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 F2 }
then ex Y being Subset of X st
( s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) & Y in F1 ) ;
hence 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 F2 } by A3; :: thesis: verum
end;
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; :: thesis: ( 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 ) ; :: thesis: FF1 <= FF2
hence FF1 <= FF2 by A2, A5, A1, A4, YELLOW_0:34; :: thesis: verum