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

Metamath Proof Explorer

Theorem cnvco1

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

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

Proof

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