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