Description: Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | cofunexg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relco | |
|
2 | relssdmrn | |
|
3 | 1 2 | ax-mp | |
4 | dmcoss | |
|
5 | dmexg | |
|
6 | ssexg | |
|
7 | 4 5 6 | sylancr | |
8 | 7 | adantl | |
9 | rnco | |
|
10 | rnexg | |
|
11 | resfunexg | |
|
12 | 10 11 | sylan2 | |
13 | rnexg | |
|
14 | 12 13 | syl | |
15 | 9 14 | eqeltrid | |
16 | 8 15 | xpexd | |
17 | ssexg | |
|
18 | 3 16 17 | sylancr | |