Description: Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | cofunex2g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvexg | |
|
2 | cofunexg | |
|
3 | 1 2 | sylan2 | |
4 | cnvco | |
|
5 | cocnvcnv2 | |
|
6 | cocnvcnv1 | |
|
7 | 4 5 6 | 3eqtrri | |
8 | cnvexg | |
|
9 | 7 8 | eqeltrid | |
10 | 3 9 | syl | |
11 | 10 | ancoms | |