Metamath Proof Explorer

Theorem coexg

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

Ref Expression
Assertion coexg ⊢ A ∈ V ∧ B ∈ W → A ∘ B ∈ V

Proof

Step Hyp Ref Expression
1 cossxp ⊢ A ∘ B ⊆ dom ⁡ B × ran ⁡ A
2 dmexg ⊢ B ∈ W → dom ⁡ B ∈ V
3 rnexg ⊢ A ∈ V → ran ⁡ A ∈ V
4 xpexg ⊢ dom ⁡ B ∈ V ∧ ran ⁡ A ∈ V → dom ⁡ B × ran ⁡ A ∈ V
5 2 3 4 syl2anr ⊢ A ∈ V ∧ B ∈ W → dom ⁡ B × ran ⁡ A ∈ V
6 ssexg ⊢ A ∘ B ⊆ dom ⁡ B × ran ⁡ A ∧ dom ⁡ B × ran ⁡ A ∈ V → A ∘ B ∈ V
7 1 5 6 sylancr ⊢ A ∈ V ∧ B ∈ W → A ∘ B ∈ V