Theorem coexg

Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998)

	Ref	Expression
Assertion	coexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cossxp	⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom 𝐵 × ran 𝐴 )
2		dmexg	⊢ ( 𝐵 ∈ 𝑊 → dom 𝐵 ∈ V )
3		rnexg	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )
4		xpexg	⊢ ( ( dom 𝐵 ∈ V ∧ ran 𝐴 ∈ V ) → ( dom 𝐵 × ran 𝐴 ) ∈ V )
5	2 3 4	syl2anr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( dom 𝐵 × ran 𝐴 ) ∈ V )
6		ssexg	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ ( dom 𝐵 × ran 𝐴 ) ∧ ( dom 𝐵 × ran 𝐴 ) ∈ V ) → ( 𝐴 ∘ 𝐵 ) ∈ V )
7	1 5 6	sylancr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )