Metamath Proof Explorer

Theorem mpofun

Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012) (Proof shortened by SN, 23-Jul-2024)

		Ref	Expression
	Hypothesis	mpofun.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	mpofun	$⊢ Fun F$

Proof

Step	Hyp	Ref	Expression
1		mpofun.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		moeq	$⊢ \exists^{*} z z = C$
3	2	moani	$⊢ \exists^{*} z ((x \in A \land y \in B) \land z = C)$
4	3	funoprab	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
5		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
6	1 5	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
7	6	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
8	4 7	mpbir	$⊢ Fun F$