relmptopab

Description: Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	relmptopab.1	$⊢ F = (x \in A ⟼ \{⟨y, z⟩ \| φ\})$
	Assertion	relmptopab	$⊢ Rel F (B)$

Proof

Step	Hyp	Ref	Expression
1		relmptopab.1	$⊢ F = (x \in A ⟼ \{⟨y, z⟩ \| φ\})$
2	1	fvmptss	$⊢ \forall x \in A \{⟨y, z⟩ \| φ\} \subseteq V \times V \to F (B) \subseteq V \times V$
3		relopab	$⊢ Rel \{⟨y, z⟩ \| φ\}$
4		df-rel	$⊢ Rel \{⟨y, z⟩ \| φ\} \leftrightarrow \{⟨y, z⟩ \| φ\} \subseteq V \times V$
5	3 4	mpbi	$⊢ \{⟨y, z⟩ \| φ\} \subseteq V \times V$
6	5	a1i	$⊢ x \in A \to \{⟨y, z⟩ \| φ\} \subseteq V \times V$
7	2 6	mprg	$⊢ F (B) \subseteq V \times V$
8		df-rel	$⊢ Rel F (B) \leftrightarrow F (B) \subseteq V \times V$
9	7 8	mpbir	$⊢ Rel F (B)$

Metamath Proof Explorer

Theorem relmptopab

Proof