let T be non empty TopSpace; :: thesis: for x being Element of the carrier of (Pervin_quasi_uniformity T)
for b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) holds { y where y is Element of T : [x,y] in b } in the topology of T
let x be Element of the carrier of (Pervin_quasi_uniformity T); :: thesis: for b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) holds { y where y is Element of T : [x,y] in b } in the topology of T
let b be Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T); :: thesis: { y where y is Element of T : [x,y] in b } in the topology of T
consider Y being Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] such that
A1: Y c= subbasis_Pervin_quasi_uniformity T and
A2: Y is finite and
A3: b = Intersect Y by CANTOR_1:def 3;
per cases ( Y is empty or not Y is empty ) ;
suppose Y is empty ; :: thesis: { y where y is Element of T : [x,y] in b } in the topology of T
then A4: b = [: the carrier of T, the carrier of T:] by A3, SETFAM_1:def 9;
{ y where y is Element of T : [x,y] in b } = the carrier of T
proof
thus { y where y is Element of T : [x,y] in b } c= the carrier of T :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= { y where y is Element of T : [x,y] in b }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of T : [x,y] in b } or a in the carrier of T )
assume a in { y where y is Element of T : [x,y] in b } ; :: thesis: a in the carrier of T
then ex y being Element of T st
( a = y & [x,y] in b ) ;
hence a in the carrier of T ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of T or a in { y where y is Element of T : [x,y] in b } )
assume a in the carrier of T ; :: thesis: a in { y where y is Element of T : [x,y] in b }
then reconsider y = a as Element of T ;
[x,y] in [: the carrier of T, the carrier of T:] ;
hence a in { y where y is Element of T : [x,y] in b } by A4; :: thesis: verum
end;
hence { y where y is Element of T : [x,y] in b } in the topology of T by PRE_TOPC:def 1; :: thesis: verum
end;
suppose A7: not Y is empty ; :: thesis: { y where y is Element of T : [x,y] in b } in the topology of T
then A8: b = meet Y by A3, SETFAM_1:def 9;
for Y being non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] st Y c= subbasis_Pervin_quasi_uniformity T & Y is finite holds
{ y where y is Element of T : [x,y] in meet Y } in the topology of T
proof
let Y be non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):]; :: thesis: ( Y c= subbasis_Pervin_quasi_uniformity T & Y is finite implies { y where y is Element of T : [x,y] in meet Y } in the topology of T )
assume that
A9: Y c= subbasis_Pervin_quasi_uniformity T and
A10: Y is finite ; :: thesis: { y where y is Element of T : [x,y] in meet Y } in the topology of T
defpred S1[ Nat] means for Z being non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] st Z c= subbasis_Pervin_quasi_uniformity T & card Z = $1 holds
{ y where y is Element of T : [x,y] in meet Z } in the topology of T;
for Z being non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] st Z c= subbasis_Pervin_quasi_uniformity T & card Z = 1 holds
{ y where y is Element of T : [x,y] in meet Z } in the topology of T
proof
let Z be non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):]; :: thesis: ( Z c= subbasis_Pervin_quasi_uniformity T & card Z = 1 implies { y where y is Element of T : [x,y] in meet Z } in the topology of T )
assume that
A11: Z c= subbasis_Pervin_quasi_uniformity T and
A12: card Z = 1 ; :: thesis: { y where y is Element of T : [x,y] in meet Z } in the topology of T
consider t being object such that
A13: Z = {t} by A12, CARD_2:42;
reconsider y = t as set by TARSKI:1;
A14: meet Z = y by A13, SETFAM_1:10;
t in subbasis_Pervin_quasi_uniformity T by A11, A13, ZFMISC_1:31;
then consider O being Element of the topology of T such that
A15: t = block_Pervin_quasi_uniformity O ;
per cases ( x in O or not x in O ) ;
suppose A16: x in O ; :: thesis: { y where y is Element of T : [x,y] in meet Z } in the topology of T
{ y where y is Element of T : [x,y] in meet Z } in the topology of T
proof
A17: { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } = O
proof
A18: { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } c= O
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } or a in O )
assume a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } ; :: thesis: a in O
then ex z being Element of T st
( a = z & [x,z] in block_Pervin_quasi_uniformity O ) ;
then ( [x,a] in [:( the carrier of T \ O), the carrier of T:] or [x,a] in [: the carrier of T,O:] ) by XBOOLE_0:def 3;
then ( ( x in the carrier of T \ O & a in the carrier of T ) or ( x in the carrier of T & a in O ) ) by ZFMISC_1:87;
hence a in O by A16, XBOOLE_0:def 5; :: thesis: verum
end;
O c= { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in O or a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } )
assume A19: a in O ; :: thesis: a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O }
then reconsider b = a as Element of T ;
[x,a] in [: the carrier of T,O:] by A19, ZFMISC_1:87;
then [x,b] in block_Pervin_quasi_uniformity O by XBOOLE_0:def 3;
hence a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } ; :: thesis: verum
end;
hence { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } = O by A18; :: thesis: verum
end;
thus { y where y is Element of T : [x,y] in meet Z } in the topology of T by A15, A14, A17; :: thesis: verum
end;
hence { y where y is Element of T : [x,y] in meet Z } in the topology of T ; :: thesis: verum
end;
suppose A20: not x in O ; :: thesis: { y where y is Element of T : [x,y] in meet Z } in the topology of T
{ z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } = the carrier of T
proof
thus { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } c= the carrier of T :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } or a in the carrier of T )
assume a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } ; :: thesis: a in the carrier of T
then ex z being Element of T st
( a = z & [x,z] in block_Pervin_quasi_uniformity O ) ;
hence a in the carrier of T ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of T or a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } )
assume a in the carrier of T ; :: thesis: a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O }
then reconsider b = a as Element of T ;
x in the carrier of T \ O by A20, XBOOLE_0:def 5;
then ( [x,b] in [:( the carrier of T \ O), the carrier of T:] or [x,b] in [: the carrier of T,O:] ) by ZFMISC_1:87;
then [x,b] in block_Pervin_quasi_uniformity O by XBOOLE_0:def 3;
hence a in { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O } ; :: thesis: verum
end;
hence { y where y is Element of T : [x,y] in meet Z } in the topology of T by A15, A14, PRE_TOPC:def 1; :: thesis: verum
end;
end;
end;
then A22: S1[1] ;
A23: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A24: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for Z being non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] st Z c= subbasis_Pervin_quasi_uniformity T & card Z = k + 1 holds
{ y where y is Element of T : [x,y] in meet Z } in the topology of T
let Z be non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):]; :: thesis: ( Z c= subbasis_Pervin_quasi_uniformity T & card Z = k + 1 implies { y where y is Element of T : [x,y] in meet Z } in the topology of T )
assume that
A25: Z c= subbasis_Pervin_quasi_uniformity T and
A26: card Z = k + 1 ; :: thesis: { y where y is Element of T : [x,y] in meet Z } in the topology of T
set z = the Element of Z;
A27: card (Z \ { the Element of Z}) = k by A26, STIRL2_1:55;
then A28: not Z \ { the Element of Z} is empty ;
Z \ { the Element of Z} c= Z by XBOOLE_1:36;
then A29: Z \ { the Element of Z} c= subbasis_Pervin_quasi_uniformity T by A25;
Z \ { the Element of Z} is non empty Subset-Family of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] by A27;
then A30: { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } in the topology of T by A24, A27, A29;
A31: { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } = { y where y is Element of T : [x,y] in meet Z }
proof
set M1 = { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } ;
set M2 = { y where y is Element of T : [x,y] in the Element of Z } ;
set M3 = { y where y is Element of T : [x,y] in meet Z } ;
A32: { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } c= { y where y is Element of T : [x,y] in meet Z }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } or a in { y where y is Element of T : [x,y] in meet Z } )
assume a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } ; :: thesis: a in { y where y is Element of T : [x,y] in meet Z }
then A33: ( a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } & a in { y where y is Element of T : [x,y] in the Element of Z } ) by XBOOLE_0:def 4;
then consider b being Element of T such that
A34: a = b and
A35: [x,b] in meet (Z \ { the Element of Z}) ;
consider c being Element of T such that
A36: a = c and
A37: [x,c] in the Element of Z by A33;
now :: thesis: for Y being set st Y in Z holds
[x,b] in Y
let Y be set ; :: thesis: ( Y in Z implies [x,b] in b1 )
assume Y in Z ; :: thesis: [x,b] in b1
per cases then ( ( Y in Z & not Y in { the Element of Z} ) or Y in { the Element of Z} ) ;
suppose ( Y in Z & not Y in { the Element of Z} ) ; :: thesis: [x,b] in b1
then Y in Z \ { the Element of Z} by XBOOLE_0:def 5;
hence [x,b] in Y by A35, SETFAM_1:def 1; :: thesis: verum
end;
suppose Y in { the Element of Z} ; :: thesis: [x,b] in b1
hence [x,b] in Y by A34, A36, A37, TARSKI:def 1; :: thesis: verum
end;
end;
end;
then [x,b] in meet Z by SETFAM_1:def 1;
hence a in { y where y is Element of T : [x,y] in meet Z } by A34; :: thesis: verum
end;
{ y where y is Element of T : [x,y] in meet Z } c= { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of T : [x,y] in meet Z } or a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } )
assume a in { y where y is Element of T : [x,y] in meet Z } ; :: thesis: a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z }
then consider b being Element of T such that
A38: a = b and
A39: [x,b] in meet Z ;
now :: thesis: for Y being set st Y in Z \ { the Element of Z} holds
[x,b] in Y
let Y be set ; :: thesis: ( Y in Z \ { the Element of Z} implies [x,b] in Y )
assume A40: Y in Z \ { the Element of Z} ; :: thesis: [x,b] in Y
Z \ { the Element of Z} c= Z by XBOOLE_1:36;
hence [x,b] in Y by A40, A39, SETFAM_1:def 1; :: thesis: verum
end;
then [x,b] in meet (Z \ { the Element of Z}) by A28, SETFAM_1:def 1;
then A41: b in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } ;
[x,b] in the Element of Z by A39, SETFAM_1:def 1;
then a in { y where y is Element of T : [x,y] in the Element of Z } by A38;
hence a in { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } by A41, A38, XBOOLE_0:def 4; :: thesis: verum
end;
hence { y where y is Element of T : [x,y] in meet (Z \ { the Element of Z}) } /\ { y where y is Element of T : [x,y] in the Element of Z } = { y where y is Element of T : [x,y] in meet Z } by A32; :: thesis: verum
end;
the Element of Z in subbasis_Pervin_quasi_uniformity T by A25;
then { y where y is Element of T : [x,y] in the Element of Z } in the topology of T by Th29;
hence { y where y is Element of T : [x,y] in meet Z } in the topology of T by A31, A30, PRE_TOPC:def 1; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A42: for k being non zero Nat holds S1[k] from NAT_1:sch 10(A22, A23);
 ex n being Nat st card Y = n by A10;
hence { y where y is Element of T : [x,y] in meet Y } in the topology of T by A9, A42; :: thesis: verum
end;
hence { y where y is Element of T : [x,y] in b } in the topology of T by A8, A1, A2, A7; :: thesis: verum
end;
end;