mpofun

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

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

Step	Hyp	Ref	Expression
1		mpofun.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		eqtr3	$⊢ (z = C \land w = C) \to z = w$
3	2	ad2ant2l	$⊢ (((x \in A \land y \in B) \land z = C) \land ((x \in A \land y \in B) \land w = C)) \to z = w$
4	3	gen2	$⊢ \forall z \forall w ((((x \in A \land y \in B) \land z = C) \land ((x \in A \land y \in B) \land w = C)) \to z = w)$
5		eqeq1	$⊢ z = w \to (z = C \leftrightarrow w = C)$
6	5	anbi2d	$⊢ z = w \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in A \land y \in B) \land w = C))$
7	6	mo4	$⊢ \exists^{*} z ((x \in A \land y \in B) \land z = C) \leftrightarrow \forall z \forall w ((((x \in A \land y \in B) \land z = C) \land ((x \in A \land y \in B) \land w = C)) \to z = w)$
8	4 7	mpbir	$⊢ \exists^{*} z ((x \in A \land y \in B) \land z = C)$
9	8	funoprab	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
10		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
11	1 10	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
12	11	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
13	9 12	mpbir	$⊢ Fun F$

Metamath Proof Explorer