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

Theorem mapsn 7884
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 4899 . . . 4 {𝐵} ∈ V
31, 2elmap 7871 . . 3 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴)
4 ffn 6032 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴𝑓 Fn {𝐵})
5 map0.2 . . . . . . . . 9 𝐵 ∈ V
65snid 4199 . . . . . . . 8 𝐵 ∈ {𝐵}
7 fneu 5983 . . . . . . . 8 ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦)
84, 6, 7sylancl 693 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → ∃!𝑦 𝐵𝑓𝑦)
9 euabsn 4252 . . . . . . . 8 (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦})
10 frel 6037 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → Rel 𝑓)
11 relimasn 5476 . . . . . . . . . . . 12 (Rel 𝑓 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
1210, 11syl 17 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = {𝑦𝐵𝑓𝑦})
13 imadmrn 5464 . . . . . . . . . . . 12 (𝑓 “ dom 𝑓) = ran 𝑓
14 fdm 6038 . . . . . . . . . . . . 13 (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵})
1514imaeq2d 5454 . . . . . . . . . . . 12 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵}))
1613, 15syl5reqr 2669 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓)
1712, 16eqtr3d 2656 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → {𝑦𝐵𝑓𝑦} = ran 𝑓)
1817eqeq1d 2622 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → ({𝑦𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦}))
1918exbidv 1848 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (∃𝑦{𝑦𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦}))
209, 19syl5bb 272 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦}))
218, 20mpbid 222 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → ∃𝑦ran 𝑓 = {𝑦})
22 vex 3198 . . . . . . . . . . 11 𝑦 ∈ V
2322snid 4199 . . . . . . . . . 10 𝑦 ∈ {𝑦}
24 eleq2 2688 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓𝑦 ∈ {𝑦}))
2523, 24mpbiri 248 . . . . . . . . 9 (ran 𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓)
26 frn 6040 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴 → ran 𝑓𝐴)
2726sseld 3594 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓𝑦𝐴))
2825, 27syl5 34 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑦𝐴))
29 dffn4 6108 . . . . . . . . . . . 12 (𝑓 Fn {𝐵} ↔ 𝑓:{𝐵}–onto→ran 𝑓)
304, 29sylib 208 . . . . . . . . . . 11 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}–onto→ran 𝑓)
31 fof 6102 . . . . . . . . . . 11 (𝑓:{𝐵}–onto→ran 𝑓𝑓:{𝐵}⟶ran 𝑓)
3230, 31syl 17 . . . . . . . . . 10 (𝑓:{𝐵}⟶𝐴𝑓:{𝐵}⟶ran 𝑓)
33 feq3 6015 . . . . . . . . . 10 (ran 𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓𝑓:{𝐵}⟶{𝑦}))
3432, 33syl5ibcom 235 . . . . . . . . 9 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦}))
355, 22fsn 6387 . . . . . . . . 9 (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {⟨𝐵, 𝑦⟩})
3634, 35syl6ib 241 . . . . . . . 8 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓 = {⟨𝐵, 𝑦⟩}))
3728, 36jcad 555 . . . . . . 7 (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → (𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3837eximdv 1844 . . . . . 6 (𝑓:{𝐵}⟶𝐴 → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩})))
3921, 38mpd 15 . . . . 5 (𝑓:{𝐵}⟶𝐴 → ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
40 df-rex 2915 . . . . 5 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} ↔ ∃𝑦(𝑦𝐴𝑓 = {⟨𝐵, 𝑦⟩}))
4139, 40sylibr 224 . . . 4 (𝑓:{𝐵}⟶𝐴 → ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
425, 22f1osn 6163 . . . . . . . . 9 {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}
43 f1oeq1 6114 . . . . . . . . 9 (𝑓 = {⟨𝐵, 𝑦⟩} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}))
4442, 43mpbiri 248 . . . . . . . 8 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}–1-1-onto→{𝑦})
45 f1of 6124 . . . . . . . 8 (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦})
4644, 45syl 17 . . . . . . 7 (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶{𝑦})
47 snssi 4330 . . . . . . 7 (𝑦𝐴 → {𝑦} ⊆ 𝐴)
48 fss 6043 . . . . . . 7 ((𝑓:{𝐵}⟶{𝑦} ∧ {𝑦} ⊆ 𝐴) → 𝑓:{𝐵}⟶𝐴)
4946, 47, 48syl2an 494 . . . . . 6 ((𝑓 = {⟨𝐵, 𝑦⟩} ∧ 𝑦𝐴) → 𝑓:{𝐵}⟶𝐴)
5049expcom 451 . . . . 5 (𝑦𝐴 → (𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴))
5150rexlimiv 3023 . . . 4 (∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴)
5241, 51impbii 199 . . 3 (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
533, 52bitri 264 . 2 (𝑓 ∈ (𝐴𝑚 {𝐵}) ↔ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
5453abbi2i 2736 1 (𝐴𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1481  wex 1702  wcel 1988  ∃!weu 2468  {cab 2606  wrex 2910  Vcvv 3195  wss 3567  {csn 4168  cop 4174   class class class wbr 4644  dom cdm 5104  ran crn 5105  cima 5107  Rel wrel 5109   Fn wfn 5871  wf 5872  ontowfo 5874  1-1-ontowf1o 5875  (class class class)co 6635  𝑚 cmap 7842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-map 7844
This theorem is referenced by:  mapsnen  8020
  Copyright terms: Public domain W3C validator