iss2

Description: A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019)

		Ref	Expression
	Assertion	iss2	$⊢ A \subseteq I \leftrightarrow A = I \cap (dom A \times ran A)$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in I)$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	opeldm	$⊢ ⟨x, y⟩ \in A \to x \in dom A$
5	1 4	jca2	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to (⟨x, y⟩ \in I \land x \in dom A))$
6	2 3	opelrn	$⊢ ⟨x, y⟩ \in A \to y \in ran A$
7	1 6	jca2	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to (⟨x, y⟩ \in I \land y \in ran A))$
8	5 7	jcad	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to ((⟨x, y⟩ \in I \land x \in dom A) \land (⟨x, y⟩ \in I \land y \in ran A)))$
9		anandi	$⊢ (⟨x, y⟩ \in I \land (x \in dom A \land y \in ran A)) \leftrightarrow ((⟨x, y⟩ \in I \land x \in dom A) \land (⟨x, y⟩ \in I \land y \in ran A))$
10	8 9	syl6ibr	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to (⟨x, y⟩ \in I \land (x \in dom A \land y \in ran A)))$
11		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
12	3	ideq	$⊢ x I y \leftrightarrow x = y$
13	11 12	bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow x = y$
14	2	eldm2	$⊢ x \in dom A \leftrightarrow \exists y ⟨x, y⟩ \in A$
15		opeq2	$⊢ x = y \to ⟨x, x⟩ = ⟨x, y⟩$
16	15	eleq1d	$⊢ x = y \to (⟨x, x⟩ \in A \leftrightarrow ⟨x, y⟩ \in A)$
17	16	biimprcd	$⊢ ⟨x, y⟩ \in A \to (x = y \to ⟨x, x⟩ \in A)$
18	13 17	syl5bi	$⊢ ⟨x, y⟩ \in A \to (⟨x, y⟩ \in I \to ⟨x, x⟩ \in A)$
19	1 18	sylcom	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \to ⟨x, x⟩ \in A)$
20	19	exlimdv	$⊢ A \subseteq I \to (\exists y ⟨x, y⟩ \in A \to ⟨x, x⟩ \in A)$
21	14 20	syl5bi	$⊢ A \subseteq I \to (x \in dom A \to ⟨x, x⟩ \in A)$
22	16	imbi2d	$⊢ x = y \to ((x \in dom A \to ⟨x, x⟩ \in A) \leftrightarrow (x \in dom A \to ⟨x, y⟩ \in A))$
23	21 22	syl5ibcom	$⊢ A \subseteq I \to (x = y \to (x \in dom A \to ⟨x, y⟩ \in A))$
24	23	imp	$⊢ (A \subseteq I \land x = y) \to (x \in dom A \to ⟨x, y⟩ \in A)$
25	24	adantrd	$⊢ (A \subseteq I \land x = y) \to ((x \in dom A \land y \in ran A) \to ⟨x, y⟩ \in A)$
26	25	ex	$⊢ A \subseteq I \to (x = y \to ((x \in dom A \land y \in ran A) \to ⟨x, y⟩ \in A))$
27	13 26	syl5bi	$⊢ A \subseteq I \to (⟨x, y⟩ \in I \to ((x \in dom A \land y \in ran A) \to ⟨x, y⟩ \in A))$
28	27	impd	$⊢ A \subseteq I \to ((⟨x, y⟩ \in I \land (x \in dom A \land y \in ran A)) \to ⟨x, y⟩ \in A)$
29	10 28	impbid	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \leftrightarrow (⟨x, y⟩ \in I \land (x \in dom A \land y \in ran A)))$
30		opelinxp	$⊢ ⟨x, y⟩ \in (I \cap (dom A \times ran A)) \leftrightarrow ((x \in dom A \land y \in ran A) \land ⟨x, y⟩ \in I)$
31	30	biancomi	$⊢ ⟨x, y⟩ \in (I \cap (dom A \times ran A)) \leftrightarrow (⟨x, y⟩ \in I \land (x \in dom A \land y \in ran A))$
32	29 31	bitr4di	$⊢ A \subseteq I \to (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in (I \cap (dom A \times ran A)))$
33	32	alrimivv	$⊢ A \subseteq I \to \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in (I \cap (dom A \times ran A)))$
34		reli	$⊢ Rel I$
35		relss	$⊢ A \subseteq I \to (Rel I \to Rel A)$
36	34 35	mpi	$⊢ A \subseteq I \to Rel A$
37		relinxp	$⊢ Rel (I \cap (dom A \times ran A))$
38		eqrel	$⊢ (Rel A \land Rel (I \cap (dom A \times ran A))) \to (A = I \cap (dom A \times ran A) \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in (I \cap (dom A \times ran A))))$
39	36 37 38	sylancl	$⊢ A \subseteq I \to (A = I \cap (dom A \times ran A) \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in (I \cap (dom A \times ran A))))$
40	33 39	mpbird	$⊢ A \subseteq I \to A = I \cap (dom A \times ran A)$
41		inss1	$⊢ I \cap (dom A \times ran A) \subseteq I$
42		sseq1	$⊢ A = I \cap (dom A \times ran A) \to (A \subseteq I \leftrightarrow I \cap (dom A \times ran A) \subseteq I)$
43	41 42	mpbiri	$⊢ A = I \cap (dom A \times ran A) \to A \subseteq I$
44	40 43	impbii	$⊢ A \subseteq I \leftrightarrow A = I \cap (dom A \times ran A)$

Metamath Proof Explorer

Theorem iss2

Proof