Metamath Proof Explorer

Theorem cnvcnv

Description: The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003) (Proof shortened by BJ, 26-Nov-2021)

		Ref	Expression
	Assertion	cnvcnv	$⊢ {A^{-1}}^{-1} = A \cap (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		cnvin	$⊢ {(A^{-1} \cap {(V \times V)}^{-1})}^{-1} = {A^{-1}}^{-1} \cap {(V \times V)}^{-1}^{-1}$
2		cnvin	$⊢ {(A \cap (V \times V))}^{-1} = A^{-1} \cap {(V \times V)}^{-1}$
3	2	cnveqi	$⊢ {(A \cap (V \times V))}^{-1}^{-1} = {(A^{-1} \cap {(V \times V)}^{-1})}^{-1}$
4		relcnv	$⊢ Rel {A^{-1}}^{-1}$
5		df-rel	$⊢ Rel {A^{-1}}^{-1} \leftrightarrow {A^{-1}}^{-1} \subseteq V \times V$
6	4 5	mpbi	$⊢ {A^{-1}}^{-1} \subseteq V \times V$
7		relxp	$⊢ Rel (V \times V)$
8		dfrel2	$⊢ Rel (V \times V) \leftrightarrow {(V \times V)}^{-1}^{-1} = V \times V$
9	7 8	mpbi	$⊢ {(V \times V)}^{-1}^{-1} = V \times V$
10	6 9	sseqtrri	$⊢ {A^{-1}}^{-1} \subseteq {(V \times V)}^{-1}^{-1}$
11		dfss	$⊢ {A^{-1}}^{-1} \subseteq {(V \times V)}^{-1}^{-1} \leftrightarrow {A^{-1}}^{-1} = {A^{-1}}^{-1} \cap {(V \times V)}^{-1}^{-1}$
12	10 11	mpbi	$⊢ {A^{-1}}^{-1} = {A^{-1}}^{-1} \cap {(V \times V)}^{-1}^{-1}$
13	1 3 12	3eqtr4ri	$⊢ {A^{-1}}^{-1} = {(A \cap (V \times V))}^{-1}^{-1}$
14		relinxp	$⊢ Rel (A \cap (V \times V))$
15		dfrel2	$⊢ Rel (A \cap (V \times V)) \leftrightarrow {(A \cap (V \times V))}^{-1}^{-1} = A \cap (V \times V)$
16	14 15	mpbi	$⊢ {(A \cap (V \times V))}^{-1}^{-1} = A \cap (V \times V)$
17	13 16	eqtri	$⊢ {A^{-1}}^{-1} = A \cap (V \times V)$