set F = f -extension_to_hom ;
set IP = InclPoset (Filt (BoolePoset X));
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def 37 :: thesis: ( Fs is empty or not Fs is directed or f -extension_to_hom preserves_sup_of Fs )
assume A1: ( not Fs is empty & Fs is directed ) ; :: thesis: f -extension_to_hom preserves_sup_of Fs
reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A1;
set FFsU = { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } ;
reconsider sFs = sup Fs as Element of (InclPoset (Filt (BoolePoset X))) ;
set FFs = { ("/\" ( { (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 sFs } ;
A2: sup Fs = union Fs by A1, Th1;
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 ) } ,L)) where Y is Subset of X : Y in sFs } implies p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } ) & ( p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } 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 ) } ,L)) where Y is Subset of X : Y in sFs } ) )
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 ) } ,L)) where Y is Subset of X : Y in sFs } implies p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } ) & ( p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } 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 ) } ,L)) where Y is Subset of X : Y in sFs } ) )
hereby :: thesis: ( p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } 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 ) } ,L)) where Y is Subset of X : Y in sFs } )
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 ) } ,L)) where Y is Subset of X : Y in sFs } ; :: thesis: p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum }
then consider Y being Subset of X such that
A3: p = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A4: Y in sFs ;
consider YY being set such that
A5: Y in YY and
A6: YY in Fs by A2, A4, TARSKI:def 4;
A7: { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 ) } ,L)) where Y1 is Subset of X : Y1 in YY } 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 YY } where YY is Element of Fs9 : verum } by A6;
p in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y1 ) } ,L)) where Y1 is Subset of X : Y1 in YY } by A3, A5;
hence p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } by A7, TARSKI:def 4; :: thesis: verum
end;
assume p in union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } ; :: 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 ) } ,L)) where Y is Subset of X : Y in sFs }
then consider r being set such that
A8: p in r and
A9: r 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 YY } where YY is Element of Fs9 : verum } by TARSKI:def 4;
consider YY being Element of Fs9 such that
A10: r = { ("/\" ( { (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 YY } by A9;
consider Y being Subset of X such that
A11: p = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A12: Y in YY by A8, A10;
Y in sFs by A2, A12, TARSKI:def 4;
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 ) } ,L)) where Y is Subset of X : Y in sFs } by A11; :: thesis: verum
end;
then A13: { ("/\" ( { (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 sFs } = union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } by TARSKI:2;
set Zs = { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ;
assume ex_sup_of Fs, InclPoset (Filt (BoolePoset X)) ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (f -extension_to_hom) .: Fs,L & "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X))))) )
thus ex_sup_of (f -extension_to_hom) .: Fs,L by YELLOW_0:17; :: thesis: "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X)))))
{ { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } c= bool the carrier of L
proof
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r 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 YY } where YY is Element of Fs9 : verum } or r in bool the carrier of L )
reconsider rr = r as set by TARSKI:1;
assume r 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 YY } where YY is Element of Fs9 : verum } ; :: thesis: r in bool the carrier of L
then consider YY being Element of Fs9 such that
A14: r = { ("/\" ( { (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 YY } ;
rr c= the carrier of L
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in rr or s in the carrier of L )
assume s in rr ; :: thesis: s in the carrier of L
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 YY ) by A14;
hence s in the carrier of L ; :: thesis: verum
end;
hence r in bool the carrier of L ; :: thesis: verum
end;
then A15: "\/" ((union { { ("/\" ( { (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 YY } where YY is Element of Fs9 : verum } ),L) = "\/" ( { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ,L) by Lm2;
A16: now :: thesis: for r being object holds
( ( r in (f -extension_to_hom) .: Fs implies r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ) & ( r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } implies r in (f -extension_to_hom) .: Fs ) )
let r be object ; :: thesis: ( ( r in (f -extension_to_hom) .: Fs implies r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ) & ( r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } implies r in (f -extension_to_hom) .: Fs ) )
hereby :: thesis: ( r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } implies r in (f -extension_to_hom) .: Fs )
assume r in (f -extension_to_hom) .: Fs ; :: thesis: r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } }
then consider YY being object such that
A17: YY in the carrier of (InclPoset (Filt (BoolePoset X))) and
A18: YY in Fs and
A19: (f -extension_to_hom) . YY = r by FUNCT_2:64;
reconsider YY = YY as Element of Fs by A18;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) by A17;
set Zi = { ("/\" ( { (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 YY9 } ;
{ ("/\" ( { (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 YY9 } c= the carrier of L
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t 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 YY9 } or t in the carrier of L )
assume t 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 YY9 } ; :: thesis: t in the carrier of L
then ex Y being Subset of X st
( t = "/\" ( { (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 YY9 ) ;
hence t in the carrier of L ; :: thesis: verum
end;
then reconsider Zi = { ("/\" ( { (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 YY9 } as Subset of L ;
A20: Zi 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 YY } where YY is Element of Fs9 : verum } ;
(f -extension_to_hom) . YY9 = "\/" ( { ("/\" ( { (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 YY9 } ,L) by Def3;
hence r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } by A19, A20; :: thesis: verum
end;
assume r in { (sup Z) where Z is Subset of L : Z 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 YY } where YY is Element of Fs9 : verum } } ; :: thesis: r in (f -extension_to_hom) .: Fs
then consider Z being Subset of L such that
A21: r = sup Z and
A22: Z 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 YY } where YY is Element of Fs9 : verum } ;
consider YY being Element of Fs such that
A23: 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 YY } by A22;
reconsider YY = YY as Element of Fs9 ;
reconsider YY9 = YY as Element of (InclPoset (Filt (BoolePoset X))) ;
(f -extension_to_hom) . YY9 = "\/" ( { ("/\" ( { (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 YY9 } ,L) by Def3;
hence r in (f -extension_to_hom) .: Fs by A21, A23, FUNCT_2:35; :: thesis: verum
end;
(f -extension_to_hom) . sFs = "\/" ( { ("/\" ( { (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 sFs } ,L) by Def3;
hence "\/" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("\/" (Fs,(InclPoset (Filt (BoolePoset X))))) by A15, A13, A16, TARSKI:2; :: thesis: verum