set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set F = f -extension_to_hom ;
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
set cL = the carrier of L;
set FUF = FixedUltraFilters X;
A1:
InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #)
by YELLOW_1:def 1;
A2:
BoolePoset X = InclPoset (bool X)
by YELLOW_1:4;
A3:
InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #)
by YELLOW_1:def 1;
then A4:
the carrier of (BoolePoset X) = bool X
by YELLOW_1:4;
let Fs be Subset of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def 32 :: thesis: f -extension_to_hom preserves_inf_of Fs
assume
ex_inf_of Fs, InclPoset (Filt (BoolePoset X))
; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (f -extension_to_hom ) .: Fs,L & "/\" ((f -extension_to_hom ) .: Fs),L = (f -extension_to_hom ) . ("/\" Fs,(InclPoset (Filt (BoolePoset X)))) )
thus
ex_inf_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))))
per cases
( Fs is empty or not Fs is empty )
;
suppose
not
Fs is
empty
;
:: thesis: "/\" ((f -extension_to_hom ) .: Fs),L = (f -extension_to_hom ) . ("/\" Fs,(InclPoset (Filt (BoolePoset X))))then reconsider Fs' =
Fs as non
empty Subset of
(InclPoset (Filt (BoolePoset X))) ;
not
{} in Fs'
;
then
Fs' is
with_non-empty_elements
by SETFAM_1:def 9;
then reconsider K =
id Fs' as
V8()
ManySortedSet of ;
defpred S1[
set ,
set ,
set ]
means X = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in L ) } ,
L;
A7:
for
i being
set st
i in Fs' holds
for
s being
set st
s in K . i holds
ex
y being
set st
(
y in (Fs' --> the carrier of L) . i &
S1[
y,
s,
i] )
proof
let i be
set ;
:: thesis: ( i in Fs' implies for s being set st s in K . i holds
ex y being set st
( y in (Fs' --> the carrier of L) . i & S1[y,s,i] ) )
assume A8:
i in Fs'
;
:: thesis: for s being set st s in K . i holds
ex y being set st
( y in (Fs' --> the carrier of L) . i & S1[y,s,i] )
let s be
set ;
:: thesis: ( s in K . i implies ex y being set st
( y in (Fs' --> the carrier of L) . i & S1[y,s,i] ) )
assume
s in K . i
;
:: thesis: ex y being set st
( y in (Fs' --> the carrier of L) . i & S1[y,s,i] )
take y =
"/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s ) } ,
L;
:: thesis: ( y in (Fs' --> the carrier of L) . i & S1[y,s,i] )
y in the
carrier of
L
;
hence
y in (Fs' --> the carrier of L) . i
by A8, FUNCOP_1:13;
:: thesis: S1[y,s,i]
thus
S1[
y,
s,
i]
;
:: thesis: verum
end; consider FD being
ManySortedFunction of
K,
Fs' --> the
carrier of
L such that A9:
for
i being
set st
i in Fs' holds
ex
g being
Function of
(K . i),
((Fs' --> the carrier of L) . i) st
(
g = FD . i & ( for
s being
set st
s in K . i holds
S1[
g . s,
s,
i] ) )
from MSSUBFAM:sch 1(A7);
A10:
dom FD = Fs'
by PARTFUN1:def 4;
deffunc H1(
Element of
Fs')
-> set =
{ ("/\" { (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 X } ;
defpred S2[
Element of
Fs']
means rng (FD . X) = H1(
X);
A11:
for
s being
Element of
Fs' holds
S2[
s]
proof
let s be
Element of
Fs';
:: thesis: S2[s]
now let t be
set ;
:: thesis: ( ( t in rng (FD . s) implies t in H1(s) ) & ( t in H1(s) implies t in rng (FD . s) ) )hereby :: thesis: ( t in H1(s) implies t in rng (FD . s) )
assume
t in rng (FD . s)
;
:: thesis: t in H1(s)then consider u being
set such that A12:
u in dom (FD . s)
and A13:
t = (FD . s) . u
by FUNCT_1:def 5;
A14:
dom (FD . s) = K . s
by FUNCT_2:def 1;
consider g being
Function of
(K . s),
((Fs' --> the carrier of L) . s) such that A15:
g = FD . s
and A16:
for
u being
set st
u in K . s holds
S1[
g . u,
u,
s]
by A9;
A17:
g . u = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in u ) } ,
L
by A12, A16;
A18:
K . s = s
by FUNCT_1:35;
s in the
carrier of
(InclPoset (Filt (BoolePoset X)))
;
then consider FF being
Filter of
(BoolePoset X) such that A19:
s = FF
by A1;
reconsider u =
u as
Subset of
X by A3, A12, A14, A18, A19, YELLOW_1:4;
u in s
by A12, A14, FUNCT_1:35;
hence
t in H1(
s)
by A13, A15, A17;
:: thesis: verum
end; assume
t in H1(
s)
;
:: thesis: t in rng (FD . s)then consider Y being
Subset of
X such that A20:
t = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
and A21:
Y in s
;
A22:
dom (FD . s) = K . s
by FUNCT_2:def 1;
A23:
K . s = s
by FUNCT_1:35;
A24:
Y in dom (FD . s)
by A21, A22, FUNCT_1:35;
consider g being
Function of
(K . s),
((Fs' --> the carrier of L) . s) such that A25:
g = FD . s
and A26:
for
u being
set st
u in K . s holds
S1[
g . u,
u,
s]
by A9;
g . Y = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
by A21, A23, A26;
hence
t in rng (FD . s)
by A20, A24, A25, FUNCT_1:def 5;
:: thesis: verum end;
hence
S2[
s]
by TARSKI:2;
:: thesis: verum
end; reconsider FD =
FD as
DoubleIndexedSet of
K,
L ;
then
(f -extension_to_hom ) .: Fs = rng (Sups )
by TARSKI:2;
then A32:
inf ((f -extension_to_hom ) .: Fs) = Inf
by YELLOW_2:def 6;
for
j being
Element of
Fs' holds
rng (FD . j) is
directed
proof
let j be
Element of
Fs';
:: thesis: rng (FD . j) is directed let k,
m be
Element of
L;
:: according to WAYBEL_0:def 1 :: thesis: ( not k in rng (FD . j) or not m in rng (FD . j) or ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 ) )
assume A33:
(
k in rng (FD . j) &
m in rng (FD . j) )
;
:: thesis: ex b1 being Element of the carrier of L st
( b1 in rng (FD . j) & k <= b1 & m <= b1 )
then consider kd being
set such that A34:
kd in dom (FD . j)
and A35:
(FD . j) . kd = k
by FUNCT_1:def 5;
consider md being
set such that A36:
md in dom (FD . j)
and A37:
(FD . j) . md = m
by A33, FUNCT_1:def 5;
A38:
dom (FD . j) = K . j
by FUNCT_2:def 1;
A39:
K . j = j
by FUNCT_1:35;
j in the
carrier of
(InclPoset (Filt (BoolePoset X)))
;
then consider FF being
Filter of
(BoolePoset X) such that A40:
j = FF
by A1;
reconsider kd =
kd as
Element of
(BoolePoset X) by A34, A38, A39, A40;
reconsider md =
md as
Element of
(BoolePoset X) by A36, A38, A39, A40;
consider nd being
Element of
(BoolePoset X) such that A41:
(
nd in FF &
nd <= kd &
nd <= md )
by A34, A36, A39, A40, WAYBEL_0:def 2;
A42:
rng (FD . j) = H1(
j)
by A11;
set n =
(FD . j) . nd;
(FD . j) . nd in rng (FD . j)
by A38, A39, A40, A41, FUNCT_1:def 5;
then consider Y being
Subset of
X such that A43:
(FD . j) . nd = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
and
Y in j
by A42;
reconsider n =
(FD . j) . nd as
Element of
L by A43;
take
n
;
:: thesis: ( n in rng (FD . j) & k <= n & m <= n )
thus
n in rng (FD . j)
by A38, A39, A40, A41, FUNCT_1:def 5;
:: thesis: ( k <= n & m <= n )
consider g being
Function of
(K . j),
((Fs' --> the carrier of L) . j) such that A44:
g = FD . j
and A45:
for
u being
set st
u in K . j holds
S1[
g . u,
u,
j]
by A9;
set kds =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ;
A46:
g . kd = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ,
L
by A34, A45;
set nds =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ;
A47:
g . nd = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ,
L
by A39, A40, A41, A45;
A48:
nd c= kd
by A41, YELLOW_1:2;
A49:
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ,
L
by YELLOW_0:17;
A50:
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ,
L
by YELLOW_0:17;
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } c= { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) }
hence
k <= n
by A35, A44, A46, A47, A49, A50, YELLOW_0:35;
:: thesis: m <= n
set mds =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ;
A54:
g . md = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ,
L
by A36, A45;
A55:
nd c= md
by A41, YELLOW_1:2;
A56:
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ,
L
by YELLOW_0:17;
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } c= { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) }
hence
m <= n
by A37, A44, A47, A50, A54, A56, YELLOW_0:35;
:: thesis: verum
end; then A60:
Inf =
Sup
by WAYBEL_5:19
.=
"\/" (rng (Infs )),
L
by YELLOW_2:def 5
;
meet Fs' is
Filter of
(BoolePoset X)
by WAYBEL16:9;
then
meet Fs' in Filt (BoolePoset X)
;
then reconsider mFs =
meet Fs' as
Element of the
carrier of
(InclPoset (Filt (BoolePoset X))) by A1;
A61:
inf Fs' = meet Fs'
by WAYBEL16:10;
set smFs =
{ ("/\" { (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 mFs } ;
A62:
(f -extension_to_hom ) . (meet Fs') = "\/" { ("/\" { (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 mFs } ,
L
by Def3;
now let r be
set ;
:: thesis: ( ( r in rng (Infs ) implies 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 mFs } ) & ( 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 mFs } implies r in rng (Infs ) ) )reconsider pdFD =
product (doms FD) as non
empty functional set ;
reconsider dFFD =
(product (doms FD)) --> Fs' as
ManySortedSet of ;
reconsider FFD =
Frege FD as
DoubleIndexedSet of
dFFD,
L ;
A63:
dom FFD = pdFD
by PARTFUN1:def 4;
deffunc H2(
Element of
pdFD)
-> set =
{ ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in X . u ) } ,L) where u is Element of Fs' : u in dom (FFD . X) } ;
A64:
now let s be
Element of
pdFD;
:: thesis: rng (FFD . s) = H2(s)A65:
dom FD = dom (FFD . s)
by A63, WAYBEL_5:8;
now let t be
set ;
:: thesis: ( ( t in rng (FFD . s) implies t in H2(s) ) & ( t in H2(s) implies t in rng (FFD . s) ) )hereby :: thesis: ( t in H2(s) implies t in rng (FFD . s) )
assume
t in rng (FFD . s)
;
:: thesis: t in H2(s)then consider u being
set such that A66:
u in dom (FFD . s)
and A67:
t = (FFD . s) . u
by FUNCT_1:def 5;
A68:
(FFD . s) . u = (FD . u) . (s . u)
by A63, A65, A66, WAYBEL_5:9;
reconsider u =
u as
Element of
Fs' by A65, A66, PARTFUN1:def 4;
consider g being
Function of
(K . u),
((Fs' --> the carrier of L) . u) such that A69:
g = FD . u
and A70:
for
v being
set st
v in K . u holds
S1[
g . v,
v,
u]
by A9;
dom (FD . u) = K . u
by FUNCT_2:def 1;
then
s . u in K . u
by A10, A63, WAYBEL_5:9;
then
g . (s . u) = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,
L
by A70;
hence
t in H2(
s)
by A66, A67, A68, A69;
:: thesis: verum
end; assume
t in H2(
s)
;
:: thesis: t in rng (FFD . s)then consider u being
Element of
Fs' such that A71:
t = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,
L
and A72:
u in dom (FFD . s)
;
reconsider u =
u as
Element of
Fs' ;
consider g being
Function of
(K . u),
((Fs' --> the carrier of L) . u) such that A73:
g = FD . u
and A74:
for
v being
set st
v in K . u holds
S1[
g . v,
v,
u]
by A9;
dom (FD . u) = K . u
by FUNCT_2:def 1;
then
s . u in K . u
by A10, A63, WAYBEL_5:9;
then
g . (s . u) = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,
L
by A74;
hence
t in rng (FFD . s)
by A63, A65, A71, A72, A73, WAYBEL_5:9;
:: thesis: verum end; hence
rng (FFD . s) = H2(
s)
by TARSKI:2;
:: thesis: verum end; hereby :: thesis: ( 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 mFs } implies r in rng (Infs ) )
assume
r in rng (Infs )
;
:: thesis: 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 mFs } then consider s being
Element of
pdFD such that A75:
r = Inf
by WAYBEL_5:14;
A76:
dom FD = dom (FFD . s)
by A63, WAYBEL_5:8;
A77:
dom s = dom FD
by A63, WAYBEL_5:8;
union (rng s) c= X
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in union (rng s) or t in X )
assume
t in union (rng s)
;
:: thesis: t in X
then consider te being
set such that A78:
(
t in te &
te in rng s )
by TARSKI:def 4;
consider u being
set such that A79:
(
u in dom s &
te = s . u )
by A78, FUNCT_1:def 5;
FD . u is
Function of
(K . u),the
carrier of
L
by A10, A77, A79, WAYBEL_5:6;
then dom (FD . u) =
K . u
by FUNCT_2:def 1
.=
u
by A10, A77, A79, FUNCT_1:34
;
then A80:
te in u
by A63, A77, A79, WAYBEL_5:9;
u in the
carrier of
(InclPoset (Filt (BoolePoset X)))
by A10, A77, A79;
then consider FF being
Filter of
(BoolePoset X) such that A81:
u = FF
by A1;
thus
t in X
by A4, A78, A80, A81;
:: thesis: verum
end; then reconsider Y =
union (rng s) as
Subset of
X ;
set Ys =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
now let Z be
set ;
:: thesis: ( Z in Fs' implies Y in Z )assume A82:
Z in Fs'
;
:: thesis: Y in Zthen
Z in the
carrier of
(InclPoset (Filt (BoolePoset X)))
;
then consider FF being
Filter of
(BoolePoset X) such that A83:
Z = FF
by A1;
s . Z in rng s
by A10, A77, A82, FUNCT_1:def 5;
then A84:
s . Z c= Y
by ZFMISC_1:92;
A85:
s . Z in dom (FD . Z)
by A10, A63, A82, WAYBEL_5:9;
FD . Z is
Function of
(K . Z),the
carrier of
L
by A82, WAYBEL_5:6;
then A86:
dom (FD . Z) =
K . Z
by FUNCT_2:def 1
.=
Z
by A82, FUNCT_1:34
;
reconsider sZ =
s . Z as
Element of
(BoolePoset X) by A2, A3, A84, XBOOLE_1:1;
reconsider Y' =
Y as
Element of
(BoolePoset X) by A3, YELLOW_1:4;
sZ <= Y'
by A84, YELLOW_1:2;
hence
Y in Z
by A83, A85, A86, WAYBEL_0:def 20;
:: thesis: verum end; then
Y in mFs
by SETFAM_1:def 1;
then A87:
"/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
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 mFs }
;
set idFFDs =
{ { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } ;
A88:
{ { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } c= bool the
carrier of
L
then A102:
H2(
s)
= { (inf YY) where YY is Subset of L : YY in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } }
by TARSKI:2;
A103:
"/\" (rng (FFD . s)),
L =
"/\" H2(
s),
L
by A64
.=
"/\" (union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } ),
L
by A88, A102, Lm1
;
now let t be
set ;
:: thesis: ( ( t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } implies t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ) & ( t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } ) )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 ) }
;
:: thesis: t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } then consider x being
Element of
(BoolePoset X) such that A111:
t = f . (uparrow x)
and A112:
ex
z being
Element of
X st
(
x = {z} &
z in Y )
;
consider z being
Element of
X such that A113:
(
x = {z} &
z in Y )
by A112;
consider ze being
set such that A114:
(
z in ze &
ze in rng s )
by A113, TARSKI:def 4;
consider u being
set such that A115:
(
u in dom s &
ze = s . u )
by A114, FUNCT_1:def 5;
reconsider u =
u as
Element of
Fs' by A77, A115, PARTFUN1:def 4;
A116:
t in { (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u ) }
by A111, A113, A114, A115;
{ (f . (uparrow x1)) where x1 is Element of (BoolePoset X) : ex z being Element of X st
( x1 = {z} & z in s . u ) } in { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) }
by A76, A77, A115;
hence
t in union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) }
by A116, TARSKI:def 4;
:: thesis: verum end; then
union { { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } where u is Element of Fs' : u in dom (FFD . s) } = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
by TARSKI:2;
hence
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 mFs }
by A75, A87, A103, YELLOW_2:def 6;
:: thesis: verum
end; 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 mFs }
;
:: thesis: r in rng (Infs )then consider Y being
Subset of
X such that A117:
r = "/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
and A118:
Y in mFs
;
set s =
Fs' --> Y;
set s' =
Fs' --> Y;
A119:
dom (doms FD) =
dom FD
by FUNCT_6:89
.=
dom (Fs' --> Y)
by A10, FUNCOP_1:19
;
now let w be
set ;
:: thesis: ( w in dom (doms FD) implies (Fs' --> Y) . w in (doms FD) . w )assume
w in dom (doms FD)
;
:: thesis: (Fs' --> Y) . w in (doms FD) . wthen A120:
w in Fs'
by A119;
then A121:
(doms FD) . w = dom (FD . w)
by A10, FUNCT_6:31;
A122:
FD . w is
Function of
(K . w),
((Fs' --> the carrier of L) . w)
by A120, PBOOLE:def 18;
(Fs' --> the carrier of L) . w = the
carrier of
L
by A120, FUNCOP_1:13;
then A123:
dom (FD . w) =
K . w
by A122, FUNCT_2:def 1
.=
w
by A120, FUNCT_1:35
;
(Fs' --> Y) . w = Y
by A120, FUNCOP_1:13;
hence
(Fs' --> Y) . w in (doms FD) . w
by A118, A120, A121, A123, SETFAM_1:def 1;
:: thesis: verum end; then reconsider s =
Fs' --> Y as
Element of
pdFD by A119, CARD_3:18;
A124:
Inf = "/\" (rng (FFD . s)),
L
by YELLOW_2:def 6;
A125:
rng (FFD . s) = H2(
s)
by A64;
then A131:
{ ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ,L) where u is Element of Fs' : u in dom (FFD . s) } = {r}
by TARSKI:2;
"/\" {r},
L = r
by A117, YELLOW_0:39;
hence
r in rng (Infs )
by A124, A125, A131, WAYBEL_5:14;
:: thesis: verum end; hence
"/\" ((f -extension_to_hom ) .: Fs),
L = (f -extension_to_hom ) . ("/\" Fs,(InclPoset (Filt (BoolePoset X))))
by A32, A60, A61, A62, TARSKI:2;
:: thesis: verum end;