Metamath Proof Explorer


Theorem cofunex2g

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

Ref Expression
Assertion cofunex2g AVFunB-1ABV

Proof

Step Hyp Ref Expression
1 cnvexg AVA-1V
2 cofunexg FunB-1A-1VB-1A-1V
3 1 2 sylan2 FunB-1AVB-1A-1V
4 cnvco B-1A-1-1=A-1-1B-1-1
5 cocnvcnv2 A-1-1B-1-1=A-1-1B
6 cocnvcnv1 A-1-1B=AB
7 4 5 6 3eqtrri AB=B-1A-1-1
8 cnvexg B-1A-1VB-1A-1-1V
9 7 8 eqeltrid B-1A-1VABV
10 3 9 syl FunB-1AVABV
11 10 ancoms AVFunB-1ABV