# Metamath Proof Explorer

## Theorem 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}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
Assertion mpofun ${⊢}\mathrm{Fun}{F}$

### Proof

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