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

Metamath Proof Explorer

Theorem cnvco2

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

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

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ◡ ( 𝐴 ∘ ◡ 𝐵 )
2 relco ⊢ Rel ( 𝐵 ∘ ◡ 𝐴 )
3 vex ⊢ 𝑦 ∈ V
4 vex ⊢ 𝑧 ∈ V
5 3 4 brcnv ⊢ ( 𝑦 ◡ 𝐵 𝑧 ↔ 𝑧 𝐵 𝑦 )
6 vex ⊢ 𝑥 ∈ V
7 6 4 brcnv ⊢ ( 𝑥 ◡ 𝐴 𝑧 ↔ 𝑧 𝐴 𝑥 )
8 7 bicomi ⊢ ( 𝑧 𝐴 𝑥 ↔ 𝑥 ◡ 𝐴 𝑧 )
9 5 8 anbi12ci ⊢ ( ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ↔ ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) )
10 9 exbii ⊢ ( ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) ↔ ∃ 𝑧 ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) )
11 6 3 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 ∘ ◡ 𝐵 ) )
12 3 6 opelco ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) )
13 11 12 bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 ◡ 𝐵 𝑧 ∧ 𝑧 𝐴 𝑥 ) )
14 6 3 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 ∘ ◡ 𝐴 ) ↔ ∃ 𝑧 ( 𝑥 ◡ 𝐴 𝑧 ∧ 𝑧 𝐵 𝑦 ) )
15 10 13 14 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ( 𝐴 ∘ ◡ 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 ∘ ◡ 𝐴 ) )
16 1 2 15 eqrelriiv ⊢ ◡ ( 𝐴 ∘ ◡ 𝐵 ) = ( 𝐵 ∘ ◡ 𝐴 )