# Metamath Proof Explorer

## Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis fmpt.1 ${⊢}{F}=\left({x}\in {A}⟼{C}\right)$
Assertion fmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}↔{F}:{A}⟶{B}$

### Proof

Step Hyp Ref Expression
1 fmpt.1 ${⊢}{F}=\left({x}\in {A}⟼{C}\right)$
2 1 fnmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\to {F}Fn{A}$
3 1 rnmpt ${⊢}\mathrm{ran}{F}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\right\}$
4 r19.29 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({C}\in {B}\wedge {y}={C}\right)$
5 eleq1 ${⊢}{y}={C}\to \left({y}\in {B}↔{C}\in {B}\right)$
6 5 biimparc ${⊢}\left({C}\in {B}\wedge {y}={C}\right)\to {y}\in {B}$
7 6 rexlimivw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({C}\in {B}\wedge {y}={C}\right)\to {y}\in {B}$
8 4 7 syl ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\wedge \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\right)\to {y}\in {B}$
9 8 ex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\to {y}\in {B}\right)$
10 9 abssdv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\right\}\subseteq {B}$
11 3 10 eqsstrid ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\to \mathrm{ran}{F}\subseteq {B}$
12 df-f ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
13 2 11 12 sylanbrc ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}\to {F}:{A}⟶{B}$
14 1 mptpreima ${⊢}{{F}}^{-1}\left[{B}\right]=\left\{{x}\in {A}|{C}\in {B}\right\}$
15 fimacnv ${⊢}{F}:{A}⟶{B}\to {{F}}^{-1}\left[{B}\right]={A}$
16 14 15 syl5reqr ${⊢}{F}:{A}⟶{B}\to {A}=\left\{{x}\in {A}|{C}\in {B}\right\}$
17 rabid2 ${⊢}{A}=\left\{{x}\in {A}|{C}\in {B}\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}$
18 16 17 sylib ${⊢}{F}:{A}⟶{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}$
19 13 18 impbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {B}↔{F}:{A}⟶{B}$