Metamath Proof Explorer

Theorem ustref

Description: Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ustref ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ A ∈ X → A V A

Proof

Step Hyp Ref Expression
1 eqid ⊢ A = A
2 resieq ⊢ A ∈ X ∧ A ∈ X → A I ↾ X A ↔ A = A
3 1 2 mpbiri ⊢ A ∈ X ∧ A ∈ X → A I ↾ X A
4 3 anidms ⊢ A ∈ X → A I ↾ X A
5 4 3ad2ant3 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ A ∈ X → A I ↾ X A
6 ustdiag ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → I ↾ X ⊆ V
7 6 ssbrd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → A I ↾ X A → A V A
8 7 3adant3 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ A ∈ X → A I ↾ X A → A V A
9 5 8 mpd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ A ∈ X → A V A