This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ◡ ◡ 𝐴 = ( 𝐴 ∩ ( V × V ) )

Proof

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