Metamath Proof Explorer

Theorem fsn

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003)

Ref Expression
Hypotheses fsn.1 ⊢A∈V
fsn.2 ⊢B∈V
Assertion fsn ⊢F:A⟶B↔F=AB

Proof

Step Hyp Ref Expression
1 fsn.1 ⊢A∈V
2 fsn.2 ⊢B∈V
3 opelf ⊢F:A⟶B∧xy∈F→x∈A∧y∈B
4 velsn ⊢x∈A↔x=A
5 velsn ⊢y∈B↔y=B
6 4 5 anbi12i ⊢x∈A∧y∈B↔x=A∧y=B
7 3 6 sylib ⊢F:A⟶B∧xy∈F→x=A∧y=B
8 7 ex ⊢F:A⟶B→xy∈F→x=A∧y=B
9 1 snid ⊢A∈A
10 feu ⊢F:A⟶B∧A∈A→∃!y∈BAy∈F
11 9 10 mpan2 ⊢F:A⟶B→∃!y∈BAy∈F
12 5 anbi1i ⊢y∈B∧Ay∈F↔y=B∧Ay∈F
13 opeq2 ⊢y=B→Ay=AB
14 13 eleq1d ⊢y=B→Ay∈F↔AB∈F
15 14 pm5.32i ⊢y=B∧Ay∈F↔y=B∧AB∈F
16 15 biancomi ⊢y=B∧Ay∈F↔AB∈F∧y=B
17 12 16 bitr2i ⊢AB∈F∧y=B↔y∈B∧Ay∈F
18 17 eubii ⊢∃!yAB∈F∧y=B↔∃!yy∈B∧Ay∈F
19 2 eueqi ⊢∃!yy=B
20 19 biantru ⊢AB∈F↔AB∈F∧∃!yy=B
21 euanv ⊢∃!yAB∈F∧y=B↔AB∈F∧∃!yy=B
22 20 21 bitr4i ⊢AB∈F↔∃!yAB∈F∧y=B
23 df-reu ⊢∃!y∈BAy∈F↔∃!yy∈B∧Ay∈F
24 18 22 23 3bitr4i ⊢AB∈F↔∃!y∈BAy∈F
25 11 24 sylibr ⊢F:A⟶B→AB∈F
26 opeq12 ⊢x=A∧y=B→xy=AB
27 26 eleq1d ⊢x=A∧y=B→xy∈F↔AB∈F
28 25 27 syl5ibrcom ⊢F:A⟶B→x=A∧y=B→xy∈F
29 8 28 impbid ⊢F:A⟶B→xy∈F↔x=A∧y=B
30 opex ⊢xy∈V
31 30 elsn ⊢xy∈AB↔xy=AB
32 1 2 opth2 ⊢xy=AB↔x=A∧y=B
33 31 32 bitr2i ⊢x=A∧y=B↔xy∈AB
34 29 33 bitrdi ⊢F:A⟶B→xy∈F↔xy∈AB
35 34 alrimivv ⊢F:A⟶B→∀x∀yxy∈F↔xy∈AB
36 frel ⊢F:A⟶B→Rel⁡F
37 1 2 relsnop ⊢Rel⁡AB
38 eqrel ⊢Rel⁡F∧Rel⁡AB→F=AB↔∀x∀yxy∈F↔xy∈AB
39 36 37 38 sylancl ⊢F:A⟶B→F=AB↔∀x∀yxy∈F↔xy∈AB
40 35 39 mpbird ⊢F:A⟶B→F=AB
41 1 2 f1osn ⊢AB:A⟶1-1 ontoB
42 f1oeq1 ⊢F=AB→F:A⟶1-1 ontoB↔AB:A⟶1-1 ontoB
43 41 42 mpbiri ⊢F=AB→F:A⟶1-1 ontoB
44 f1of ⊢F:A⟶1-1 ontoB→F:A⟶B
45 43 44 syl ⊢F=AB→F:A⟶B
46 40 45 impbii ⊢F:A⟶B↔F=AB