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}\in \mathrm{V}$
fsn.2 ${⊢}{B}\in \mathrm{V}$
Assertion fsn ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}$

Proof

Step Hyp Ref Expression
1 fsn.1 ${⊢}{A}\in \mathrm{V}$
2 fsn.2 ${⊢}{B}\in \mathrm{V}$
3 opelf ${⊢}\left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}\wedge ⟨{x},{y}⟩\in {F}\right)\to \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{B}\right\}\right)$
4 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
5 velsn ${⊢}{y}\in \left\{{B}\right\}↔{y}={B}$
6 4 5 anbi12i ${⊢}\left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{B}\right\}\right)↔\left({x}={A}\wedge {y}={B}\right)$
7 3 6 sylib ${⊢}\left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}\wedge ⟨{x},{y}⟩\in {F}\right)\to \left({x}={A}\wedge {y}={B}\right)$
8 7 ex ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \left(⟨{x},{y}⟩\in {F}\to \left({x}={A}\wedge {y}={B}\right)\right)$
9 1 snid ${⊢}{A}\in \left\{{A}\right\}$
10 feu ${⊢}\left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}\wedge {A}\in \left\{{A}\right\}\right)\to \exists !{y}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}⟨{A},{y}⟩\in {F}$
11 9 10 mpan2 ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \exists !{y}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}⟨{A},{y}⟩\in {F}$
12 5 anbi1i ${⊢}\left({y}\in \left\{{B}\right\}\wedge ⟨{A},{y}⟩\in {F}\right)↔\left({y}={B}\wedge ⟨{A},{y}⟩\in {F}\right)$
13 opeq2 ${⊢}{y}={B}\to ⟨{A},{y}⟩=⟨{A},{B}⟩$
14 13 eleq1d ${⊢}{y}={B}\to \left(⟨{A},{y}⟩\in {F}↔⟨{A},{B}⟩\in {F}\right)$
15 14 pm5.32i ${⊢}\left({y}={B}\wedge ⟨{A},{y}⟩\in {F}\right)↔\left({y}={B}\wedge ⟨{A},{B}⟩\in {F}\right)$
16 15 biancomi ${⊢}\left({y}={B}\wedge ⟨{A},{y}⟩\in {F}\right)↔\left(⟨{A},{B}⟩\in {F}\wedge {y}={B}\right)$
17 12 16 bitr2i ${⊢}\left(⟨{A},{B}⟩\in {F}\wedge {y}={B}\right)↔\left({y}\in \left\{{B}\right\}\wedge ⟨{A},{y}⟩\in {F}\right)$
18 17 eubii ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩\in {F}\wedge {y}={B}\right)↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{B}\right\}\wedge ⟨{A},{y}⟩\in {F}\right)$
19 2 eueqi ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}$
20 19 biantru ${⊢}⟨{A},{B}⟩\in {F}↔\left(⟨{A},{B}⟩\in {F}\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}\right)$
21 euanv ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩\in {F}\wedge {y}={B}\right)↔\left(⟨{A},{B}⟩\in {F}\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}{y}={B}\right)$
22 20 21 bitr4i ${⊢}⟨{A},{B}⟩\in {F}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩\in {F}\wedge {y}={B}\right)$
23 df-reu ${⊢}\exists !{y}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}⟨{A},{y}⟩\in {F}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left\{{B}\right\}\wedge ⟨{A},{y}⟩\in {F}\right)$
24 18 22 23 3bitr4i ${⊢}⟨{A},{B}⟩\in {F}↔\exists !{y}\in \left\{{B}\right\}\phantom{\rule{.4em}{0ex}}⟨{A},{y}⟩\in {F}$
25 11 24 sylibr ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to ⟨{A},{B}⟩\in {F}$
26 opeq12 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to ⟨{x},{y}⟩=⟨{A},{B}⟩$
27 26 eleq1d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left(⟨{x},{y}⟩\in {F}↔⟨{A},{B}⟩\in {F}\right)$
28 25 27 syl5ibrcom ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \left(\left({x}={A}\wedge {y}={B}\right)\to ⟨{x},{y}⟩\in {F}\right)$
29 8 28 impbid ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \left(⟨{x},{y}⟩\in {F}↔\left({x}={A}\wedge {y}={B}\right)\right)$
30 opex ${⊢}⟨{x},{y}⟩\in \mathrm{V}$
31 30 elsn ${⊢}⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}↔⟨{x},{y}⟩=⟨{A},{B}⟩$
32 1 2 opth2 ${⊢}⟨{x},{y}⟩=⟨{A},{B}⟩↔\left({x}={A}\wedge {y}={B}\right)$
33 31 32 bitr2i ${⊢}\left({x}={A}\wedge {y}={B}\right)↔⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}$
34 29 33 syl6bb ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \left(⟨{x},{y}⟩\in {F}↔⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}\right)$
35 34 alrimivv ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}↔⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}\right)$
36 frel ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \mathrm{Rel}{F}$
37 1 2 relsnop ${⊢}\mathrm{Rel}\left\{⟨{A},{B}⟩\right\}$
38 eqrel ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{Rel}\left\{⟨{A},{B}⟩\right\}\right)\to \left({F}=\left\{⟨{A},{B}⟩\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}↔⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}\right)\right)$
39 36 37 38 sylancl ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to \left({F}=\left\{⟨{A},{B}⟩\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}↔⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}\right)\right)$
40 35 39 mpbird ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\to {F}=\left\{⟨{A},{B}⟩\right\}$
41 1 2 f1osn ${⊢}\left\{⟨{A},{B}⟩\right\}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{B}\right\}$
42 f1oeq1 ${⊢}{F}=\left\{⟨{A},{B}⟩\right\}\to \left({F}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{B}\right\}↔\left\{⟨{A},{B}⟩\right\}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{B}\right\}\right)$
43 41 42 mpbiri ${⊢}{F}=\left\{⟨{A},{B}⟩\right\}\to {F}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{B}\right\}$
44 f1of ${⊢}{F}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{B}\right\}\to {F}:\left\{{A}\right\}⟶\left\{{B}\right\}$
45 43 44 syl ${⊢}{F}=\left\{⟨{A},{B}⟩\right\}\to {F}:\left\{{A}\right\}⟶\left\{{B}\right\}$
46 40 45 impbii ${⊢}{F}:\left\{{A}\right\}⟶\left\{{B}\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}$