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