cofunex2g

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

		Ref	Expression
	Assertion	cofunex2g	$⊢ (A \in V \land Fun B^{-1}) \to A \circ B \in V$

Step	Hyp	Ref	Expression
1		cnvexg	$⊢ A \in V \to A^{-1} \in V$
2		cofunexg	$⊢ (Fun B^{-1} \land A^{-1} \in V) \to B^{-1} \circ A^{-1} \in V$
3	1 2	sylan2	$⊢ (Fun B^{-1} \land A \in V) \to B^{-1} \circ A^{-1} \in V$
4		cnvco	$⊢ {(B^{-1} \circ A^{-1})}^{-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 = {(B^{-1} \circ A^{-1})}^{-1}$
8		cnvexg	$⊢ B^{-1} \circ A^{-1} \in V \to {(B^{-1} \circ A^{-1})}^{-1} \in V$
9	7 8	eqeltrid	$⊢ B^{-1} \circ A^{-1} \in V \to A \circ B \in V$
10	3 9	syl	$⊢ (Fun B^{-1} \land A \in V) \to A \circ B \in V$
11	10	ancoms	$⊢ (A \in V \land Fun B^{-1}) \to A \circ B \in V$

Metamath Proof Explorer