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

Theorem mapsn 7758
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 4826 . . . 4 {𝐵} ∈ V
31, 2elmap 7745 . . 3 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴)
4 ffn 5940 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴𝑓 Fn {𝐵})
5 map0.2 . . . . . . . . 9 𝐵 ∈ V
65snid 4150 . . . . . . . 8 𝐵 ∈ {𝐵}
7 fneu 5891 . . . . . . . 8 ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦)
84, 6, 7sylancl 692 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → ∃!𝑦 𝐵𝑓𝑦)
9 euabsn 4200 . . . . . . . 8 (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦})
10 frel 5945 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → Rel 𝑓)
11 relimasn 5390 . . . . . . . . . . . 12 (Rel 𝑓 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
1210, 11syl 17 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
13 imadmrn 5378 . . . . . . . . . . . 12 (𝑓 “ dom 𝑓) = ran 𝑓
14 fdm 5946 . . . . . . . . . . . . 13 (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵})
1514imaeq2d 5368 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵}))
1613, 15syl5reqr 2654 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓)
1712, 16eqtr3d 2641 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → {𝑦𝐵𝑓𝑦} = ran 𝑓)
1817eqeq1d 2607 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → ({𝑦𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦}))
1918exbidv 1835 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦}))
209, 19syl5bb 270 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦}))
218, 20mpbid 220 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → ∃𝑦ran 𝑓 = {𝑦})
22 vex 3171 . . . . . . . . . . 11 𝑦 ∈ V
2322snid 4150 . . . . . . . . . 10 𝑦 ∈ {𝑦}
24 eleq2 2672 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓𝑦 ∈ {𝑦}))
2523, 24mpbiri 246 . . . . . . . . 9 (ran 𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓)
26 frn 5948 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → ran 𝑓𝐴)
2726sseld 3562 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓𝑦𝐴))
2825, 27syl5 33 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦𝐴))
29 dffn4 6015 . . . . . . . . . . . 12 (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓)
304, 29sylib 206 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}–onto→ran 𝑓)
31 fof 6009 . . . . . . . . . . 11 (𝑓:{𝐵}–onto→ran 𝑓𝑓:{𝐵}⟶ran 𝑓)
3230, 31syl 17 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}⟶ran 𝑓)
33 feq3 5923 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓𝑓:{𝐵}⟶{𝑦}))
3432, 33syl5ibcom 233 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦}))
355, 22fsn 6289 . . . . . . . . 9 (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {⟨𝐵, 𝑦⟩})
3634, 35syl6ib 239 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓 = {⟨𝐵, 𝑦⟩}))
3728, 36jcad 553 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → (𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3837eximdv 1831 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3921, 38mpd 15 . . . . 5 (𝑓:{𝐵}⟶𝐴 → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
40 df-rex 2897 . . . . 5 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} ↔ ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
4139, 40sylibr 222 . . . 4 (𝑓:{𝐵}⟶𝐴 → ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
425, 22f1osn 6069 . . . . . . . . 9 {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}
43 f1oeq1 6021 . . . . . . . . 9 (𝑓 = {⟨𝐵, 𝑦⟩} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}))
4442, 43mpbiri 246 . . . . . . . 8 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}–1-1-onto→{𝑦})
45 f1of 6031 . . . . . . . 8 (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦})
4644, 45syl 17 . . . . . . 7 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶{𝑦})
47 snssi 4275 . . . . . . 7 (𝑦𝐴 → {𝑦} ⊆ 𝐴)
48 fss 5951 . . . . . . 7 ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴)
4946, 47, 48syl2an 492 . . . . . 6 ((𝑓 = {⟨𝐵, 𝑦⟩} ∧ 𝑦𝐴) → 𝑓:{𝐵}⟶𝐴)
5049expcom 449 . . . . 5 (𝑦𝐴 → (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴))
5150rexlimiv 3004 . . . 4 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴)
5241, 51impbii 197 . . 3 (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
533, 52bitri 262 . 2 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
5453abbi2i 2720 1 (𝐴𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1975  ∃!weu 2453  {cab 2591  wrex 2892  Vcvv 3168  wss 3535  {csn 4120  cop 4126   class class class wbr 4573  dom cdm 5024  ran crn 5025  cima 5027  Rel wrel 5029   Fn wfn 5781  wf 5782  ontowfo 5784  1-1-ontowf1o 5785  (class class class)co 6523  𝑚 cmap 7717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-map 7719
This theorem is referenced by:  mapsnen  7893
  Copyright terms: Public domain W3C validator