Database
BASIC TOPOLOGY
Uniform Structures and Spaces
Uniform structures
ustelimasn
Next ⟩
ustneism
Metamath Proof Explorer
Ascii
Unicode
Theorem
ustelimasn
Description:
Any point
A
is near enough to itself.
(Contributed by
Thierry Arnoux
, 18-Nov-2017)
Ref
Expression
Assertion
ustelimasn
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
A
∈
V
A
Proof
Step
Hyp
Ref
Expression
1
simp3
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
A
∈
X
2
ustdiag
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
→
I
↾
X
⊆
V
3
2
3adant3
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
I
↾
X
⊆
V
4
opelidres
⊢
A
∈
X
→
A
A
∈
I
↾
X
↔
A
∈
X
5
4
ibir
⊢
A
∈
X
→
A
A
∈
I
↾
X
6
5
3ad2ant3
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
A
A
∈
I
↾
X
7
3
6
sseldd
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
A
A
∈
V
8
elimasng
⊢
A
∈
X
∧
A
∈
X
→
A
∈
V
A
↔
A
A
∈
V
9
8
anidms
⊢
A
∈
X
→
A
∈
V
A
↔
A
A
∈
V
10
9
biimpar
⊢
A
∈
X
∧
A
A
∈
V
→
A
∈
V
A
11
1
7
10
syl2anc
⊢
U
∈
UnifOn
⁡
X
∧
V
∈
U
∧
A
∈
X
→
A
∈
V
A