Metamath Proof Explorer

Theorem mapsnd

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses mapsnd.1 ${⊢}{\phi }\to {A}\in {V}$
mapsnd.2 ${⊢}{\phi }\to {B}\in {W}$
Assertion mapsnd ${⊢}{\phi }\to {{A}}^{\left\{{B}\right\}}=\left\{{f}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\right\}$

Proof

Step Hyp Ref Expression
1 mapsnd.1 ${⊢}{\phi }\to {A}\in {V}$
2 mapsnd.2 ${⊢}{\phi }\to {B}\in {W}$
3 snex ${⊢}\left\{{B}\right\}\in \mathrm{V}$
4 3 a1i ${⊢}{\phi }\to \left\{{B}\right\}\in \mathrm{V}$
5 1 4 elmapd ${⊢}{\phi }\to \left({f}\in \left({{A}}^{\left\{{B}\right\}}\right)↔{f}:\left\{{B}\right\}⟶{A}\right)$
6 ffn ${⊢}{f}:\left\{{B}\right\}⟶{A}\to {f}Fn\left\{{B}\right\}$
7 snidg ${⊢}{B}\in {W}\to {B}\in \left\{{B}\right\}$
8 2 7 syl ${⊢}{\phi }\to {B}\in \left\{{B}\right\}$
9 fneu ${⊢}\left({f}Fn\left\{{B}\right\}\wedge {B}\in \left\{{B}\right\}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}{B}{f}{y}$
10 6 8 9 syl2anr ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}{B}{f}{y}$
11 euabsn ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{B}{f}{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{B}{f}{y}\right\}=\left\{{y}\right\}$
12 frel ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \mathrm{Rel}{f}$
13 relimasn ${⊢}\mathrm{Rel}{f}\to {f}\left[\left\{{B}\right\}\right]=\left\{{y}|{B}{f}{y}\right\}$
14 12 13 syl ${⊢}{f}:\left\{{B}\right\}⟶{A}\to {f}\left[\left\{{B}\right\}\right]=\left\{{y}|{B}{f}{y}\right\}$
15 imadmrn ${⊢}{f}\left[\mathrm{dom}{f}\right]=\mathrm{ran}{f}$
16 fdm ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \mathrm{dom}{f}=\left\{{B}\right\}$
17 16 imaeq2d ${⊢}{f}:\left\{{B}\right\}⟶{A}\to {f}\left[\mathrm{dom}{f}\right]={f}\left[\left\{{B}\right\}\right]$
18 15 17 syl5reqr ${⊢}{f}:\left\{{B}\right\}⟶{A}\to {f}\left[\left\{{B}\right\}\right]=\mathrm{ran}{f}$
19 14 18 eqtr3d ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left\{{y}|{B}{f}{y}\right\}=\mathrm{ran}{f}$
20 19 eqeq1d ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left(\left\{{y}|{B}{f}{y}\right\}=\left\{{y}\right\}↔\mathrm{ran}{f}=\left\{{y}\right\}\right)$
21 20 exbidv ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{y}|{B}{f}{y}\right\}=\left\{{y}\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{f}=\left\{{y}\right\}\right)$
22 11 21 syl5bb ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}{B}{f}{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{f}=\left\{{y}\right\}\right)$
23 22 adantl ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}{B}{f}{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{f}=\left\{{y}\right\}\right)$
24 10 23 mpbid ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{f}=\left\{{y}\right\}$
25 frn ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \mathrm{ran}{f}\subseteq {A}$
26 25 sseld ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left({y}\in \mathrm{ran}{f}\to {y}\in {A}\right)$
27 vsnid ${⊢}{y}\in \left\{{y}\right\}$
28 eleq2 ${⊢}\mathrm{ran}{f}=\left\{{y}\right\}\to \left({y}\in \mathrm{ran}{f}↔{y}\in \left\{{y}\right\}\right)$
29 27 28 mpbiri ${⊢}\mathrm{ran}{f}=\left\{{y}\right\}\to {y}\in \mathrm{ran}{f}$
30 26 29 impel ${⊢}\left({f}:\left\{{B}\right\}⟶{A}\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {y}\in {A}$
31 30 adantll ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {y}\in {A}$
32 ffrn ${⊢}{f}:\left\{{B}\right\}⟶{A}\to {f}:\left\{{B}\right\}⟶\mathrm{ran}{f}$
33 feq3 ${⊢}\mathrm{ran}{f}=\left\{{y}\right\}\to \left({f}:\left\{{B}\right\}⟶\mathrm{ran}{f}↔{f}:\left\{{B}\right\}⟶\left\{{y}\right\}\right)$
34 32 33 syl5ibcom ${⊢}{f}:\left\{{B}\right\}⟶{A}\to \left(\mathrm{ran}{f}=\left\{{y}\right\}\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}\right)$
35 34 imp ${⊢}\left({f}:\left\{{B}\right\}⟶{A}\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}$
36 35 adantll ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}$
37 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {B}\in {W}$
38 vex ${⊢}{y}\in \mathrm{V}$
39 fsng ${⊢}\left({B}\in {W}\wedge {y}\in \mathrm{V}\right)\to \left({f}:\left\{{B}\right\}⟶\left\{{y}\right\}↔{f}=\left\{⟨{B},{y}⟩\right\}\right)$
40 37 38 39 sylancl ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to \left({f}:\left\{{B}\right\}⟶\left\{{y}\right\}↔{f}=\left\{⟨{B},{y}⟩\right\}\right)$
41 36 40 mpbid ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to {f}=\left\{⟨{B},{y}⟩\right\}$
42 31 41 jca ${⊢}\left(\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\wedge \mathrm{ran}{f}=\left\{{y}\right\}\right)\to \left({y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)$
43 42 ex ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \left(\mathrm{ran}{f}=\left\{{y}\right\}\to \left({y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\right)$
44 43 eximdv ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{f}=\left\{{y}\right\}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\right)$
45 24 44 mpd ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)$
46 df-rex ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)$
47 45 46 sylibr ${⊢}\left({\phi }\wedge {f}:\left\{{B}\right\}⟶{A}\right)\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}$
48 47 ex ${⊢}{\phi }\to \left({f}:\left\{{B}\right\}⟶{A}\to \exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\right)$
49 f1osng ${⊢}\left({B}\in {W}\wedge {y}\in \mathrm{V}\right)\to \left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}$
50 2 38 49 sylancl ${⊢}{\phi }\to \left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}$
51 50 adantr ${⊢}\left({\phi }\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to \left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}$
52 f1oeq1 ${⊢}{f}=\left\{⟨{B},{y}⟩\right\}\to \left({f}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}↔\left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}\right)$
53 52 bicomd ${⊢}{f}=\left\{⟨{B},{y}⟩\right\}\to \left(\left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}↔{f}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}\right)$
54 53 adantl ${⊢}\left({\phi }\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to \left(\left\{⟨{B},{y}⟩\right\}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}↔{f}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}\right)$
55 51 54 mpbid ${⊢}\left({\phi }\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to {f}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}$
56 f1of ${⊢}{f}:\left\{{B}\right\}\underset{1-1 onto}{⟶}\left\{{y}\right\}\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}$
57 55 56 syl ${⊢}\left({\phi }\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}$
58 57 3adant2 ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to {f}:\left\{{B}\right\}⟶\left\{{y}\right\}$
59 snssi ${⊢}{y}\in {A}\to \left\{{y}\right\}\subseteq {A}$
60 59 3ad2ant2 ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to \left\{{y}\right\}\subseteq {A}$
61 58 60 fssd ${⊢}\left({\phi }\wedge {y}\in {A}\wedge {f}=\left\{⟨{B},{y}⟩\right\}\right)\to {f}:\left\{{B}\right\}⟶{A}$
62 61 rexlimdv3a ${⊢}{\phi }\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\to {f}:\left\{{B}\right\}⟶{A}\right)$
63 48 62 impbid ${⊢}{\phi }\to \left({f}:\left\{{B}\right\}⟶{A}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\right)$
64 5 63 bitrd ${⊢}{\phi }\to \left({f}\in \left({{A}}^{\left\{{B}\right\}}\right)↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\right)$
65 64 abbi2dv ${⊢}{\phi }\to {{A}}^{\left\{{B}\right\}}=\left\{{f}|\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}=\left\{⟨{B},{y}⟩\right\}\right\}$