let X be set ; :: thesis: for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 holds
ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.cB.] )
let cB be Subset-Family of [:X,X:]; :: thesis: ( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 implies ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.cB.] ) )
assume that
A1: cB is quasi_basis and
A2: cB is axiom_UP1 and
A3: cB is axiom_UP2 and
A4: cB is axiom_UP3 ; :: thesis: ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.cB.] )
set US = UniformSpaceStr(# X,<.cB.] #);
A5: <.cB.] = { x where x is Subset of [:X,X:] : ex b being Element of cB st b c= x } by CARDFIL2:14;
now :: thesis: ( UniformSpaceStr(# X,<.cB.] #) is upper & UniformSpaceStr(# X,<.cB.] #) is cap-closed & UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U2 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for Y1, Y2 being Subset of [:X,X:] st Y1 in <.cB.] & Y1 c= Y2 holds
Y2 in <.cB.]
proof
let Y1, Y2 be Subset of [:X,X:]; :: thesis: ( Y1 in <.cB.] & Y1 c= Y2 implies Y2 in <.cB.] )
assume that
A6: Y1 in <.cB.] and
A7: Y1 c= Y2 ; :: thesis: Y2 in <.cB.]
consider x being Subset of [:X,X:] such that
A8: Y1 = x and
A9: ex b being Element of cB st b c= x by A5, A6;
consider B being Element of cB such that
A10: B c= x by A9;
B c= Y2 by A10, A8, A7;
hence Y2 in <.cB.] by A5; :: thesis: verum
end;
then <.cB.] is upper ;
hence UniformSpaceStr(# X,<.cB.] #) is upper ; :: thesis: ( UniformSpaceStr(# X,<.cB.] #) is cap-closed & UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U2 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for Y1, Y2 being set st Y1 in <.cB.] & Y2 in <.cB.] holds
Y1 /\ Y2 in <.cB.]
proof
let Y1, Y2 be set ; :: thesis: ( Y1 in <.cB.] & Y2 in <.cB.] implies Y1 /\ Y2 in <.cB.] )
assume that
A11: Y1 in <.cB.] and
A12: Y2 in <.cB.] ; :: thesis: Y1 /\ Y2 in <.cB.]
consider x being Subset of [:X,X:] such that
A13: Y1 = x and
A14: ex b being Element of cB st b c= x by A5, A11;
consider B1 being Element of cB such that
A15: B1 c= x by A14;
Y2 in { x where x is Subset of [:X,X:] : ex b being Element of cB st b c= x } by CARDFIL2:14, A12;
then consider y being Subset of [:X,X:] such that
A16: Y2 = y and
A17: ex b being Element of cB st b c= y ;
consider B2 being Element of cB such that
A18: B2 c= y by A17;
A19: B1 /\ B2 c= Y1 /\ Y2 by A13, A15, A18, A16, XBOOLE_1:27;
consider B3 being Element of cB such that
A20: B3 c= B1 /\ B2 by A1;
A21: Y1 /\ Y2 c= [:X,X:] /\ [:X,X:] by A11, A12, XBOOLE_1:27;
B3 c= Y1 /\ Y2 by A20, A19;
hence Y1 /\ Y2 in <.cB.] by A5, A21; :: thesis: verum
end;
hence UniformSpaceStr(# X,<.cB.] #) is cap-closed by FINSUB_1:def 2; :: thesis: ( UniformSpaceStr(# X,<.cB.] #) is axiom_U1 & UniformSpaceStr(# X,<.cB.] #) is axiom_U2 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for S being Element of <.cB.] holds id X c= S
proof
let S be Element of <.cB.]; :: thesis: id X c= S
S in { x where x is Subset of [:X,X:] : ex b being Element of cB st b c= x } by A5;
then consider x being Subset of [:X,X:] such that
A22: S = x and
A23: ex b being Element of cB st b c= x ;
consider B being Element of cB such that
A24: B c= x by A23;
id X c= B by A2;
hence id X c= S by A24, A22; :: thesis: verum
end;
hence UniformSpaceStr(# X,<.cB.] #) is axiom_U1 ; :: thesis: ( UniformSpaceStr(# X,<.cB.] #) is axiom_U2 & UniformSpaceStr(# X,<.cB.] #) is axiom_U3 )
for S being Element of <.cB.] holds S ~ in <.cB.]
proof
let S be Element of <.cB.]; :: thesis: S ~ in <.cB.]
reconsider S1 = S as Subset of [:X,X:] ;
consider B being Element of cB such that
A27: B c= S1 by CARDFIL2:def 8;
A29: B ~ c= S1 ~ by A27, SYSREL:11;
consider B2 being Element of cB such that
A30: B2 c= B ~ by A3;
B2 c= S1 ~ by A29, A30;
hence S ~ in <.cB.] by CARDFIL2:def 8; :: thesis: verum
end;
hence UniformSpaceStr(# X,<.cB.] #) is axiom_U2 ; :: thesis: UniformSpaceStr(# X,<.cB.] #) is axiom_U3
for S being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S
proof
let S be Element of the entourages of UniformSpaceStr(# X,<.cB.] #); :: thesis: ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S
S in <.cB.] ;
then consider B1 being Element of cB such that
A31: B1 c= S by CARDFIL2:def 8;
consider B2 being Element of cB such that
A32: B2 * B2 c= B1 by A4;
per cases ( cB is empty or not cB is empty ) ;
suppose A34: cB is empty ; :: thesis: ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S
then A35: B2 = {} by SUBSET_1:def 1;
{} c= [:X,X:] ;
then reconsider B2 = B2 as Element of the entourages of UniformSpaceStr(# X,<.cB.] #) by A35, A34, CARDFIL2:15;
B2 [*] B2 c= S by A35;
hence ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S ; :: thesis: verum
end;
suppose A36: not cB is empty ; :: thesis: ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S
cB c= <.cB.] by CARDFIL2:18;
then reconsider W = B2 as Element of the entourages of UniformSpaceStr(# X,<.cB.] #) by A36;
W [*] W c= S by A31, A32;
hence ex W being Element of the entourages of UniformSpaceStr(# X,<.cB.] #) st W * W c= S ; :: thesis: verum
end;
end;
end;
hence UniformSpaceStr(# X,<.cB.] #) is axiom_U3 ; :: thesis: verum
end;
then reconsider US = UniformSpaceStr(# X,<.cB.] #) as strict UniformSpace ;
take US ; :: thesis: ( the carrier of US = X & the entourages of US = <.cB.] )
thus the carrier of US = X ; :: thesis: the entourages of US = <.cB.]
thus the entourages of US = <.cB.] ; :: thesis: verum