dfcnv2

Description: Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018)

		Ref	Expression
	Assertion	dfcnv2	$⊢ ran R \subseteq A \to R^{-1} = ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}])$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel R^{-1}$
2		relxp	$⊢ Rel (\{x\} \times R^{-1} [\{x\}])$
3	2	rgenw	$⊢ \forall x \in A Rel (\{x\} \times R^{-1} [\{x\}])$
4		reliun	$⊢ Rel ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}]) \leftrightarrow \forall x \in A Rel (\{x\} \times R^{-1} [\{x\}])$
5	3 4	mpbir	$⊢ Rel ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}])$
6		vex	$⊢ z \in V$
7		vex	$⊢ y \in V$
8	6 7	opeldm	$⊢ ⟨z, y⟩ \in R^{-1} \to z \in dom R^{-1}$
9		df-rn	$⊢ ran R = dom R^{-1}$
10	8 9	eleqtrrdi	$⊢ ⟨z, y⟩ \in R^{-1} \to z \in ran R$
11		ssel2	$⊢ (ran R \subseteq A \land z \in ran R) \to z \in A$
12	10 11	sylan2	$⊢ (ran R \subseteq A \land ⟨z, y⟩ \in R^{-1}) \to z \in A$
13	12	ex	$⊢ ran R \subseteq A \to (⟨z, y⟩ \in R^{-1} \to z \in A)$
14	13	pm4.71rd	$⊢ ran R \subseteq A \to (⟨z, y⟩ \in R^{-1} \leftrightarrow (z \in A \land ⟨z, y⟩ \in R^{-1}))$
15	6 7	elimasn	$⊢ y \in R^{-1} [\{z\}] \leftrightarrow ⟨z, y⟩ \in R^{-1}$
16	15	anbi2i	$⊢ (z \in A \land y \in R^{-1} [\{z\}]) \leftrightarrow (z \in A \land ⟨z, y⟩ \in R^{-1})$
17	14 16	bitr4di	$⊢ ran R \subseteq A \to (⟨z, y⟩ \in R^{-1} \leftrightarrow (z \in A \land y \in R^{-1} [\{z\}]))$
18		sneq	$⊢ x = z \to \{x\} = \{z\}$
19	18	imaeq2d	$⊢ x = z \to R^{-1} [\{x\}] = R^{-1} [\{z\}]$
20	19	opeliunxp2	$⊢ ⟨z, y⟩ \in ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}]) \leftrightarrow (z \in A \land y \in R^{-1} [\{z\}])$
21	17 20	bitr4di	$⊢ ran R \subseteq A \to (⟨z, y⟩ \in R^{-1} \leftrightarrow ⟨z, y⟩ \in ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}]))$
22	1 5 21	eqrelrdv	$⊢ ran R \subseteq A \to R^{-1} = ⋃_{x \in A} (\{x\} \times R^{-1} [\{x\}])$

Metamath Proof Explorer

Theorem dfcnv2

Proof