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=x∈A⟼C
Assertion fmpt ⊢∀x∈AC∈B↔F:A⟶B

Proof

Step Hyp Ref Expression
1 fmpt.1 ⊢F=x∈A⟼C
2 1 fnmpt ⊢∀x∈AC∈B→FFnA
3 1 rnmpt ⊢ran⁡F=y|∃x∈Ay=C
4 r19.29 ⊢∀x∈AC∈B∧∃x∈Ay=C→∃x∈AC∈B∧y=C
5 eleq1 ⊢y=C→y∈B↔C∈B
6 5 biimparc ⊢C∈B∧y=C→y∈B
7 6 rexlimivw ⊢∃x∈AC∈B∧y=C→y∈B
8 4 7 syl ⊢∀x∈AC∈B∧∃x∈Ay=C→y∈B
9 8 ex ⊢∀x∈AC∈B→∃x∈Ay=C→y∈B
10 9 abssdv ⊢∀x∈AC∈B→y|∃x∈Ay=C⊆B
11 3 10 eqsstrid ⊢∀x∈AC∈B→ran⁡F⊆B
12 df-f ⊢F:A⟶B↔FFnA∧ran⁡F⊆B
13 2 11 12 sylanbrc ⊢∀x∈AC∈B→F:A⟶B
14 fimacnv ⊢F:A⟶B→F-1B=A
15 1 mptpreima ⊢F-1B=x∈A|C∈B
16 14 15 eqtr3di ⊢F:A⟶B→A=x∈A|C∈B
17 rabid2 ⊢A=x∈A|C∈B↔∀x∈AC∈B
18 16 17 sylib ⊢F:A⟶B→∀x∈AC∈B
19 13 18 impbii ⊢∀x∈AC∈B↔F:A⟶B