:: WAYBEL22 semantic presentation
begin
Lm1: for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L)
proof
let L be complete LATTICE; ::_thesis: for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L)
let X be set ; ::_thesis: ( X c= bool the carrier of L implies "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L) )
assume A1: X c= bool the carrier of L ; ::_thesis: "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L)
defpred S1[ Subset of L] means $1 in X;
set XX = { Z where Z is Subset of L : S1[Z] } ;
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__implies_x_in_X_)_&_(_x_in_X_implies_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__)_)
let x be set ; ::_thesis: ( ( x in { Z where Z is Subset of L : S1[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S1[Z] } ) )
hereby ::_thesis: ( x in X implies x in { Z where Z is Subset of L : S1[Z] } )
assume x in { Z where Z is Subset of L : S1[Z] } ; ::_thesis: x in X
then ex Z being Subset of L st
( x = Z & Z in X ) ;
hence x in X ; ::_thesis: verum
end;
assume A3: x in X ; ::_thesis: x in { Z where Z is Subset of L : S1[Z] }
then reconsider x9 = x as Subset of L by A1;
x9 in { Z where Z is Subset of L : S1[Z] } by A3;
hence x in { Z where Z is Subset of L : S1[Z] } ; ::_thesis: verum
end;
"/\" ( { ("/\" (Y,L)) where Y is Subset of L : S1[Y] } ,L) = "/\" ((union { Z where Z is Subset of L : S1[Z] } ),L) from YELLOW_3:sch_3();
hence "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L) by A2, TARSKI:1; ::_thesis: verum
end;
Lm2: for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)
proof
let L be complete LATTICE; ::_thesis: for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)
let X be set ; ::_thesis: ( X c= bool the carrier of L implies "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L) )
assume A1: X c= bool the carrier of L ; ::_thesis: "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)
defpred S1[ set ] means $1 in X;
set XX = { Z where Z is Subset of L : S1[Z] } ;
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__implies_x_in_X_)_&_(_x_in_X_implies_x_in__{__Z_where_Z_is_Subset_of_L_:_S1[Z]__}__)_)
let x be set ; ::_thesis: ( ( x in { Z where Z is Subset of L : S1[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S1[Z] } ) )
hereby ::_thesis: ( x in X implies x in { Z where Z is Subset of L : S1[Z] } )
assume x in { Z where Z is Subset of L : S1[Z] } ; ::_thesis: x in X
then ex Z being Subset of L st
( x = Z & Z in X ) ;
hence x in X ; ::_thesis: verum
end;
assume A3: x in X ; ::_thesis: x in { Z where Z is Subset of L : S1[Z] }
then reconsider x9 = x as Subset of L by A1;
x9 in { Z where Z is Subset of L : S1[Z] } by A3;
hence x in { Z where Z is Subset of L : S1[Z] } ; ::_thesis: verum
end;
"\/" ( { ("\/" (Y,L)) where Y is Subset of L : S1[Y] } ,L) = "\/" ((union { Z where Z is Subset of L : S1[Z] } ),L) from YELLOW_3:sch_5();
hence "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L) by A2, TARSKI:1; ::_thesis: verum
end;
theorem Th1: :: WAYBEL22:1
for L being upper-bounded Semilattice
for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
proof
let L be upper-bounded Semilattice; ::_thesis: for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
let F be non empty directed Subset of (InclPoset (Filt L)); ::_thesis: sup F = union F
Filt L = Ids (L opp) by WAYBEL16:7;
hence sup F = union F by WAYBEL13:9; ::_thesis: verum
end;
theorem Th2: :: WAYBEL22:2
for L, S, T being non empty complete Poset
for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
proof
let L, S, T be non empty complete Poset; ::_thesis: for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let f be CLHomomorphism of L,S; ::_thesis: for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let g be CLHomomorphism of S,T; ::_thesis: g * f is CLHomomorphism of L,T
( f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL16:def_1;
then A1: g * f is directed-sups-preserving by WAYBEL20:28;
( f is infs-preserving & g is infs-preserving ) by WAYBEL16:def_1;
then g * f is infs-preserving by WAYBEL20:25;
hence g * f is CLHomomorphism of L,T by A1, WAYBEL16:def_1; ::_thesis: verum
end;
theorem Th3: :: WAYBEL22:3
for L being non empty RelStr holds id L is infs-preserving
proof
let L be non empty RelStr ; ::_thesis: id L is infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: id L preserves_inf_of X
set f = id L;
assume ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (id L) .: X,L & "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) )
hence ex_inf_of (id L) .: X,L by FUNCT_1:92; ::_thesis: "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L))
(id L) .: X = X by FUNCT_1:92;
hence "/\" (((id L) .: X),L) = (id L) . ("/\" (X,L)) by FUNCT_1:18; ::_thesis: verum
end;
theorem Th4: :: WAYBEL22:4
for L being non empty RelStr holds id L is directed-sups-preserving
proof
let L be non empty RelStr ; ::_thesis: id L is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or id L preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: id L preserves_sup_of X
set f = id L;
assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (id L) .: X,L & "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) )
hence ex_sup_of (id L) .: X,L by FUNCT_1:92; ::_thesis: "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L))
(id L) .: X = X by FUNCT_1:92;
hence "\/" (((id L) .: X),L) = (id L) . ("\/" (X,L)) by FUNCT_1:18; ::_thesis: verum
end;
theorem Th5: :: WAYBEL22:5
for L being non empty complete Poset holds id L is CLHomomorphism of L,L
proof
let L be non empty complete Poset; ::_thesis: id L is CLHomomorphism of L,L
( id L is directed-sups-preserving & id L is infs-preserving ) by Th3, Th4;
hence id L is CLHomomorphism of L,L by WAYBEL16:def_1; ::_thesis: verum
end;
theorem Th6: :: WAYBEL22:6
for L being non empty upper-bounded with_infima Poset holds InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
proof
let L be non empty upper-bounded with_infima Poset; ::_thesis: InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
set cL = the carrier of L;
set BP = BoolePoset the carrier of L;
set cBP = the carrier of (BoolePoset the carrier of L);
set rBP = the InternalRel of (BoolePoset the carrier of L);
set IP = InclPoset (Filt L);
set cIP = the carrier of (InclPoset (Filt L));
set rIP = the InternalRel of (InclPoset (Filt L));
A1: InclPoset (bool the carrier of L) = RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) by YELLOW_1:def_1;
A2: InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def_1;
A3: BoolePoset the carrier of L = InclPoset (bool the carrier of L) by YELLOW_1:4;
A4: the carrier of (InclPoset (Filt L)) c= the carrier of (BoolePoset the carrier of L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (InclPoset (Filt L)) or x in the carrier of (BoolePoset the carrier of L) )
assume x in the carrier of (InclPoset (Filt L)) ; ::_thesis: x in the carrier of (BoolePoset the carrier of L)
then ex X being Filter of L st x = X by A2;
hence x in the carrier of (BoolePoset the carrier of L) by A3, A1; ::_thesis: verum
end;
A5: field the InternalRel of (InclPoset (Filt L)) = Filt L by A2, WELLORD2:def_1;
the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in the InternalRel of (InclPoset (Filt L)) or p in the InternalRel of (BoolePoset the carrier of L) )
assume A6: p in the InternalRel of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (BoolePoset the carrier of L)
then consider x, y being set such that
A7: p = [x,y] by RELAT_1:def_1;
A8: y in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider Y being Filter of L such that
A9: y = Y by A5;
A10: x in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider X being Filter of L such that
A11: x = X by A5;
X c= Y by A2, A5, A6, A7, A10, A8, A11, A9, WELLORD2:def_1;
hence p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A7, A11, A9, WELLORD2:def_1; ::_thesis: verum
end;
then reconsider IP = InclPoset (Filt L) as SubRelStr of BoolePoset the carrier of L by A4, YELLOW_0:def_13;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_the_InternalRel_of_(InclPoset_(Filt_L))_implies_p_in_the_InternalRel_of_(BoolePoset_the_carrier_of_L)_|_2_the_carrier_of_(InclPoset_(Filt_L))_)_&_(_p_in_the_InternalRel_of_(BoolePoset_the_carrier_of_L)_|_2_the_carrier_of_(InclPoset_(Filt_L))_implies_p_in_the_InternalRel_of_(InclPoset_(Filt_L))_)_)
let p be set ; ::_thesis: ( ( p in the InternalRel of (InclPoset (Filt L)) implies p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ) & ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) ) )
A12: the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) = the InternalRel of (BoolePoset the carrier of L) /\ [: the carrier of (InclPoset (Filt L)), the carrier of (InclPoset (Filt L)):] by WELLORD1:def_6;
hereby ::_thesis: ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) )
assume A13: p in the InternalRel of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L))
then consider x, y being set such that
A14: p = [x,y] by RELAT_1:def_1;
A15: y in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider Y being Filter of L such that
A16: y = Y by A5;
A17: x in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider X being Filter of L such that
A18: x = X by A5;
X c= Y by A2, A5, A13, A14, A17, A15, A18, A16, WELLORD2:def_1;
then p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A14, A18, A16, WELLORD2:def_1;
hence p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) by A12, A13, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A19: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ; ::_thesis: p in the InternalRel of (InclPoset (Filt L))
then A20: p in the InternalRel of (BoolePoset the carrier of L) by A12, XBOOLE_0:def_4;
p in [: the carrier of (InclPoset (Filt L)), the carrier of (InclPoset (Filt L)):] by A12, A19, XBOOLE_0:def_4;
then consider x, y being set such that
A21: ( x in the carrier of (InclPoset (Filt L)) & y in the carrier of (InclPoset (Filt L)) ) and
A22: p = [x,y] by ZFMISC_1:def_2;
( ex X being Filter of L st x = X & ex Y being Filter of L st y = Y ) by A2, A21;
then x c= y by A3, A1, A20, A22, WELLORD2:def_1;
hence p in the InternalRel of (InclPoset (Filt L)) by A2, A21, A22, WELLORD2:def_1; ::_thesis: verum
end;
then the InternalRel of (InclPoset (Filt L)) = the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) by TARSKI:1;
then reconsider IP = IP as full SubRelStr of BoolePoset the carrier of L by YELLOW_0:def_14;
A23: Filt L c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Filt L or x in bool the carrier of L )
assume x in Filt L ; ::_thesis: x in bool the carrier of L
then ex X being Filter of L st x = X ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
A24: IP is directed-sups-inheriting
proof
let X be directed Subset of IP; :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X, BoolePoset the carrier of L or "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP )
assume that
A25: X <> {} and
ex_sup_of X, BoolePoset the carrier of L ; ::_thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP
consider Y being set such that
A26: Y in X by A25, XBOOLE_0:def_1;
reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
A27: for P, R being Subset of L st P in F & R in F holds
ex Z being Subset of L st
( Z in F & P \/ R c= Z )
proof
let P, R be Subset of L; ::_thesis: ( P in F & R in F implies ex Z being Subset of L st
( Z in F & P \/ R c= Z ) )
assume A28: ( P in F & R in F ) ; ::_thesis: ex Z being Subset of L st
( Z in F & P \/ R c= Z )
then reconsider P9 = P, R9 = R as Element of IP ;
consider Z being Element of IP such that
A29: Z in X and
A30: ( P9 <= Z & R9 <= Z ) by A28, WAYBEL_0:def_1;
Z in the carrier of IP by A29;
then consider Z9 being Filter of L such that
A31: Z9 = Z by A2;
take Z9 ; ::_thesis: ( Z9 in F & P \/ R c= Z9 )
thus Z9 in F by A29, A31; ::_thesis: P \/ R c= Z9
( P9 c= Z & R9 c= Z ) by A30, YELLOW_1:3;
hence P \/ R c= Z9 by A31, XBOOLE_1:8; ::_thesis: verum
end;
reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
set sX = "\/" (X,(BoolePoset the carrier of L));
A32: sup X9 = union X by YELLOW_1:21;
reconsider sX = "\/" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
A33: for X being Subset of L st X in F holds
( X is upper & X is filtered )
proof
let X be Subset of L; ::_thesis: ( X in F implies ( X is upper & X is filtered ) )
assume X in F ; ::_thesis: ( X is upper & X is filtered )
then X in Filt L by A2;
then ex Y being Filter of L st X = Y ;
hence ( X is upper & X is filtered ) ; ::_thesis: verum
end;
then for X being Subset of L st X in F holds
X is upper ;
then A34: sX is upper by A32, WAYBEL_0:28;
for X being Subset of L st X in F holds
X is filtered by A33;
then A35: sX is filtered by A32, A27, WAYBEL_0:47;
Y in Filt L by A2, A26;
then ex Z being Filter of L st Y = Z ;
then Top L in Y by WAYBEL_4:22;
then not sX is empty by A32, A26, TARSKI:def_4;
hence "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A34, A35; ::_thesis: verum
end;
IP is infs-inheriting
proof
let X be Subset of IP; :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X, BoolePoset the carrier of L or "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP )
assume ex_inf_of X, BoolePoset the carrier of L ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
set sX = "/\" (X,(BoolePoset the carrier of L));
percases ( X is empty or not X is empty ) ;
supposeA36: X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
A37: [#] L = the carrier of L ;
"/\" (X,(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by A36
.= the carrier of L by YELLOW_1:19 ;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A37; ::_thesis: verum
end;
supposeA38: not X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP
reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
reconsider sX = "/\" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
A39: inf X9 = meet X by A38, YELLOW_1:20;
A40: for X being Subset of L st X in F holds
( X is upper & X is filtered )
proof
let X be Subset of L; ::_thesis: ( X in F implies ( X is upper & X is filtered ) )
assume X in F ; ::_thesis: ( X is upper & X is filtered )
then X in Filt L by A2;
then ex Y being Filter of L st X = Y ;
hence ( X is upper & X is filtered ) ; ::_thesis: verum
end;
then A41: sX is filtered by A39, YELLOW_2:39;
for X being Subset of L st X in F holds
X is upper by A40;
then A42: sX is upper by A39, YELLOW_2:37;
for Y being set st Y in X holds
Top L in Y
proof
let Y be set ; ::_thesis: ( Y in X implies Top L in Y )
assume Y in X ; ::_thesis: Top L in Y
then Y in Filt L by A2;
then ex Z being Filter of L st Y = Z ;
hence Top L in Y by WAYBEL_4:22; ::_thesis: verum
end;
then not sX is empty by A38, A39, SETFAM_1:def_1;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A42, A41; ::_thesis: verum
end;
end;
end;
hence InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L by A24; ::_thesis: verum
end;
registration
let L be non empty upper-bounded with_infima Poset;
cluster InclPoset (Filt L) -> continuous ;
coherence
InclPoset (Filt L) is continuous
proof
InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L by Th6;
hence InclPoset (Filt L) is continuous by WAYBEL_5:28; ::_thesis: verum
end;
end;
registration
let L be non empty upper-bounded Poset;
cluster -> non empty for Element of the carrier of (InclPoset (Filt L));
coherence
for b1 being Element of (InclPoset (Filt L)) holds not b1 is empty
proof
let x be Element of (InclPoset (Filt L)); ::_thesis: not x is empty
InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def_1;
then x in Filt L ;
then ex X being Filter of L st x = X ;
hence not x is empty ; ::_thesis: verum
end;
end;
begin
definition
let S be non empty complete continuous Poset;
let A be set ;
predA is_FreeGen_set_of S means :Def1: :: WAYBEL22:def 1
for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) );
end;
:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def_1_:_
for S being non empty complete continuous Poset
for A being set holds
( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );
theorem Th7: :: WAYBEL22:7
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
A is Subset of S
proof
set T = the non empty complete continuous Poset;
let S be non empty complete continuous Poset; ::_thesis: for A being set st A is_FreeGen_set_of S holds
A is Subset of S
let A be set ; ::_thesis: ( A is_FreeGen_set_of S implies A is Subset of S )
assume A1: A is_FreeGen_set_of S ; ::_thesis: A is Subset of S
set f = the Function of A, the carrier of the non empty complete continuous Poset;
consider h being CLHomomorphism of S, the non empty complete continuous Poset such that
A2: h | A = the Function of A, the carrier of the non empty complete continuous Poset and
for h9 being CLHomomorphism of S, the non empty complete continuous Poset st h9 | A = the Function of A, the carrier of the non empty complete continuous Poset holds
h9 = h by A1, Def1;
dom (h | A) = (dom h) /\ A by RELAT_1:61;
hence A is Subset of S by A2, FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th8: :: WAYBEL22:8
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
proof
let S be non empty complete continuous Poset; ::_thesis: for A being set st A is_FreeGen_set_of S holds
for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
let A be set ; ::_thesis: ( A is_FreeGen_set_of S implies for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S )
assume A1: A is_FreeGen_set_of S ; ::_thesis: for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
set L = S;
A2: A is Subset of S by A1, Th7;
then A3: (id S) | A = id A by FUNCT_3:1;
( dom (id A) = A & rng (id A) = A ) ;
then reconsider f = id A as Function of A, the carrier of S by A2, RELSET_1:4;
consider h being CLHomomorphism of S,S such that
h | A = f and
A4: for h9 being CLHomomorphism of S,S st h9 | A = f holds
h9 = h by A1, Def1;
A5: id S is CLHomomorphism of S,S by Th5;
let h9 be CLHomomorphism of S,S; ::_thesis: ( h9 | A = id A implies h9 = id S )
assume h9 | A = id A ; ::_thesis: h9 = id S
hence h9 = h by A4
.= id S by A4, A5, A3 ;
::_thesis: verum
end;
begin
definition
let X be set ;
func FixedUltraFilters X -> Subset-Family of (BoolePoset X) equals :: WAYBEL22:def 2
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;
coherence
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } is Subset-Family of (BoolePoset X)
proof
set FUF = { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } ;
{ (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } c= bool the carrier of (BoolePoset X)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } or z in bool the carrier of (BoolePoset X) )
assume z in { (uparrow x) where x is Element of (BoolePoset X) : ex y being Element of X st x = {y} } ; ::_thesis: z in bool the carrier of (BoolePoset X)
then ex x being Element of (BoolePoset X) st
( z = uparrow x & ex y being Element of X st x = {y} ) ;
hence z in bool the carrier of (BoolePoset X) ; ::_thesis: verum
end;
hence { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } is Subset-Family of (BoolePoset X) ; ::_thesis: verum
end;
end;
:: deftheorem defines FixedUltraFilters WAYBEL22:def_2_:_
for X being set holds FixedUltraFilters X = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;
theorem Th9: :: WAYBEL22:9
for X being set holds FixedUltraFilters X c= Filt (BoolePoset X)
proof
let X be set ; ::_thesis: FixedUltraFilters X c= Filt (BoolePoset X)
let F be set ; :: according to TARSKI:def_3 ::_thesis: ( not F in FixedUltraFilters X or F in Filt (BoolePoset X) )
assume F in FixedUltraFilters X ; ::_thesis: F in Filt (BoolePoset X)
then ex x being Element of (BoolePoset X) st
( F = uparrow x & ex y being Element of X st x = {y} ) ;
hence F in Filt (BoolePoset X) ; ::_thesis: verum
end;
theorem Th10: :: WAYBEL22:10
for X being set holds card (FixedUltraFilters X) = card X
proof
let X be set ; ::_thesis: card (FixedUltraFilters X) = card X
set FUF = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;
A1: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
A2: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1;
then A3: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;
X, { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } are_equipotent
proof
defpred S1[ set , set ] means ex y being Element of X ex x being Element of (BoolePoset X) st
( x = {y} & $1 = y & $2 = uparrow x );
A4: for x being set st x in X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] )
assume A5: x in X ; ::_thesis: ex y being set st S1[x,y]
then reconsider x9 = x as Element of X ;
reconsider bx = {x} as Element of (BoolePoset X) by A1, A2, A5, ZFMISC_1:31;
take uparrow bx ; ::_thesis: S1[x, uparrow bx]
take x9 ; ::_thesis: ex x being Element of (BoolePoset X) st
( x = {x9} & x = x9 & uparrow bx = uparrow x )
take bx ; ::_thesis: ( bx = {x9} & x = x9 & uparrow bx = uparrow bx )
thus ( bx = {x9} & x = x9 & uparrow bx = uparrow bx ) ; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = X & ( for x being set st x in X holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A4);
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )
thus f is one-to-one ::_thesis: ( dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A7: x1 in dom f and
A8: x2 in dom f and
A9: f . x1 = f . x2 ; ::_thesis: x1 = x2
consider x29 being Element of X, bx2 being Element of (BoolePoset X) such that
A10: ( bx2 = {x29} & x2 = x29 ) and
A11: f . x2 = uparrow bx2 by A6, A8;
consider x19 being Element of X, bx1 being Element of (BoolePoset X) such that
A12: ( bx1 = {x19} & x1 = x19 ) and
A13: f . x1 = uparrow bx1 by A6, A7;
bx1 = bx2 by A9, A13, A11, WAYBEL_0:20;
hence x1 = x2 by A12, A10, ZFMISC_1:3; ::_thesis: verum
end;
thus dom f = X by A6; ::_thesis: rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_rng_f_implies_z_in__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_x_=_{z}__}__)_&_(_z_in__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_x_=_{z}__}__implies_z_in_rng_f_)_)
let z be set ; ::_thesis: ( ( z in rng f implies z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ) & ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f ) )
hereby ::_thesis: ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f )
assume z in rng f ; ::_thesis: z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }
then consider x1 being set such that
A14: x1 in dom f and
A15: z = f . x1 by FUNCT_1:def_3;
ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st
( bx1 = {x19} & x1 = x19 & f . x1 = uparrow bx1 ) by A6, A14;
hence z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } by A15; ::_thesis: verum
end;
assume z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ; ::_thesis: z in rng f
then consider bx being Element of (BoolePoset X) such that
A16: z = uparrow bx and
A17: ex y being Element of X st bx = {y} ;
consider y being Element of X such that
A18: bx = {y} by A17;
A19: y in X by A3, A18, ZFMISC_1:31;
then ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st
( bx1 = {x19} & y = x19 & f . y = uparrow bx1 ) by A6;
hence z in rng f by A6, A16, A18, A19, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } by TARSKI:1; ::_thesis: verum
end;
hence card (FixedUltraFilters X) = card X by CARD_1:5; ::_thesis: verum
end;
theorem Th11: :: WAYBEL22:11
for X being set
for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
proof
let X be set ; ::_thesis: for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
let F be Filter of (BoolePoset X); ::_thesis: F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
set Xs = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ;
set RS = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
F in Filt (BoolePoset X) ;
then reconsider F9 = F as Element of (InclPoset (Filt (BoolePoset X))) by A1;
A2: { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } or p in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ; ::_thesis: p in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex YY being Subset of X st
( p = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) & YY in F ) ;
hence p in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: verum
end;
A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_not__{__("/\"_(_{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,(InclPoset_(Filt_(BoolePoset_X)))))_where_Y_is_Subset_of_X_:_Y_in_F__}__is_empty
consider YY being set such that
A4: YY in F by XBOOLE_0:def_1;
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A3, A4;
hence not { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } is empty ; ::_thesis: verum
end;
then reconsider Xs9 = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A2;
A5: ex_sup_of Xs9, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
F c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in F or p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) )
assume A6: p in F ; ::_thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
then reconsider Y = p as Element of F ;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
A7: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A3;
percases ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty or not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ) ;
supposeA8: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; ::_thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
A9: p in the carrier of (BoolePoset X) by A6;
Xs9 is_<=_than "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A5, YELLOW_0:def_9;
then A10: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) <= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A7, LATTICE3:def_9;
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A8
.= bool X by WAYBEL16:15 ;
then bool X c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A10, YELLOW_1:3;
hence p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A3, A9; ::_thesis: verum
end;
supposeA11: not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; ::_thesis: p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; ::_thesis: verum
end;
then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A11;
for yy being set st yy in Xsi holds
Y in yy
proof
reconsider Y9 = Y as Element of (BoolePoset X) ;
let yy be set ; ::_thesis: ( yy in Xsi implies Y in yy )
assume yy in Xsi ; ::_thesis: Y in yy
then consider r being Element of (BoolePoset X) such that
A12: yy = uparrow r and
A13: ex z being Element of X st
( r = {z} & z in Y ) ;
r c= Y by A13, ZFMISC_1:31;
then r <= Y9 by YELLOW_1:2;
hence Y in yy by A12, WAYBEL_0:18; ::_thesis: verum
end;
then ( "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi & Y in meet Xsi ) by SETFAM_1:def_1, WAYBEL16:10;
then A14: p in union { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } by A7, TARSKI:def_4;
union Xs9 c= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by WAYBEL16:17, YELLOW_0:17;
hence p in "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A14; ::_thesis: verum
end;
end;
end;
then A15: F9 <= "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3;
{ ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } is_<=_than F9
proof
let b be Element of (InclPoset (Filt (BoolePoset X))); :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } or b <= F9 )
assume b in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ; ::_thesis: b <= F9
then consider Y being Subset of X such that
A16: b = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) and
A17: Y in F ;
reconsider Y9 = Y as Element of F by A17;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
percases ( Y is empty or not Y is empty ) ;
supposeA18: Y is empty ; ::_thesis: b <= F9
now__::_thesis:__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__is_empty
assume not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; ::_thesis: contradiction
then consider p being set such that
A19: p in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by XBOOLE_0:def_1;
ex x being Element of (BoolePoset X) st
( p = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A19;
hence contradiction by A18; ::_thesis: verum
end;
then A20: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X)))
.= bool X by WAYBEL16:15 ;
Bottom (BoolePoset X) = {} by YELLOW_1:18;
then uparrow (Bottom (BoolePoset X)) c= F by A17, A18, WAYBEL11:42;
then bool X c= F by A3, WAYBEL14:10;
hence b <= F9 by A3, A16, A20, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA21: not Y is empty ; ::_thesis: b <= F9
A22: now__::_thesis:_not__{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__is_empty
consider z being set such that
A23: z in Y by A21, XBOOLE_0:def_1;
reconsider z = z as Element of X by A23;
reconsider x = {z} as Element of (BoolePoset X) by A3, A23, ZFMISC_1:31;
uparrow x in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A23;
hence not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is empty ; ::_thesis: verum
end;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A1; ::_thesis: verum
end;
then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A22;
A24: "/\" (Xsi,(InclPoset (Filt (BoolePoset X)))) = meet Xsi by WAYBEL16:10;
b c= F9
proof
let yy be set ; :: according to TARSKI:def_3 ::_thesis: ( not yy in b or yy in F9 )
b in Filt (BoolePoset X) by A1;
then consider bf being Filter of (BoolePoset X) such that
A25: b = bf ;
assume A26: yy in b ; ::_thesis: yy in F9
then reconsider yy9 = yy as Element of bf by A25;
reconsider yy9 = yy9 as Element of (BoolePoset X) ;
Y c= yy9
proof
let zz be set ; :: according to TARSKI:def_3 ::_thesis: ( not zz in Y or zz in yy9 )
assume A27: zz in Y ; ::_thesis: zz in yy9
then reconsider z = zz as Element of X ;
reconsider xz = {z} as Element of (BoolePoset X) by A3, A27, ZFMISC_1:31;
uparrow xz in Xsi by A27;
then yy in uparrow xz by A16, A24, A26, SETFAM_1:def_1;
then xz <= yy9 by WAYBEL_0:18;
then {z} c= yy by YELLOW_1:2;
hence zz in yy9 by ZFMISC_1:31; ::_thesis: verum
end;
then Y9 <= yy9 by YELLOW_1:2;
then ( uparrow Y9 c= F9 & yy in uparrow Y9 ) by WAYBEL11:42, WAYBEL_0:18;
hence yy in F9 ; ::_thesis: verum
end;
hence b <= F9 by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
then "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) <= F9 by A5, YELLOW_0:def_9;
hence F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X)))) by A15, YELLOW_0:def_3; ::_thesis: verum
end;
definition
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
funcf -extension_to_hom -> Function of (InclPoset (Filt (BoolePoset X))),L means :Def3: :: WAYBEL22:def 3
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L);
existence
ex b1 being Function of (InclPoset (Filt (BoolePoset X))),L st
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L)
proof
set IP = InclPoset (Filt (BoolePoset X));
deffunc H1( Element of (InclPoset (Filt (BoolePoset X)))) -> Element of the carrier of L = "\/" ( { ("/\" ( { (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 $1 } ,L);
consider F being Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L such that
A1: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = H1(Fi) from FUNCT_2:sch_4();
reconsider F = F as Function of (InclPoset (Filt (BoolePoset X))),L ;
take F ; ::_thesis: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L)
thus for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds F . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b2 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) ) holds
b1 = b2
proof
set IP = InclPoset (Filt (BoolePoset X));
let it1, it2 be Function of (InclPoset (Filt (BoolePoset X))),L; ::_thesis: ( ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) ) implies it1 = it2 )
assume that
A2: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) and
A3: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) ; ::_thesis: it1 = it2
reconsider it29 = it2 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
reconsider it19 = it1 as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
now__::_thesis:_for_Fi_being_Element_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_it19_._Fi_=_it29_._Fi
let Fi be Element of (InclPoset (Filt (BoolePoset X))); ::_thesis: it19 . Fi = it29 . Fi
thus it19 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) by A2
.= it29 . Fi by A3 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def_3_:_
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for b4 being Function of (InclPoset (Filt (BoolePoset X))),L holds
( b4 = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b4 . Fi = "\/" ( { ("/\" ( { (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 Fi } ,L) );
theorem :: WAYBEL22:12
for X being 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
proof
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 set ; :: 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
end;
theorem Th13: :: WAYBEL22:13
for X being 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) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
proof
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) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
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) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
set IP = InclPoset (Filt (BoolePoset X));
set F = f -extension_to_hom ;
reconsider T = Top (InclPoset (Filt (BoolePoset X))) as Element of (InclPoset (Filt (BoolePoset X))) ;
reconsider E = {} as Subset of X by XBOOLE_1:2;
set 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 T } ;
A1: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {}
proof
assume not { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } = {} ; ::_thesis: contradiction
then consider r being set such that
A2: r in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } by XBOOLE_0:def_1;
ex x being Element of (BoolePoset X) st
( r = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in E ) ) by A2;
hence contradiction ; ::_thesis: verum
end;
A3: (f -extension_to_hom) . T = "\/" ( { ("/\" ( { (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 T } ,L) by Def3;
T = bool X by WAYBEL16:15;
then A4: "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in E ) } ,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 T } ;
{ ("/\" ( { (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 T } is_<=_than "\/" ( { ("/\" ( { (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 T } ,L) by YELLOW_0:32;
then Top L <= "\/" ( { ("/\" ( { (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 T } ,L) by A4, A1, LATTICE3:def_9;
hence (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L by A3, WAYBEL15:3; ::_thesis: verum
end;
registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom -> directed-sups-preserving ;
coherence
f -extension_to_hom is directed-sups-preserving
proof
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_set_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 set ; ::_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:1;
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 set ; :: 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 )
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 } ;
r c= the carrier of L
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in r or s in the carrier of L )
assume s in r ; ::_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_set_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 set ; ::_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 set 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 set ; :: 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:1; ::_thesis: verum
end;
end;
registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom -> infs-preserving ;
coherence
f -extension_to_hom is infs-preserving
proof
set FUF = FixedUltraFilters X;
set cL = the carrier of L;
set F = f -extension_to_hom ;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
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)))))
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;
percases ( Fs is empty or not Fs is empty ) ;
suppose Fs is empty ; ::_thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))
then ( "/\" (((f -extension_to_hom) .: Fs),L) = Top L & "/\" (Fs,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) ) ;
hence "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by Th13; ::_thesis: verum
end;
suppose not Fs is empty ; ::_thesis: "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X)))))
then reconsider Fs9 = Fs as non empty Subset of (InclPoset (Filt (BoolePoset X))) ;
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);
deffunc H1( Element of Fs9) -> 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 } ;
not {} in Fs9 ;
then Fs9 is with_non-empty_elements by SETFAM_1:def_8;
then reconsider K = id Fs9 as V8() ManySortedSet of Fs9 ;
A5: for i being set st i in Fs9 holds
for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] )
proof
let i be set ; ::_thesis: ( i in Fs9 implies for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> the carrier of L) . i & S1[y,s,i] ) )
assume A6: i in Fs9 ; ::_thesis: for s being set st s in K . i holds
ex y being set st
( y in (Fs9 --> 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 (Fs9 --> the carrier of L) . i & S1[y,s,i] ) )
assume s in K . i ; ::_thesis: ex y being set st
( y in (Fs9 --> 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 (Fs9 --> the carrier of L) . i & S1[y,s,i] )
y in the carrier of L ;
hence y in (Fs9 --> the carrier of L) . i by A6, FUNCOP_1:7; ::_thesis: S1[y,s,i]
thus S1[y,s,i] ; ::_thesis: verum
end;
consider FD being ManySortedFunction of K,Fs9 --> the carrier of L such that
A7: for i being set st i in Fs9 holds
ex g being Function of (K . i),((Fs9 --> 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(A5);
defpred S2[ Element of Fs9] means rng (FD . X) = H1(X);
A8: for s being Element of Fs9 holds S2[s]
proof
let s be Element of Fs9; ::_thesis: S2[s]
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_rng_(FD_._s)_implies_t_in_H1(s)_)_&_(_t_in_H1(s)_implies_t_in_rng_(FD_._s)_)_)
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) ) )
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A9: g = FD . s and
A10: for u being set st u in K . s holds
S1[g . u,u,s] by A7;
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
A11: u in dom (FD . s) and
A12: t = (FD . s) . u by FUNCT_1:def_3;
consider g being Function of (K . s),((Fs9 --> the carrier of L) . s) such that
A13: g = FD . s and
A14: for u being set st u in K . s holds
S1[g . u,u,s] by A7;
A15: dom (FD . s) = K . s by FUNCT_2:def_1;
A16: 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 A11, A14;
s in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then ( K . s = s & ex FF being Filter of (BoolePoset X) st s = FF ) by A1, FUNCT_1:18;
then reconsider u = u as Subset of X by A3, A11, A15, YELLOW_1:4;
u in s by A11, A15, FUNCT_1:18;
hence t in H1(s) by A12, A13, A16; ::_thesis: verum
end;
assume t in H1(s) ; ::_thesis: t in rng (FD . s)
then consider Y being Subset of X such that
A17: 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
A18: Y in s ;
dom (FD . s) = K . s by FUNCT_2:def_1;
then A19: Y in dom (FD . s) by A18, FUNCT_1:18;
K . s = s by FUNCT_1:18;
then 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 A18, A10;
hence t in rng (FD . s) by A17, A19, A9, FUNCT_1:def_3; ::_thesis: verum
end;
hence S2[s] by TARSKI:1; ::_thesis: verum
end;
meet Fs9 is Filter of (BoolePoset X) by WAYBEL16:9;
then meet Fs9 in Filt (BoolePoset X) ;
then reconsider mFs = meet Fs9 as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A1;
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 } ;
A20: dom FD = Fs9 by PARTFUN1:def_2;
reconsider FD = FD as DoubleIndexedSet of K,L ;
now__::_thesis:_for_r_being_set_holds_
(_(_r_in_(f_-extension_to_hom)_.:_Fs_implies_r_in_rng_(Sups_)_)_&_(_r_in_rng_(Sups_)_implies_r_in_(f_-extension_to_hom)_.:_Fs_)_)
let r be set ; ::_thesis: ( ( r in (f -extension_to_hom) .: Fs implies r in rng (Sups ) ) & ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs ) )
hereby ::_thesis: ( r in rng (Sups ) implies r in (f -extension_to_hom) .: Fs )
assume r in (f -extension_to_hom) .: Fs ; ::_thesis: r in rng (Sups )
then consider s being set such that
A21: s in the carrier of (InclPoset (Filt (BoolePoset X))) and
A22: s in Fs and
A23: (f -extension_to_hom) . s = r by FUNCT_2:64;
reconsider s9 = s as Element of the carrier of (InclPoset (Filt (BoolePoset X))) by A21;
reconsider s = s as Element of Fs9 by A22;
A24: S2[s] by A8;
(f -extension_to_hom) . s9 = "\/" ( { ("/\" ( { (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 s9 } ,L) by Def3;
then r = Sup by A23, A24, YELLOW_2:def_5;
hence r in rng (Sups ) by WAYBEL_5:14; ::_thesis: verum
end;
assume r in rng (Sups ) ; ::_thesis: r in (f -extension_to_hom) .: Fs
then consider s being Element of Fs9 such that
A25: r = Sup by WAYBEL_5:14;
S2[s] by A8;
then (f -extension_to_hom) . s = "\/" ((rng (FD . s)),L) by Def3
.= Sup by YELLOW_2:def_5 ;
hence r in (f -extension_to_hom) .: Fs by A25, FUNCT_2:35; ::_thesis: verum
end;
then (f -extension_to_hom) .: Fs = rng (Sups ) by TARSKI:1;
then A26: inf ((f -extension_to_hom) .: Fs) = Inf by YELLOW_2:def_6;
A27: now__::_thesis:_for_r_being_set_holds_
(_(_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 ;
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 dFFD = (product (doms FD)) --> Fs9 as ManySortedSet of pdFD ;
reconsider FFD = Frege FD as DoubleIndexedSet of dFFD,L ;
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 Fs9 : u in dom (FFD . X) } ;
A28: dom FFD = pdFD by PARTFUN1:def_2;
A29: now__::_thesis:_for_s_being_Element_of_pdFD_holds_rng_(FFD_._s)_=_H2(s)
let s be Element of pdFD; ::_thesis: rng (FFD . s) = H2(s)
A30: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_rng_(FFD_._s)_implies_t_in_H2(s)_)_&_(_t_in_H2(s)_implies_t_in_rng_(FFD_._s)_)_)
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
A31: u in dom (FFD . s) and
A32: t = (FFD . s) . u by FUNCT_1:def_3;
A33: (FFD . s) . u = (FD . u) . (s . u) by A28, A30, A31, WAYBEL_5:9;
reconsider u = u as Element of Fs9 by A30, A31;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A34: g = FD . u and
A35: for v being set st v in K . u holds
S1[g . v,v,u] by A7;
dom (FD . u) = K . u by FUNCT_2:def_1;
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 A20, A28, A35, WAYBEL_5:9;
hence t in H2(s) by A31, A32, A33, A34; ::_thesis: verum
end;
assume t in H2(s) ; ::_thesis: t in rng (FFD . s)
then consider u being Element of Fs9 such that
A36: ( 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) & u in dom (FFD . s) ) ;
reconsider u = u as Element of Fs9 ;
consider g being Function of (K . u),((Fs9 --> the carrier of L) . u) such that
A37: g = FD . u and
A38: for v being set st v in K . u holds
S1[g . v,v,u] by A7;
dom (FD . u) = K . u by FUNCT_2:def_1;
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 A20, A28, A38, WAYBEL_5:9;
hence t in rng (FFD . s) by A28, A30, A36, A37, WAYBEL_5:9; ::_thesis: verum
end;
hence rng (FFD . s) = H2(s) by TARSKI:1; ::_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
A39: r = Inf by WAYBEL_5:14;
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 Fs9 : u in dom (FFD . s) } ;
A40: { { (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 Fs9 : u in dom (FFD . s) } c= bool the carrier of L
proof
let t be set ; :: 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 s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } or t in bool 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 s . u ) } where u is Element of Fs9 : u in dom (FFD . s) } ; ::_thesis: t in bool the carrier of L
then consider u being Element of Fs9 such that
A41: t = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } and
u in dom (FFD . s) ;
t c= the carrier of L
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in t or v in the carrier of L )
assume v in t ; ::_thesis: v in the carrier of L
then consider x being Element of (BoolePoset X) such that
A42: v = f . (uparrow x) and
A43: ex z being Element of X st
( x = {z} & z in s . u ) by A41;
uparrow x in FixedUltraFilters X by A43;
hence v in the carrier of L by A42, FUNCT_2:5; ::_thesis: verum
end;
hence t in bool the carrier of L ; ::_thesis: verum
end;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_H2(s)_implies_t_in__{__(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_Fs9_:_u_in_dom_(FFD_._s)__}___}__)_&_(_t_in__{__(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_Fs9_:_u_in_dom_(FFD_._s)__}___}__implies_t_in_H2(s)_)_)
let t be set ; ::_thesis: ( ( t in H2(s) implies t in { (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 Fs9 : u in dom (FFD . s) } } ) & ( t in { (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 Fs9 : u in dom (FFD . s) } } implies t in H2(s) ) )
hereby ::_thesis: ( t in { (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 Fs9 : u in dom (FFD . s) } } implies t in H2(s) )
assume t in H2(s) ; ::_thesis: t in { (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 Fs9 : u in dom (FFD . s) } }
then consider u being Element of Fs9 such that
A44: 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
A45: 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 s . u ) } c= the carrier of L
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } or v in the carrier of L )
assume v in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } ; ::_thesis: v in the carrier of L
then consider x being Element of (BoolePoset X) such that
A46: v = f . (uparrow x) and
A47: ex z being Element of X st
( x = {z} & z in s . u ) ;
uparrow x in FixedUltraFilters X by A47;
hence v in the carrier of L by A46, FUNCT_2:5; ::_thesis: verum
end;
then reconsider Y1 = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } as Subset of L ;
Y1 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 Fs9 : u in dom (FFD . s) } by A45;
hence t in { (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 Fs9 : u in dom (FFD . s) } } by A44; ::_thesis: verum
end;
assume t in { (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 Fs9 : u in dom (FFD . s) } } ; ::_thesis: t in H2(s)
then consider YY being Subset of L such that
A48: t = inf YY and
A49: 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 Fs9 : u in dom (FFD . s) } ;
ex u1 being Element of Fs9 st
( YY = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u1 ) } & u1 in dom (FFD . s) ) by A49;
hence t in H2(s) by A48; ::_thesis: verum
end;
then A50: 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 Fs9 : u in dom (FFD . s) } } by TARSKI:1;
A51: dom s = dom FD by A28, 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
A52: t in te and
A53: te in rng s by TARSKI:def_4;
consider u being set such that
A54: u in dom s and
A55: te = s . u by A53, FUNCT_1:def_3;
FD . u is Function of (K . u), the carrier of L by A51, A54, WAYBEL_5:6;
then dom (FD . u) = K . u by FUNCT_2:def_1
.= u by A51, A54, FUNCT_1:17 ;
then A56: te in u by A28, A51, A54, A55, WAYBEL_5:9;
u in the carrier of (InclPoset (Filt (BoolePoset X))) by A20, A51, A54;
then ex FF being Filter of (BoolePoset X) st u = FF by A1;
hence t in X by A4, A52, A56; ::_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 ) } ;
A57: dom FD = dom (FFD . s) by A28, WAYBEL_5:8;
now__::_thesis:_for_t_being_set_holds_
(_(_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_Fs9_:_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_Fs9_:_u_in_dom_(FFD_._s)__}__)_)
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 Fs9 : 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 Fs9 : u in dom (FFD . s) } ) )
hereby ::_thesis: ( 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 Fs9 : u in dom (FFD . s) } )
assume 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 Fs9 : u in dom (FFD . s) } ; ::_thesis: t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
then consider te being set such that
A58: t in te and
A59: te 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 Fs9 : u in dom (FFD . s) } by TARSKI:def_4;
consider u being Element of Fs9 such that
A60: te = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in s . u ) } and
A61: u in dom (FFD . s) by A59;
consider x being Element of (BoolePoset X) such that
A62: t = f . (uparrow x) and
A63: ex z being Element of X st
( x = {z} & z in s . u ) by A58, A60;
consider z being Element of X such that
A64: x = {z} and
A65: z in s . u by A63;
s . u in rng s by A57, A51, A61, FUNCT_1:def_3;
then z in Y by A65, TARSKI:def_4;
hence t in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A62, A64; ::_thesis: verum
end;
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 Fs9 : u in dom (FFD . s) }
then consider x being Element of (BoolePoset X) such that
A66: t = f . (uparrow x) and
A67: ex z being Element of X st
( x = {z} & z in Y ) ;
consider z being Element of X such that
A68: x = {z} and
A69: z in Y by A67;
consider ze being set such that
A70: z in ze and
A71: ze in rng s by A69, TARSKI:def_4;
consider u being set such that
A72: u in dom s and
A73: ze = s . u by A71, FUNCT_1:def_3;
reconsider u = u as Element of Fs9 by A51, A72;
A74: { (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 Fs9 : u in dom (FFD . s) } by A57, A51, A72;
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 A66, A68, A70, A73;
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 Fs9 : u in dom (FFD . s) } by A74, TARSKI:def_4; ::_thesis: verum
end;
then A75: 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 Fs9 : 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:1;
now__::_thesis:_for_Z_being_set_st_Z_in_Fs9_holds_
Y_in_Z
reconsider Y9 = Y as Element of (BoolePoset X) by A3, YELLOW_1:4;
let Z be set ; ::_thesis: ( Z in Fs9 implies Y in Z )
assume A76: Z in Fs9 ; ::_thesis: Y in Z
then FD . Z is Function of (K . Z), the carrier of L by WAYBEL_5:6;
then A77: dom (FD . Z) = K . Z by FUNCT_2:def_1
.= Z by A76, FUNCT_1:17 ;
s . Z in rng s by A20, A51, A76, FUNCT_1:def_3;
then A78: s . Z c= Y by ZFMISC_1:74;
then reconsider sZ = s . Z as Element of (BoolePoset X) by A2, A3, XBOOLE_1:1;
A79: sZ <= Y9 by A78, YELLOW_1:2;
Z in the carrier of (InclPoset (Filt (BoolePoset X))) by A76;
then A80: ex FF being Filter of (BoolePoset X) st Z = FF by A1;
s . Z in dom (FD . Z) by A20, A28, A76, WAYBEL_5:9;
hence Y in Z by A80, A77, A79, WAYBEL_0:def_20; ::_thesis: verum
end;
then Y in mFs by SETFAM_1:def_1;
then A81: "/\" ( { (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 } ;
"/\" ((rng (FFD . s)),L) = "/\" (H2(s),L) by A29
.= "/\" ((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 Fs9 : u in dom (FFD . s) } ),L) by A40, A50, Lm1 ;
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 A39, A81, A75, 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
A82: 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
A83: Y in mFs ;
A84: "/\" ({r},L) = r by A82, YELLOW_0:39;
set s = Fs9 --> Y;
A85: dom (doms FD) = dom FD by FUNCT_6:59
.= dom (Fs9 --> Y) by A20, FUNCOP_1:13 ;
A86: now__::_thesis:_for_w_being_set_st_w_in_dom_(doms_FD)_holds_
(Fs9_-->_Y)_._w_in_(doms_FD)_._w
let w be set ; ::_thesis: ( w in dom (doms FD) implies (Fs9 --> Y) . w in (doms FD) . w )
assume A87: w in dom (doms FD) ; ::_thesis: (Fs9 --> Y) . w in (doms FD) . w
then FD . w is Function of (K . w),((Fs9 --> the carrier of L) . w) by A85, PBOOLE:def_15;
then A88: dom (FD . w) = K . w by A85, A87, FUNCT_2:def_1
.= w by A85, A87, FUNCT_1:18 ;
( (doms FD) . w = dom (FD . w) & (Fs9 --> Y) . w = Y ) by A20, A85, A87, FUNCOP_1:7, FUNCT_6:22;
hence (Fs9 --> Y) . w in (doms FD) . w by A83, A85, A87, A88, SETFAM_1:def_1; ::_thesis: verum
end;
set s9 = Fs9 --> Y;
reconsider s = Fs9 --> Y as Element of pdFD by A85, A86, CARD_3:9;
now__::_thesis:_for_t_being_set_holds_
(_(_t_in_H2(s)_implies_t_in_{r}_)_&_(_t_in_{r}_implies_t_in_H2(s)_)_)
set u = the Element of Fs9;
let t be set ; ::_thesis: ( ( t in H2(s) implies t in {r} ) & ( t in {r} implies t in H2(s) ) )
A89: ( dom (Fs9 --> Y) = Fs9 & s . the Element of Fs9 = Y ) by FUNCOP_1:7, FUNCOP_1:13;
hereby ::_thesis: ( t in {r} implies t in H2(s) )
assume t in H2(s) ; ::_thesis: t in {r}
then consider u being Element of Fs9 such that
A90: 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
u in dom (FFD . s) ;
s . u = Y by FUNCOP_1:7;
hence t in {r} by A82, A90, TARSKI:def_1; ::_thesis: verum
end;
assume t in {r} ; ::_thesis: t in H2(s)
then A91: t = r by TARSKI:def_1;
( dom FD = dom (FFD . s) & dom s = dom FD ) by A28, WAYBEL_5:8;
hence t in H2(s) by A82, A91, A89; ::_thesis: verum
end;
then A92: { ("/\" ( { (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 Fs9 : u in dom (FFD . s) } = {r} by TARSKI:1;
( Inf = "/\" ((rng (FFD . s)),L) & rng (FFD . s) = H2(s) ) by A29, YELLOW_2:def_6;
hence r in rng (Infs ) by A92, A84, WAYBEL_5:14; ::_thesis: verum
end;
for j being Element of Fs9 holds rng (FD . j) is directed
proof
let j be Element of Fs9; ::_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 that
A93: k in rng (FD . j) and
A94: 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 )
consider kd being set such that
A95: kd in dom (FD . j) and
A96: (FD . j) . kd = k by A93, FUNCT_1:def_3;
consider md being set such that
A97: md in dom (FD . j) and
A98: (FD . j) . md = m by A94, FUNCT_1:def_3;
A99: K . j = j by FUNCT_1:18;
j in the carrier of (InclPoset (Filt (BoolePoset X))) ;
then consider FF being Filter of (BoolePoset X) such that
A100: j = FF by A1;
A101: dom (FD . j) = K . j by FUNCT_2:def_1;
then reconsider kd = kd as Element of (BoolePoset X) by A95, A99, A100;
reconsider md = md as Element of (BoolePoset X) by A97, A101, A99, A100;
consider nd being Element of (BoolePoset X) such that
A102: nd in FF and
A103: nd <= kd and
A104: nd <= md by A95, A97, A99, A100, WAYBEL_0:def_2;
set n = (FD . j) . nd;
A105: (FD . j) . nd in rng (FD . j) by A101, A99, A100, A102, FUNCT_1:def_3;
consider g being Function of (K . j),((Fs9 --> the carrier of L) . j) such that
A106: g = FD . j and
A107: for u being set st u in K . j holds
S1[g . u,u,j] by A7;
set nds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ;
A108: 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 A99, A100, A102, A107;
reconsider n = (FD . j) . nd as Element of L by A105;
take n ; ::_thesis: ( n in rng (FD . j) & k <= n & m <= n )
thus n in rng (FD . j) by A101, A99, A100, A102, FUNCT_1:def_3; ::_thesis: ( k <= n & m <= n )
A109: 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;
set mds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } ;
A110: nd c= md by A104, YELLOW_1:2;
A111: { (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 ) }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } or w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } )
assume w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ; ::_thesis: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) }
then ex x being Element of (BoolePoset X) st
( w = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in nd ) ) ;
hence w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in md ) } by A110; ::_thesis: verum
end;
A112: 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;
set kds = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } ;
A113: 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;
A114: nd c= kd by A103, YELLOW_1:2;
A115: { (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 ) }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } or w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } )
assume w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in nd ) } ; ::_thesis: w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) }
then ex x being Element of (BoolePoset X) st
( w = f . (uparrow x) & ex z being Element of X st
( x = {z} & z in nd ) ) ;
hence w in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in kd ) } by A114; ::_thesis: verum
end;
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 A95, A107;
hence k <= n by A96, A106, A108, A113, A109, A115, YELLOW_0:35; ::_thesis: m <= n
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 A97, A107;
hence m <= n by A98, A106, A108, A109, A112, A111, YELLOW_0:35; ::_thesis: verum
end;
then A116: Inf = Sup by WAYBEL_5:19
.= "\/" ((rng (Infs )),L) by YELLOW_2:def_5 ;
( inf Fs9 = meet Fs9 & (f -extension_to_hom) . (meet Fs9) = "\/" ( { ("/\" ( { (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, WAYBEL16:10;
hence "/\" (((f -extension_to_hom) .: Fs),L) = (f -extension_to_hom) . ("/\" (Fs,(InclPoset (Filt (BoolePoset X))))) by A26, A116, A27, TARSKI:1; ::_thesis: verum
end;
end;
end;
end;
theorem Th14: :: WAYBEL22:14
for X being 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) | (FixedUltraFilters X) = f
proof
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) | (FixedUltraFilters X) = f
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) | (FixedUltraFilters X) = f
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: (f -extension_to_hom) | (FixedUltraFilters X) = f
set FUF = FixedUltraFilters X;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
set F = f -extension_to_hom ;
A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_(_FixedUltraFilters_X_=_dom_((f_-extension_to_hom)_|_(FixedUltraFilters_X))_&_FixedUltraFilters_X_=_dom_f_&_(_for_xf_being_set_st_xf_in_FixedUltraFilters_X_holds_
((f_-extension_to_hom)_|_(FixedUltraFilters_X))_._xf_=_f_._xf_)_)
A3: dom (f -extension_to_hom) = the carrier of (InclPoset (Filt (BoolePoset X))) by FUNCT_2:def_1;
hence FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) by A1, Th9, RELAT_1:62; ::_thesis: ( FixedUltraFilters X = dom f & ( for xf being set st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )
thus FixedUltraFilters X = dom f by FUNCT_2:def_1; ::_thesis: for xf being set st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
let xf be set ; ::_thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )
assume A4: xf in FixedUltraFilters X ; ::_thesis: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
then reconsider FUF9 = FixedUltraFilters X as non empty Subset-Family of (BoolePoset X) ;
A5: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf by A4, FUNCT_1:49;
FixedUltraFilters X c= dom (f -extension_to_hom) by A1, A3, Th9;
then reconsider x9 = xf as Element of (InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def_1;
reconsider xf9 = xf as Element of FUF9 by A4;
set Xs = { ("/\" ( { (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 x9 } ;
reconsider f9 = f as Function of FUF9, the carrier of L ;
f9 . xf9 is Element of L ;
then reconsider fxf = f . xf9 as Element of L ;
consider xx being Element of (BoolePoset X) such that
A6: xf = uparrow xx and
A7: ex y being Element of X st xx = {y} by A4;
A8: { ("/\" ( { (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 x9 } is_<=_than fxf
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b 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 x9 } or b <= fxf )
assume b 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 x9 } ; ::_thesis: b <= fxf
then consider Y being Subset of X such that
A9: b = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A10: Y in x9 ;
set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L by YELLOW_0:17;
then A11: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is_>=_than b by A9, YELLOW_0:def_10;
reconsider Y = Y as Element of (BoolePoset X) by A6, A10;
consider y being Element of X such that
A12: xx = {y} by A7;
xx <= Y by A6, A10, WAYBEL_0:18;
then xx c= Y by YELLOW_1:2;
then y in Y by A12, ZFMISC_1:31;
then fxf in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A6, A12;
hence b <= fxf by A11, LATTICE3:def_8; ::_thesis: verum
end;
A13: for a being Element of L st { ("/\" ( { (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 x9 } is_<=_than a holds
fxf <= a
proof
xx <= xx ;
then reconsider Y = xx as Element of x9 by A6, WAYBEL_0:18;
set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
consider y being Element of X such that
A14: xx = {y} by A7;
now__::_thesis:_for_p_being_set_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_)__}__implies_p_in_{fxf}_)_&_(_p_in_{fxf}_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_)__}__)_)
let p be set ; ::_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 ) } implies p in {fxf} ) & ( p in {fxf} 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 ) } ) )
hereby ::_thesis: ( p in {fxf} 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 ) } )
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 ) } ; ::_thesis: p in {fxf}
then consider r being Element of (BoolePoset X) such that
A15: p = f . (uparrow r) and
A16: ex z being Element of X st
( r = {z} & z in Y ) ;
xx = r by A14, A16, TARSKI:def_1;
hence p in {fxf} by A6, A15, TARSKI:def_1; ::_thesis: verum
end;
assume p in {fxf} ; ::_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 ) }
then A17: p = fxf by TARSKI:def_1;
y in Y by A14, TARSKI:def_1;
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 ) } by A6, A14, A17; ::_thesis: verum
end;
then { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } = {fxf} by TARSKI:1;
then fxf = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) by YELLOW_0:39;
then A18: fxf 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 x9 } by A2;
let a be Element of L; ::_thesis: ( { ("/\" ( { (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 x9 } is_<=_than a implies fxf <= a )
assume { ("/\" ( { (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 x9 } is_<=_than a ; ::_thesis: fxf <= a
hence fxf <= a by A18, LATTICE3:def_9; ::_thesis: verum
end;
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 x9 } ,L by YELLOW_0:17;
then f . xf = "\/" ( { ("/\" ( { (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 x9 } ,L) by A8, A13, YELLOW_0:def_9;
hence ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf by A5, Def3; ::_thesis: verum
end;
hence (f -extension_to_hom) | (FixedUltraFilters X) = f by FUNCT_1:2; ::_thesis: verum
end;
theorem Th15: :: WAYBEL22:15
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
proof
let X be set ; ::_thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let L be non empty complete continuous Poset; ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
let h be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; ::_thesis: ( h | (FixedUltraFilters X) = f implies h = f -extension_to_hom )
assume A1: h | (FixedUltraFilters X) = f ; ::_thesis: h = f -extension_to_hom
set F = f -extension_to_hom ;
set cL = the carrier of L;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
set cIP = the carrier of (InclPoset (Filt (BoolePoset X)));
A2: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def_1;
reconsider F9 = f -extension_to_hom as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
reconsider h9 = h as Function of the carrier of (InclPoset (Filt (BoolePoset X))), the carrier of L ;
A3: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
now__::_thesis:_for_Fi_being_Element_of_the_carrier_of_(InclPoset_(Filt_(BoolePoset_X)))_holds_h9_._Fi_=_F9_._Fi
set FUF = FixedUltraFilters X;
let Fi be Element of the carrier of (InclPoset (Filt (BoolePoset X))); ::_thesis: h9 . Fi = F9 . Fi
Fi in Filt (BoolePoset X) by A2;
then consider FF being Filter of (BoolePoset X) such that
A4: Fi = FF ;
set Xsf = { ("/\" ( { (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 FF } ;
set Xs = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } ;
A5: { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } or p in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume p in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } ; ::_thesis: p in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex YY being Subset of X st
( p = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) & YY in FF ) ;
hence p in the carrier of (InclPoset (Filt (BoolePoset X))) ; ::_thesis: verum
end;
now__::_thesis:_not__{__("/\"_(_{__(uparrow_x)_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__,(InclPoset_(Filt_(BoolePoset_X)))))_where_Y_is_Subset_of_X_:_Y_in_FF__}__is_empty
consider YY being set such that
A6: YY in FF by XBOOLE_0:def_1;
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in YY ) } ,(InclPoset (Filt (BoolePoset X)))) in { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } by A3, A6;
hence not { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } is empty ; ::_thesis: verum
end;
then reconsider Xs = { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A5;
A7: ex_sup_of Xs, InclPoset (Filt (BoolePoset X)) by YELLOW_0:17;
A8: Xs is directed
proof
let a, b be Element of (InclPoset (Filt (BoolePoset X))); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in Xs or not b in Xs or ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 ) )
assume that
A9: a in Xs and
A10: b in Xs ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
consider Yb being Subset of X such that
A11: b = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) and
A12: Yb in FF by A10;
reconsider Yb9 = Yb as Element of FF by A12;
set Xsb = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ;
consider Ya being Subset of X such that
A13: a = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) and
A14: Ya in FF by A9;
reconsider Ya9 = Ya as Element of FF by A14;
set Xsa = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ;
percases ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty or { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty or ( not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty & not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty ) ) ;
supposeA15: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take a ; ::_thesis: ( a in Xs & a <= a & b <= a )
thus a in Xs by A9; ::_thesis: ( a <= a & b <= a )
thus a <= a ; ::_thesis: b <= a
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A15;
hence b <= a by A13, YELLOW_0:45; ::_thesis: verum
end;
supposeA16: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take b ; ::_thesis: ( b in Xs & a <= b & b <= b )
thus b in Xs by A10; ::_thesis: ( a <= b & b <= b )
"/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A16;
hence a <= b by A11, YELLOW_0:45; ::_thesis: b <= b
thus b <= b ; ::_thesis: verum
end;
supposeA17: ( not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } is empty & not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } is empty ) ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yb ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsb = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yb ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Ya ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsa = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Ya ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A17;
A18: "/\" (Xsb,(InclPoset (Filt (BoolePoset X)))) = meet Xsb by WAYBEL16:10;
consider Yab being Element of (BoolePoset X) such that
A19: Yab in FF and
A20: Yab <= Ya9 and
A21: Yab <= Yb9 by WAYBEL_0:def_2;
reconsider Yab = Yab as Element of FF by A19;
set c = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))));
set Xsc = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ;
A22: "/\" (Xsa,(InclPoset (Filt (BoolePoset X)))) = meet Xsa by WAYBEL16:10;
thus ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 ) ::_thesis: verum
proof
percases ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty or not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty ) ;
supposeA23: { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
take "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; ::_thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; ::_thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
A24: "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) = Top (InclPoset (Filt (BoolePoset X))) by A23;
hence a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_0:45; ::_thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
thus b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A24, YELLOW_0:45; ::_thesis: verum
end;
supposeA25: not { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } is empty ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (Filt (BoolePoset X))) st
( b1 in Xs & a <= b1 & b <= b1 )
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsc = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } as non empty Subset of (InclPoset (Filt (BoolePoset X))) by A25;
take "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) ; ::_thesis: ( "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs & a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
thus "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) in Xs by A3; ::_thesis: ( a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) & b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
A26: "/\" (Xsc,(InclPoset (Filt (BoolePoset X)))) = meet Xsc by WAYBEL16:10;
a c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in a or d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
Xsc c= Xsa
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Xsc or r in Xsa )
assume r in Xsc ; ::_thesis: r in Xsa
then A27: ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
Yab c= Ya by A20, YELLOW_1:2;
hence r in Xsa by A27; ::_thesis: verum
end;
then A28: meet Xsa c= meet Xsc by SETFAM_1:6;
assume d in a ; ::_thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A13, A22, A26, A28; ::_thesis: verum
end;
hence a <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; ::_thesis: b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
b c= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in b or d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) )
Xsc c= Xsb
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Xsc or r in Xsb )
assume r in Xsc ; ::_thesis: r in Xsb
then A29: ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Yab ) ) ;
Yab c= Yb by A21, YELLOW_1:2;
hence r in Xsb by A29; ::_thesis: verum
end;
then A30: meet Xsb c= meet Xsc by SETFAM_1:6;
assume d in b ; ::_thesis: d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X))))
hence d in "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by A11, A18, A26, A30; ::_thesis: verum
end;
hence b <= "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Yab ) } ,(InclPoset (Filt (BoolePoset X)))) by YELLOW_1:3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A31: h is infs-preserving by WAYBEL16:def_1;
now__::_thesis:_for_s_being_set_holds_
(_(_s_in_h_.:_Xs_implies_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_FF__}__)_&_(_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_FF__}__implies_s_in_h_.:_Xs_)_)
let s be set ; ::_thesis: ( ( s in h .: Xs implies 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 FF } ) & ( 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 FF } implies s in h .: Xs ) )
hereby ::_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 FF } implies s in h .: Xs )
assume s in h .: Xs ; ::_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 FF }
then consider t being set such that
t in the carrier of (InclPoset (Filt (BoolePoset X))) and
A32: t in Xs and
A33: s = h . t by FUNCT_2:64;
consider Y being Subset of X such that
A34: ( t = "/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X)))) & Y in FF ) by A32;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as Subset of (InclPoset (Filt (BoolePoset X))) ;
set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
now__::_thesis:_for_u_being_set_holds_
(_(_u_in_h_.:_Xsi_implies_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_&_(_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_u_in_h_.:_Xsi_)_)
let u be set ; ::_thesis: ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies u in h .: Xsi ) )
hereby ::_thesis: ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies u in h .: Xsi )
assume u in h .: Xsi ; ::_thesis: u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
then consider v being set such that
v in the carrier of (InclPoset (Filt (BoolePoset X))) and
A35: v in Xsi and
A36: u = h . v by FUNCT_2:64;
A37: ex x being Element of (BoolePoset X) st
( v = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A35;
then v in FixedUltraFilters X ;
then h . v = f . v by A1, FUNCT_1:49;
hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A36, A37; ::_thesis: verum
end;
assume u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: u in h .: Xsi
then consider x being Element of (BoolePoset X) such that
A38: u = f . (uparrow x) and
A39: ex z being Element of X st
( x = {z} & z in Y ) ;
uparrow x in FixedUltraFilters X by A39;
then A40: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;
uparrow x in Xsi by A39;
hence u in h .: Xsi by A38, A40, FUNCT_2:35; ::_thesis: verum
end;
then A41: h .: Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by TARSKI:1;
( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, WAYBEL_0:def_32, YELLOW_0:17;
then inf (h .: Xsi) = h . (inf Xsi) by WAYBEL_0:def_30;
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 FF } by A33, A34, A41; ::_thesis: verum
end;
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 FF } ; ::_thesis: s in h .: Xs
then consider Y being Subset of X such that
A42: s = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A43: Y in FF ;
set Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
{ (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } c= the carrier of (InclPoset (Filt (BoolePoset X)))
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } or r in the carrier of (InclPoset (Filt (BoolePoset X))) )
assume r in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: r in the carrier of (InclPoset (Filt (BoolePoset X)))
then ex xz being Element of (BoolePoset X) st
( r = uparrow xz & ex z being Element of X st
( xz = {z} & z in Y ) ) ;
hence r in the carrier of (InclPoset (Filt (BoolePoset X))) by A2; ::_thesis: verum
end;
then reconsider Xsi = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } as Subset of (InclPoset (Filt (BoolePoset X))) ;
set Xsif = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
( h preserves_inf_of Xsi & ex_inf_of Xsi, InclPoset (Filt (BoolePoset X)) ) by A31, WAYBEL_0:def_32, YELLOW_0:17;
then A44: inf (h .: Xsi) = h . (inf Xsi) by WAYBEL_0:def_30;
now__::_thesis:_for_u_being_set_holds_
(_(_u_in_h_.:_Xsi_implies_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__)_&_(_u_in__{__(f_._(uparrow_x))_where_x_is_Element_of_(BoolePoset_X)_:_ex_z_being_Element_of_X_st_
(_x_=_{z}_&_z_in_Y_)__}__implies_u_in_h_.:_Xsi_)_)
let u be set ; ::_thesis: ( ( u in h .: Xsi implies u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ) & ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies u in h .: Xsi ) )
hereby ::_thesis: ( u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies u in h .: Xsi )
assume u in h .: Xsi ; ::_thesis: u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
then consider v being set such that
v in the carrier of (InclPoset (Filt (BoolePoset X))) and
A45: v in Xsi and
A46: u = h . v by FUNCT_2:64;
A47: ex x being Element of (BoolePoset X) st
( v = uparrow x & ex z being Element of X st
( x = {z} & z in Y ) ) by A45;
then v in FixedUltraFilters X ;
then h . v = f . v by A1, FUNCT_1:49;
hence u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A46, A47; ::_thesis: verum
end;
assume u in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; ::_thesis: u in h .: Xsi
then consider x being Element of (BoolePoset X) such that
A48: u = f . (uparrow x) and
A49: ex z being Element of X st
( x = {z} & z in Y ) ;
uparrow x in FixedUltraFilters X by A49;
then A50: h . (uparrow x) = f . (uparrow x) by A1, FUNCT_1:49;
uparrow x in Xsi by A49;
hence u in h .: Xsi by A48, A50, FUNCT_2:35; ::_thesis: verum
end;
then A51: h .: Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by TARSKI:1;
inf Xsi in Xs by A43;
hence s in h .: Xs by A42, A44, A51, FUNCT_2:35; ::_thesis: verum
end;
then A52: h .: Xs = { ("/\" ( { (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 FF } by TARSKI:1;
A53: FF = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in FF } ,(InclPoset (Filt (BoolePoset X)))) by Th11;
h is directed-sups-preserving by WAYBEL16:def_1;
then h preserves_sup_of Xs by A8, WAYBEL_0:def_37;
hence h9 . Fi = sup (h .: Xs) by A4, A53, A7, WAYBEL_0:def_31
.= F9 . Fi by A4, A52, Def3 ;
::_thesis: verum
end;
hence h = f -extension_to_hom by FUNCT_2:63; ::_thesis: verum
end;
theorem Th16: :: WAYBEL22:16
for X being set holds FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
proof
let X be set ; ::_thesis: FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
set FUF = FixedUltraFilters X;
set IP = InclPoset (Filt (BoolePoset X));
let L be non empty complete continuous Poset; :: according to WAYBEL22:def_1 ::_thesis: for f being Function of (FixedUltraFilters X), the carrier of L ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
let f be Function of (FixedUltraFilters X), the carrier of L; ::_thesis: ex h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st
( h | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = h ) )
reconsider F = f -extension_to_hom as CLHomomorphism of InclPoset (Filt (BoolePoset X)),L by WAYBEL16:def_1;
take F ; ::_thesis: ( F | (FixedUltraFilters X) = f & ( for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F ) )
thus F | (FixedUltraFilters X) = f by Th14; ::_thesis: for h9 being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h9 | (FixedUltraFilters X) = f holds
h9 = F
let h9 be CLHomomorphism of InclPoset (Filt (BoolePoset X)),L; ::_thesis: ( h9 | (FixedUltraFilters X) = f implies h9 = F )
assume h9 | (FixedUltraFilters X) = f ; ::_thesis: h9 = F
hence h9 = F by Th15; ::_thesis: verum
end;
theorem Th17: :: WAYBEL22:17
for L, M being complete continuous LATTICE
for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds
L,M are_isomorphic
proof
let L, M be complete continuous LATTICE; ::_thesis: for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds
L,M are_isomorphic
let Lg, Mg be set ; ::_thesis: ( Lg is_FreeGen_set_of L & Mg is_FreeGen_set_of M & card Lg = card Mg implies L,M are_isomorphic )
assume that
A1: Lg is_FreeGen_set_of L and
A2: Mg is_FreeGen_set_of M and
A3: card Lg = card Mg ; ::_thesis: L,M are_isomorphic
Lg,Mg are_equipotent by A3, CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = Lg and
A6: rng f = Mg by WELLORD2:def_4;
set g = f " ;
A7: dom (f ") = Mg by A4, A6, FUNCT_1:33;
reconsider Mg = Mg as Subset of M by A2, Th7;
A8: rng (f ") = Lg by A4, A5, FUNCT_1:33;
reconsider Lg = Lg as Subset of L by A1, Th7;
Mg c= the carrier of M ;
then reconsider f = f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def_1, RELSET_1:4;
consider F being CLHomomorphism of L,M such that
A9: F | Lg = f and
for h9 being CLHomomorphism of L,M st h9 | Lg = f holds
h9 = F by A1, Def1;
Lg c= the carrier of L ;
then reconsider g = f " as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def_1, RELSET_1:4;
consider G being CLHomomorphism of M,L such that
A10: G | Mg = g and
for h9 being CLHomomorphism of M,L st h9 | Mg = g holds
h9 = G by A2, Def1;
reconsider GF = G * F as CLHomomorphism of L,L by Th2;
GF | Lg = G * f by A9, RELAT_1:83
.= g * f by A6, A10, FUNCT_4:2
.= id Lg by A4, A5, FUNCT_1:39 ;
then A11: GF = id L by A1, Th8;
then A12: F is V13() by FUNCT_2:23;
reconsider FG = F * G as CLHomomorphism of M,M by Th2;
F is directed-sups-preserving by WAYBEL16:def_1;
then A13: F is monotone by WAYBEL17:3;
G is directed-sups-preserving by WAYBEL16:def_1;
then A14: G is monotone by WAYBEL17:3;
FG | Mg = F * g by A10, RELAT_1:83
.= f * g by A8, A9, FUNCT_4:2
.= id Mg by A4, A6, FUNCT_1:39 ;
then FG = id M by A2, Th8;
then F is onto by FUNCT_2:23;
then rng F = the carrier of M by FUNCT_2:def_3;
then G = F " by A11, A12, FUNCT_2:30;
then F is isomorphic by A12, A13, A14, WAYBEL_0:def_38;
hence L,M are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;
theorem :: WAYBEL22:18
for X being set
for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
proof
let X be set ; ::_thesis: for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
A1: ( FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X)) & card X = card (FixedUltraFilters X) ) by Th10, Th16;
let L be complete continuous LATTICE; ::_thesis: for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
let G be set ; ::_thesis: ( G is_FreeGen_set_of L & card G = card X implies L, InclPoset (Filt (BoolePoset X)) are_isomorphic )
assume ( G is_FreeGen_set_of L & card G = card X ) ; ::_thesis: L, InclPoset (Filt (BoolePoset X)) are_isomorphic
hence L, InclPoset (Filt (BoolePoset X)) are_isomorphic by A1, Th17; ::_thesis: verum
end;