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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Fun ◡ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cnvexg	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )
2		cofunexg	⊢ ( ( Fun ◡ 𝐵 ∧ ◡ 𝐴 ∈ V ) → ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
3	1 2	sylan2	⊢ ( ( Fun ◡ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
4		cnvco	⊢ ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 ) = ( ◡ ◡ 𝐴 ∘ ◡ ◡ 𝐵 )
5		cocnvcnv2	⊢ ( ◡ ◡ 𝐴 ∘ ◡ ◡ 𝐵 ) = ( ◡ ◡ 𝐴 ∘ 𝐵 )
6		cocnvcnv1	⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )
7	4 5 6	3eqtrri	⊢ ( 𝐴 ∘ 𝐵 ) = ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 )
8		cnvexg	⊢ ( ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V → ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
9	7 8	eqeltrid	⊢ ( ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V → ( 𝐴 ∘ 𝐵 ) ∈ V )
10	3 9	syl	⊢ ( ( Fun ◡ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )
11	10	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Fun ◡ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )