Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mapsn Structured version   Visualization version   GIF version

Theorem mapsn 7785
 Description: The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
Hypotheses
Ref Expression
map0.1 𝐴 ∈ V
map0.2 𝐵 ∈ V
Assertion
Ref Expression
mapsn (𝐴𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Distinct variable groups:   𝑦,𝑓,𝐴   𝐵,𝑓,𝑦

Proof of Theorem mapsn
StepHypRef Expression
1 map0.1 . . . 4 𝐴 ∈ V
2 snex 4835 . . . 4 {𝐵} ∈ V
31, 2elmap 7772 . . 3 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴)
4 ffn 5958 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴𝑓 Fn {𝐵})
5 map0.2 . . . . . . . . 9 𝐵 ∈ V
65snid 4155 . . . . . . . 8 𝐵 ∈ {𝐵}
7 fneu 5909 . . . . . . . 8 ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦)
84, 6, 7sylancl 693 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → ∃!𝑦 𝐵𝑓𝑦)
9 euabsn 4205 . . . . . . . 8 (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦})
10 frel 5963 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → Rel 𝑓)
11 relimasn 5407 . . . . . . . . . . . 12 (Rel 𝑓 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
1210, 11syl 17 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
13 imadmrn 5395 . . . . . . . . . . . 12 (𝑓 “ dom 𝑓) = ran 𝑓
14 fdm 5964 . . . . . . . . . . . . 13 (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵})
1514imaeq2d 5385 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵}))
1613, 15syl5reqr 2659 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓)
1712, 16eqtr3d 2646 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → {𝑦𝐵𝑓𝑦} = ran 𝑓)
1817eqeq1d 2612 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → ({𝑦𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦}))
1918exbidv 1837 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦}))
209, 19syl5bb 271 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦}))
218, 20mpbid 221 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → ∃𝑦ran 𝑓 = {𝑦})
22 vex 3176 . . . . . . . . . . 11 𝑦 ∈ V
2322snid 4155 . . . . . . . . . 10 𝑦 ∈ {𝑦}
24 eleq2 2677 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓𝑦 ∈ {𝑦}))
2523, 24mpbiri 247 . . . . . . . . 9 (ran 𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓)
26 frn 5966 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → ran 𝑓𝐴)
2726sseld 3567 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓𝑦𝐴))
2825, 27syl5 33 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦𝐴))
29 dffn4 6034 . . . . . . . . . . . 12 (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓)
304, 29sylib 207 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}–onto→ran 𝑓)
31 fof 6028 . . . . . . . . . . 11 (𝑓:{𝐵}–onto→ran 𝑓𝑓:{𝐵}⟶ran 𝑓)
3230, 31syl 17 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}⟶ran 𝑓)
33 feq3 5941 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓𝑓:{𝐵}⟶{𝑦}))
3432, 33syl5ibcom 234 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦}))
355, 22fsn 6308 . . . . . . . . 9 (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {⟨𝐵, 𝑦⟩})
3634, 35syl6ib 240 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓 = {⟨𝐵, 𝑦⟩}))
3728, 36jcad 554 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → (𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3837eximdv 1833 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3921, 38mpd 15 . . . . 5 (𝑓:{𝐵}⟶𝐴 → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
40 df-rex 2902 . . . . 5 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} ↔ ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
4139, 40sylibr 223 . . . 4 (𝑓:{𝐵}⟶𝐴 → ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
425, 22f1osn 6088 . . . . . . . . 9 {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}
43 f1oeq1 6040 . . . . . . . . 9 (𝑓 = {⟨𝐵, 𝑦⟩} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}))
4442, 43mpbiri 247 . . . . . . . 8 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}–1-1-onto→{𝑦})
45 f1of 6050 . . . . . . . 8 (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦})
4644, 45syl 17 . . . . . . 7 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶{𝑦})
47 snssi 4280 . . . . . . 7 (𝑦𝐴 → {𝑦} ⊆ 𝐴)
48 fss 5969 . . . . . . 7 ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴)
4946, 47, 48syl2an 493 . . . . . 6 ((𝑓 = {⟨𝐵, 𝑦⟩} ∧ 𝑦𝐴) → 𝑓:{𝐵}⟶𝐴)
5049expcom 450 . . . . 5 (𝑦𝐴 → (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴))
5150rexlimiv 3009 . . . 4 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴)
5241, 51impbii 198 . . 3 (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
533, 52bitri 263 . 2 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
5453abbi2i 2725 1 (𝐴𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  {cab 2596  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  {csn 4125  ⟨cop 4131   class class class wbr 4583  dom cdm 5038  ran crn 5039   “ cima 5041  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  (class class class)co 6549   ↑𝑚 cmap 7744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746 This theorem is referenced by:  mapsnen  7920
 Copyright terms: Public domain W3C validator