idrefALT

Description: Alternate proof of idref not relying on definitions related to functions. 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) (Proof shortened by BJ, 28-Aug-2022) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfss2	$⊢ {I ↾}_{A} \subseteq R \leftrightarrow \forall y (y \in ({I ↾}_{A}) \to y \in R)$
2		elrid	$⊢ y \in ({I ↾}_{A}) \leftrightarrow \exists x \in A y = ⟨x, x⟩$
3	2	imbi1i	$⊢ (y \in ({I ↾}_{A}) \to y \in R) \leftrightarrow (\exists x \in A y = ⟨x, x⟩ \to y \in R)$
4		r19.23v	$⊢ \forall x \in A (y = ⟨x, x⟩ \to y \in R) \leftrightarrow (\exists x \in A y = ⟨x, x⟩ \to y \in R)$
5		eleq1	$⊢ y = ⟨x, x⟩ \to (y \in R \leftrightarrow ⟨x, x⟩ \in R)$
6		df-br	$⊢ x R x \leftrightarrow ⟨x, x⟩ \in R$
7	5 6	syl6bbr	$⊢ y = ⟨x, x⟩ \to (y \in R \leftrightarrow x R x)$
8	7	pm5.74i	$⊢ (y = ⟨x, x⟩ \to y \in R) \leftrightarrow (y = ⟨x, x⟩ \to x R x)$
9	8	ralbii	$⊢ \forall x \in A (y = ⟨x, x⟩ \to y \in R) \leftrightarrow \forall x \in A (y = ⟨x, x⟩ \to x R x)$
10	3 4 9	3bitr2i	$⊢ (y \in ({I ↾}_{A}) \to y \in R) \leftrightarrow \forall x \in A (y = ⟨x, x⟩ \to x R x)$
11	10	albii	$⊢ \forall y (y \in ({I ↾}_{A}) \to y \in R) \leftrightarrow \forall y \forall x \in A (y = ⟨x, x⟩ \to x R x)$
12		ralcom4	$⊢ \forall x \in A \forall y (y = ⟨x, x⟩ \to x R x) \leftrightarrow \forall y \forall x \in A (y = ⟨x, x⟩ \to x R x)$
13		opex	$⊢ ⟨x, x⟩ \in V$
14		biidd	$⊢ y = ⟨x, x⟩ \to (x R x \leftrightarrow x R x)$
15	13 14	ceqsalv	$⊢ \forall y (y = ⟨x, x⟩ \to x R x) \leftrightarrow x R x$
16	15	ralbii	$⊢ \forall x \in A \forall y (y = ⟨x, x⟩ \to x R x) \leftrightarrow \forall x \in A x R x$
17	11 12 16	3bitr2i	$⊢ \forall y (y \in ({I ↾}_{A}) \to y \in R) \leftrightarrow \forall x \in A x R x$
18	1 17	bitri	$⊢ {I ↾}_{A} \subseteq R \leftrightarrow \forall x \in A x R x$

Metamath Proof Explorer

Theorem idrefALT

Proof