Metamath Proof Explorer


Theorem cofunexg

Description: Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007)

Ref Expression
Assertion cofunexg FunABCABV

Proof

Step Hyp Ref Expression
1 relco RelAB
2 relssdmrn RelABABdomAB×ranAB
3 1 2 ax-mp ABdomAB×ranAB
4 dmcoss domABdomB
5 dmexg BCdomBV
6 ssexg domABdomBdomBVdomABV
7 4 5 6 sylancr BCdomABV
8 7 adantl FunABCdomABV
9 rnco ranAB=ranAranB
10 rnexg BCranBV
11 resfunexg FunAranBVAranBV
12 10 11 sylan2 FunABCAranBV
13 rnexg AranBVranAranBV
14 12 13 syl FunABCranAranBV
15 9 14 eqeltrid FunABCranABV
16 8 15 xpexd FunABCdomAB×ranABV
17 ssexg ABdomAB×ranABdomAB×ranABVABV
18 3 16 17 sylancr FunABCABV