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 ∩ V × V

Proof

Step Hyp Ref Expression
1 cnvin ⊢ A -1 ∩ V × V -1 -1 = A -1 -1 ∩ V × V -1 -1
2 cnvin ⊢ A ∩ V × V -1 = A -1 ∩ V × V -1
3 2 cnveqi ⊢ A ∩ V × V -1 -1 = A -1 ∩ V × V -1 -1
4 relcnv ⊢ Rel ⁡ A -1 -1
5 df-rel ⊢ Rel ⁡ A -1 -1 ↔ A -1 -1 ⊆ V × V
6 4 5 mpbi ⊢ A -1 -1 ⊆ V × V
7 relxp ⊢ Rel ⁡ V × V
8 dfrel2 ⊢ Rel ⁡ V × V ↔ V × V -1 -1 = V × V
9 7 8 mpbi ⊢ V × V -1 -1 = V × V
10 6 9 sseqtrri ⊢ A -1 -1 ⊆ V × V -1 -1
11 dfss ⊢ A -1 -1 ⊆ V × V -1 -1 ↔ A -1 -1 = A -1 -1 ∩ V × V -1 -1
12 10 11 mpbi ⊢ A -1 -1 = A -1 -1 ∩ V × V -1 -1
13 1 3 12 3eqtr4ri ⊢ A -1 -1 = A ∩ V × V -1 -1
14 relinxp ⊢ Rel ⁡ A ∩ V × V
15 dfrel2 ⊢ Rel ⁡ A ∩ V × V ↔ A ∩ V × V -1 -1 = A ∩ V × V
16 14 15 mpbi ⊢ A ∩ V × V -1 -1 = A ∩ V × V
17 13 16 eqtri ⊢ A -1 -1 = A ∩ V × V