rnco

Description: The range of the composition of two classes. (Contributed by NM, 12-Dec-2006) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	rnco	$⊢ ran (A \circ B) = ran ({A ↾}_{ran B})$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	brco	$⊢ x (A \circ B) y \leftrightarrow \exists z (x B z \land z A y)$
4	3	exbii	$⊢ \exists x x (A \circ B) y \leftrightarrow \exists x \exists z (x B z \land z A y)$
5		excom	$⊢ \exists x \exists z (x B z \land z A y) \leftrightarrow \exists z \exists x (x B z \land z A y)$
6		vex	$⊢ z \in V$
7	6	elrn	$⊢ z \in ran B \leftrightarrow \exists x x B z$
8	7	anbi1i	$⊢ (z \in ran B \land z A y) \leftrightarrow (\exists x x B z \land z A y)$
9	2	brresi	$⊢ z ({A ↾}_{ran B}) y \leftrightarrow (z \in ran B \land z A y)$
10		19.41v	$⊢ \exists x (x B z \land z A y) \leftrightarrow (\exists x x B z \land z A y)$
11	8 9 10	3bitr4ri	$⊢ \exists x (x B z \land z A y) \leftrightarrow z ({A ↾}_{ran B}) y$
12	11	exbii	$⊢ \exists z \exists x (x B z \land z A y) \leftrightarrow \exists z z ({A ↾}_{ran B}) y$
13	4 5 12	3bitri	$⊢ \exists x x (A \circ B) y \leftrightarrow \exists z z ({A ↾}_{ran B}) y$
14	2	elrn	$⊢ y \in ran (A \circ B) \leftrightarrow \exists x x (A \circ B) y$
15	2	elrn	$⊢ y \in ran ({A ↾}_{ran B}) \leftrightarrow \exists z z ({A ↾}_{ran B}) y$
16	13 14 15	3bitr4i	$⊢ y \in ran (A \circ B) \leftrightarrow y \in ran ({A ↾}_{ran B})$
17	16	eqriv	$⊢ ran (A \circ B) = ran ({A ↾}_{ran B})$

Metamath Proof Explorer