# 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 \left(\mathrm{V}×\mathrm{V}\right)$

### Proof

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