Metamath Proof Explorer

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