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 \in UnifOn (X) \land V \in U \land A \in X) \to A V A$

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

Metamath Proof Explorer