rnmpo

Description: The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011)

		Ref	Expression
	Hypothesis	rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	rnmpo	$⊢ ran F = \{z \| \exists x \in A \exists y \in B z = C\}$

Step	Hyp	Ref	Expression
1		rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
3	1 2	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
4	3	rneqi	$⊢ ran F = ran \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
5		rnoprab2	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{z \| \exists x \in A \exists y \in B z = C\}$
6	4 5	eqtri	$⊢ ran F = \{z \| \exists x \in A \exists y \in B z = C\}$

Metamath Proof Explorer