Theorem dmco

Description: The domain of a composition. Exercise 27 of Enderton p. 53. (Contributed by NM, 4-Feb-2004)

	Ref	Expression
Assertion	dmco	⊢ dom ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 “ dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfdm4	⊢ dom ( 𝐴 ∘ 𝐵 ) = ran ◡ ( 𝐴 ∘ 𝐵 )
2		cnvco	⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )
3	2	rneqi	⊢ ran ◡ ( 𝐴 ∘ 𝐵 ) = ran ( ◡ 𝐵 ∘ ◡ 𝐴 )
4		rnco2	⊢ ran ( ◡ 𝐵 ∘ ◡ 𝐴 ) = ( ◡ 𝐵 “ ran ◡ 𝐴 )
5		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
6	5	imaeq2i	⊢ ( ◡ 𝐵 “ dom 𝐴 ) = ( ◡ 𝐵 “ ran ◡ 𝐴 )
7	4 6	eqtr4i	⊢ ran ( ◡ 𝐵 ∘ ◡ 𝐴 ) = ( ◡ 𝐵 “ dom 𝐴 )
8	1 3 7	3eqtri	⊢ dom ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 “ dom 𝐴 )