Metamath Proof Explorer


Theorem dmco

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

Ref Expression
Assertion dmco domAB=B-1domA

Proof

Step Hyp Ref Expression
1 dfdm4 domAB=ranAB-1
2 cnvco AB-1=B-1A-1
3 2 rneqi ranAB-1=ranB-1A-1
4 rnco2 ranB-1A-1=B-1ranA-1
5 dfdm4 domA=ranA-1
6 5 imaeq2i B-1domA=B-1ranA-1
7 4 6 eqtr4i ranB-1A-1=B-1domA
8 1 3 7 3eqtri domAB=B-1domA