let T be non empty TopSpace; 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); 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); { 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 A7:
not
Y is
empty
;
{ y where y is Element of T : [x,y] in b } in the topology of Tthen 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):];
( 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
;
{ 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):];
( 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
;
{ 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 A20:
not
x in O
;
{ 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
XBOOLE_0:def 10 the carrier of T c= { z where z is Element of T : [x,z] in block_Pervin_quasi_uniformity O }
let a be
object ;
TARSKI:def 3 ( 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
;
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 }
;
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;
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;
( S1[k] implies S1[k + 1] )
assume A24:
S1[
k]
;
S1[k + 1]
now 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 Tlet Z be non
empty Subset-Family of
[: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):];
( 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
;
{ y where y is Element of T : [x,y] in meet Z } in the topology of Tset 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 ;
TARSKI:def 3 ( 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 }
;
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;
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;
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 ;
TARSKI:def 3 ( 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 }
;
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
;
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;
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;
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;
verum end;
hence
S1[
k + 1]
;
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;
verum
end; hence
{ y where y is Element of T : [x,y] in b } in the
topology of
T
by A8, A1, A2, A7;
verum end; end;