coexg

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

		Ref	Expression
	Assertion	coexg	$⊢ (A \in V \land B \in W) \to A \circ B \in V$

Step	Hyp	Ref	Expression
1		cossxp	$⊢ A \circ B \subseteq dom B \times ran A$
2		dmexg	$⊢ B \in W \to dom B \in V$
3		rnexg	$⊢ A \in V \to ran A \in V$
4		xpexg	$⊢ (dom B \in V \land ran A \in V) \to dom B \times ran A \in V$
5	2 3 4	syl2anr	$⊢ (A \in V \land B \in W) \to dom B \times ran A \in V$
6		ssexg	$⊢ (A \circ B \subseteq dom B \times ran A \land dom B \times ran A \in V) \to A \circ B \in V$
7	1 5 6	sylancr	$⊢ (A \in V \land B \in W) \to A \circ B \in V$

Metamath Proof Explorer