Metamath Proof Explorer

Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

		Ref	Expression
	Assertion	idref	$⊢ {I ↾}_{A} \subseteq R \leftrightarrow \forall x \in A x R x$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in A ⟼ ⟨x, x⟩) = (x \in A ⟼ ⟨x, x⟩)$
2	1	fmpt	$⊢ \forall x \in A ⟨x, x⟩ \in R \leftrightarrow (x \in A ⟼ ⟨x, x⟩) : A ⟶ R$
3		opex	$⊢ ⟨x, x⟩ \in V$
4	3 1	fnmpti	$⊢ (x \in A ⟼ ⟨x, x⟩) Fn A$
5		df-f	$⊢ (x \in A ⟼ ⟨x, x⟩) : A ⟶ R \leftrightarrow ((x \in A ⟼ ⟨x, x⟩) Fn A \land ran (x \in A ⟼ ⟨x, x⟩) \subseteq R)$
6	4 5	mpbiran	$⊢ (x \in A ⟼ ⟨x, x⟩) : A ⟶ R \leftrightarrow ran (x \in A ⟼ ⟨x, x⟩) \subseteq R$
7	2 6	bitri	$⊢ \forall x \in A ⟨x, x⟩ \in R \leftrightarrow ran (x \in A ⟼ ⟨x, x⟩) \subseteq R$
8		df-br	$⊢ x R x \leftrightarrow ⟨x, x⟩ \in R$
9	8	ralbii	$⊢ \forall x \in A x R x \leftrightarrow \forall x \in A ⟨x, x⟩ \in R$
10		mptresid	$⊢ {I ↾}_{A} = (x \in A ⟼ x)$
11		vex	$⊢ x \in V$
12	11	fnasrn	$⊢ (x \in A ⟼ x) = ran (x \in A ⟼ ⟨x, x⟩)$
13	10 12	eqtri	$⊢ {I ↾}_{A} = ran (x \in A ⟼ ⟨x, x⟩)$
14	13	sseq1i	$⊢ {I ↾}_{A} \subseteq R \leftrightarrow ran (x \in A ⟼ ⟨x, x⟩) \subseteq R$
15	7 9 14	3bitr4ri	$⊢ {I ↾}_{A} \subseteq R \leftrightarrow \forall x \in A x R x$