bj-idres

Description: Alternate expression for the restricted identity relation. The advantage of that expression is to expose it as a "bounded" class, being included in the Cartesian square of the restricting class. (Contributed by BJ, 27-Dec-2023)

		Ref	Expression
	Assertion	bj-idres	$⊢ {I ↾}_{A} = I \cap (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		df-res	$⊢ {I ↾}_{A} = I \cap (A \times V)$
2		inss1	$⊢ I \cap (A \times V) \subseteq I$
3		relinxp	$⊢ Rel (I \cap (A \times V))$
4		elin	$⊢ ⟨x, y⟩ \in (I \cap (A \times V)) \leftrightarrow (⟨x, y⟩ \in I \land ⟨x, y⟩ \in (A \times V))$
5		bj-opelidb1	$⊢ ⟨x, y⟩ \in I \leftrightarrow (x \in V \land x = y)$
6	5	simprbi	$⊢ ⟨x, y⟩ \in I \to x = y$
7		opelxp1	$⊢ ⟨x, y⟩ \in (A \times V) \to x \in A$
8		simpr	$⊢ (x = y \land x \in A) \to x \in A$
9		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
10	9	biimpa	$⊢ (x = y \land x \in A) \to y \in A$
11	8 10	jca	$⊢ (x = y \land x \in A) \to (x \in A \land y \in A)$
12	6 7 11	syl2an	$⊢ (⟨x, y⟩ \in I \land ⟨x, y⟩ \in (A \times V)) \to (x \in A \land y \in A)$
13	4 12	sylbi	$⊢ ⟨x, y⟩ \in (I \cap (A \times V)) \to (x \in A \land y \in A)$
14		opelxpi	$⊢ (x \in A \land y \in A) \to ⟨x, y⟩ \in (A \times A)$
15	13 14	syl	$⊢ ⟨x, y⟩ \in (I \cap (A \times V)) \to ⟨x, y⟩ \in (A \times A)$
16	3 15	relssi	$⊢ I \cap (A \times V) \subseteq A \times A$
17	2 16	ssini	$⊢ I \cap (A \times V) \subseteq I \cap (A \times A)$
18		ssv	$⊢ A \subseteq V$
19		xpss2	$⊢ A \subseteq V \to A \times A \subseteq A \times V$
20		sslin	$⊢ A \times A \subseteq A \times V \to I \cap (A \times A) \subseteq I \cap (A \times V)$
21	18 19 20	mp2b	$⊢ I \cap (A \times A) \subseteq I \cap (A \times V)$
22	17 21	eqssi	$⊢ I \cap (A \times V) = I \cap (A \times A)$
23	1 22	eqtri	$⊢ {I ↾}_{A} = I \cap (A \times A)$

Metamath Proof Explorer

Theorem bj-idres

Proof