:: 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;