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	$$⊢\left(A\in V\wedge \mathrm{Fun}{B}^{-1}\right)\to A\circ B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cnvexg	$$⊢A\in V\to A^{-1}\in \mathrm{V}$$
2		cofunexg	$$⊢\left(\mathrm{Fun}{B}^{-1}\wedge A^{-1}\in \mathrm{V}\right)\to B^{-1}\circ A^{-1}\in \mathrm{V}$$
3	1 2	sylan2	$$⊢\left(\mathrm{Fun}{B}^{-1}\wedge A\in V\right)\to B^{-1}\circ A^{-1}\in \mathrm{V}$$
4		cnvco	$$⊢{\left(B^{-1}\circ A^{-1}\right)}^{-1}={A^{-1}}^{-1}\circ {B^{-1}}^{-1}$$
5		cocnvcnv2	$$⊢{A^{-1}}^{-1}\circ {B^{-1}}^{-1}={A^{-1}}^{-1}\circ B$$
6		cocnvcnv1	$$⊢{A^{-1}}^{-1}\circ B=A\circ B$$
7	4 5 6	3eqtrri	$$⊢A\circ B={\left(B^{-1}\circ A^{-1}\right)}^{-1}$$
8		cnvexg	$$⊢B^{-1}\circ A^{-1}\in \mathrm{V}\to {\left(B^{-1}\circ A^{-1}\right)}^{-1}\in \mathrm{V}$$
9	7 8	eqeltrid	$$⊢B^{-1}\circ A^{-1}\in \mathrm{V}\to A\circ B\in \mathrm{V}$$
10	3 9	syl	$$⊢\left(\mathrm{Fun}{B}^{-1}\wedge A\in V\right)\to A\circ B\in \mathrm{V}$$
11	10	ancoms	$$⊢\left(A\in V\wedge \mathrm{Fun}{B}^{-1}\right)\to A\circ B\in \mathrm{V}$$