# 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 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {A}\in {X}\right)\to {A}{V}{A}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{A}={A}$
2 resieq ${⊢}\left({A}\in {X}\wedge {A}\in {X}\right)\to \left({A}\left({\mathrm{I}↾}_{{X}}\right){A}↔{A}={A}\right)$
3 1 2 mpbiri ${⊢}\left({A}\in {X}\wedge {A}\in {X}\right)\to {A}\left({\mathrm{I}↾}_{{X}}\right){A}$
4 3 anidms ${⊢}{A}\in {X}\to {A}\left({\mathrm{I}↾}_{{X}}\right){A}$
5 4 3ad2ant3 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {A}\in {X}\right)\to {A}\left({\mathrm{I}↾}_{{X}}\right){A}$
6 ustdiag ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {\mathrm{I}↾}_{{X}}\subseteq {V}$
7 6 ssbrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \left({A}\left({\mathrm{I}↾}_{{X}}\right){A}\to {A}{V}{A}\right)$
8 7 3adant3 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {A}\in {X}\right)\to \left({A}\left({\mathrm{I}↾}_{{X}}\right){A}\to {A}{V}{A}\right)$
9 5 8 mpd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {A}\in {X}\right)\to {A}{V}{A}$