Database
BASIC TOPOLOGY
Uniform Structures and Spaces
The topology induced by an uniform structure
ustuqtop0
Next ⟩
ustuqtop1
Metamath Proof Explorer
Ascii
Unicode
Theorem
ustuqtop0
Description:
Lemma for
ustuqtop
.
(Contributed by
Thierry Arnoux
, 11-Jan-2018)
Ref
Expression
Hypothesis
utopustuq.1
⊢
N
=
p
∈
X
⟼
ran
⁡
v
∈
U
⟼
v
p
Assertion
ustuqtop0
⊢
U
∈
UnifOn
⁡
X
→
N
:
X
⟶
𝒫
𝒫
X
Proof
Step
Hyp
Ref
Expression
1
utopustuq.1
⊢
N
=
p
∈
X
⟼
ran
⁡
v
∈
U
⟼
v
p
2
ustimasn
⊢
U
∈
UnifOn
⁡
X
∧
v
∈
U
∧
p
∈
X
→
v
p
⊆
X
3
2
3expa
⊢
U
∈
UnifOn
⁡
X
∧
v
∈
U
∧
p
∈
X
→
v
p
⊆
X
4
3
an32s
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
∧
v
∈
U
→
v
p
⊆
X
5
vex
⊢
v
∈
V
6
5
imaex
⊢
v
p
∈
V
7
6
elpw
⊢
v
p
∈
𝒫
X
↔
v
p
⊆
X
8
4
7
sylibr
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
∧
v
∈
U
→
v
p
∈
𝒫
X
9
8
ralrimiva
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
→
∀
v
∈
U
v
p
∈
𝒫
X
10
eqid
⊢
v
∈
U
⟼
v
p
=
v
∈
U
⟼
v
p
11
10
rnmptss
⊢
∀
v
∈
U
v
p
∈
𝒫
X
→
ran
⁡
v
∈
U
⟼
v
p
⊆
𝒫
X
12
9
11
syl
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
→
ran
⁡
v
∈
U
⟼
v
p
⊆
𝒫
X
13
mptexg
⊢
U
∈
UnifOn
⁡
X
→
v
∈
U
⟼
v
p
∈
V
14
rnexg
⊢
v
∈
U
⟼
v
p
∈
V
→
ran
⁡
v
∈
U
⟼
v
p
∈
V
15
elpwg
⊢
ran
⁡
v
∈
U
⟼
v
p
∈
V
→
ran
⁡
v
∈
U
⟼
v
p
∈
𝒫
𝒫
X
↔
ran
⁡
v
∈
U
⟼
v
p
⊆
𝒫
X
16
13
14
15
3syl
⊢
U
∈
UnifOn
⁡
X
→
ran
⁡
v
∈
U
⟼
v
p
∈
𝒫
𝒫
X
↔
ran
⁡
v
∈
U
⟼
v
p
⊆
𝒫
X
17
16
adantr
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
→
ran
⁡
v
∈
U
⟼
v
p
∈
𝒫
𝒫
X
↔
ran
⁡
v
∈
U
⟼
v
p
⊆
𝒫
X
18
12
17
mpbird
⊢
U
∈
UnifOn
⁡
X
∧
p
∈
X
→
ran
⁡
v
∈
U
⟼
v
p
∈
𝒫
𝒫
X
19
18
1
fmptd
⊢
U
∈
UnifOn
⁡
X
→
N
:
X
⟶
𝒫
𝒫
X