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

Metamath Proof Explorer

Theorem cnvco

Description: Distributive law of converse over class composition. Theorem 26 of Suppes p. 64. (Contributed by NM, 19-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion cnvco ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )

Proof

Step Hyp Ref Expression
1 exancom ⊢ ( ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 𝐴 𝑦 ∧ 𝑥 𝐵 𝑧 ) )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 brco ⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
5 vex ⊢ 𝑧 ∈ V
6 3 5 brcnv ⊢ ( 𝑦 ◡ 𝐴 𝑧 ↔ 𝑧 𝐴 𝑦 )
7 5 2 brcnv ⊢ ( 𝑧 ◡ 𝐵 𝑥 ↔ 𝑥 𝐵 𝑧 )
8 6 7 anbi12i ⊢ ( ( 𝑦 ◡ 𝐴 𝑧 ∧ 𝑧 ◡ 𝐵 𝑥 ) ↔ ( 𝑧 𝐴 𝑦 ∧ 𝑥 𝐵 𝑧 ) )
9 8 exbii ⊢ ( ∃ 𝑧 ( 𝑦 ◡ 𝐴 𝑧 ∧ 𝑧 ◡ 𝐵 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 𝐴 𝑦 ∧ 𝑥 𝐵 𝑧 ) )
10 1 4 9 3bitr4i ⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑦 ◡ 𝐴 𝑧 ∧ 𝑧 ◡ 𝐵 𝑥 ) )
11 10 opabbii ⊢ { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ∃ 𝑧 ( 𝑦 ◡ 𝐴 𝑧 ∧ 𝑧 ◡ 𝐵 𝑥 ) }
12 df-cnv ⊢ ◡ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 }
13 df-co ⊢ ( ◡ 𝐵 ∘ ◡ 𝐴 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ∃ 𝑧 ( 𝑦 ◡ 𝐴 𝑧 ∧ 𝑧 ◡ 𝐵 𝑥 ) }
14 11 12 13 3eqtr4i ⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )