set F = f -extension_to_hom ;
set IP = InclPoset (Filt (BoolePoset X));
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); WAYBEL_0:def 37 ( 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 )
; 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 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 ;
( ( 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 ( 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 }
;
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;
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 }
;
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;
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))
; WAYBEL_0:def 31 ( 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; "\/" (((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
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;
(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; verum