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	⊢ ◡ ( 𝐴 ∘ ◡ 𝐵 ) = ( 𝐵 ∘ ◡ 𝐴 )