Theorem cofunexg

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

	Ref	Expression
Assertion	cofunexg	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
2		relssdmrn	⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) )
3	1 2	ax-mp	⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) )
4		dmcoss	⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵
5		dmexg	⊢ ( 𝐵 ∈ 𝐶 → dom 𝐵 ∈ V )
6		ssexg	⊢ ( ( dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 ∧ dom 𝐵 ∈ V ) → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
7	4 5 6	sylancr	⊢ ( 𝐵 ∈ 𝐶 → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
8	7	adantl	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
9		rnco	⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )
10		rnexg	⊢ ( 𝐵 ∈ 𝐶 → ran 𝐵 ∈ V )
11		resfunexg	⊢ ( ( Fun 𝐴 ∧ ran 𝐵 ∈ V ) → ( 𝐴 ↾ ran 𝐵 ) ∈ V )
12	10 11	sylan2	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ ran 𝐵 ) ∈ V )
13		rnexg	⊢ ( ( 𝐴 ↾ ran 𝐵 ) ∈ V → ran ( 𝐴 ↾ ran 𝐵 ) ∈ V )
14	12 13	syl	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ran ( 𝐴 ↾ ran 𝐵 ) ∈ V )
15	9 14	eqeltrid	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ran ( 𝐴 ∘ 𝐵 ) ∈ V )
16	8 15	xpexd	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ V )
17		ssexg	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∧ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ V ) → ( 𝐴 ∘ 𝐵 ) ∈ V )
18	3 16 17	sylancr	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )