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

Theorem mapsnend 8436
Description: Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
mapsnend.a (𝜑𝐴𝑉)
mapsnend.b (𝜑𝐵𝑊)
Assertion
Ref Expression
mapsnend (𝜑 → (𝐴𝑚 {𝐵}) ≈ 𝐴)

Proof of Theorem mapsnend
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovexd 7050 . 2 (𝜑 → (𝐴𝑚 {𝐵}) ∈ V)
2 mapsnend.a . . 3 (𝜑𝐴𝑉)
32elexd 3457 . 2 (𝜑𝐴 ∈ V)
4 fvexd 6553 . . 3 (𝑧 ∈ (𝐴𝑚 {𝐵}) → (𝑧𝐵) ∈ V)
54a1i 11 . 2 (𝜑 → (𝑧 ∈ (𝐴𝑚 {𝐵}) → (𝑧𝐵) ∈ V))
6 snex 5223 . . 3 {⟨𝐵, 𝑤⟩} ∈ V
762a1i 12 . 2 (𝜑 → (𝑤𝐴 → {⟨𝐵, 𝑤⟩} ∈ V))
8 mapsnend.b . . . . . . 7 (𝜑𝐵𝑊)
92, 8mapsnd 8299 . . . . . 6 (𝜑 → (𝐴𝑚 {𝐵}) = {𝑧 ∣ ∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩}})
109abeq2d 2916 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴𝑚 {𝐵}) ↔ ∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩}))
1110anbi1d 629 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴𝑚 {𝐵}) ∧ 𝑤 = (𝑧𝐵)) ↔ (∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))))
12 r19.41v 3308 . . . . . 6 (∃𝑦𝐴 (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ (∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)))
1312bicomi 225 . . . . 5 ((∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ ∃𝑦𝐴 (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)))
1413a1i 11 . . . 4 (𝜑 → ((∃𝑦𝐴 𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ ∃𝑦𝐴 (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))))
15 df-rex 3111 . . . . 5 (∃𝑦𝐴 (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ ∃𝑦(𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))))
1615a1i 11 . . . 4 (𝜑 → (∃𝑦𝐴 (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ ∃𝑦(𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)))))
1711, 14, 163bitrd 306 . . 3 (𝜑 → ((𝑧 ∈ (𝐴𝑚 {𝐵}) ∧ 𝑤 = (𝑧𝐵)) ↔ ∃𝑦(𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)))))
18 fveq1 6537 . . . . . . . . . 10 (𝑧 = {⟨𝐵, 𝑦⟩} → (𝑧𝐵) = ({⟨𝐵, 𝑦⟩}‘𝐵))
19 vex 3440 . . . . . . . . . . 11 𝑦 ∈ V
20 fvsng 6805 . . . . . . . . . . 11 ((𝐵𝑊𝑦 ∈ V) → ({⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
218, 19, 20sylancl 586 . . . . . . . . . 10 (𝜑 → ({⟨𝐵, 𝑦⟩}‘𝐵) = 𝑦)
2218, 21sylan9eqr 2853 . . . . . . . . 9 ((𝜑𝑧 = {⟨𝐵, 𝑦⟩}) → (𝑧𝐵) = 𝑦)
2322eqeq2d 2805 . . . . . . . 8 ((𝜑𝑧 = {⟨𝐵, 𝑦⟩}) → (𝑤 = (𝑧𝐵) ↔ 𝑤 = 𝑦))
24 equcom 2002 . . . . . . . 8 (𝑤 = 𝑦𝑦 = 𝑤)
2523, 24syl6bb 288 . . . . . . 7 ((𝜑𝑧 = {⟨𝐵, 𝑦⟩}) → (𝑤 = (𝑧𝐵) ↔ 𝑦 = 𝑤))
2625pm5.32da 579 . . . . . 6 (𝜑 → ((𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵)) ↔ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑦 = 𝑤)))
2726anbi2d 628 . . . . 5 (𝜑 → ((𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))) ↔ (𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑦 = 𝑤))))
28 anass 469 . . . . . 6 (((𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}) ∧ 𝑦 = 𝑤) ↔ (𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑦 = 𝑤)))
2928a1i 11 . . . . 5 (𝜑 → (((𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}) ∧ 𝑦 = 𝑤) ↔ (𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑦 = 𝑤))))
30 ancom 461 . . . . . 6 (((𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}) ∧ 𝑦 = 𝑤) ↔ (𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩})))
3130a1i 11 . . . . 5 (𝜑 → (((𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}) ∧ 𝑦 = 𝑤) ↔ (𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}))))
3227, 29, 313bitr2d 308 . . . 4 (𝜑 → ((𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))) ↔ (𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}))))
3332exbidv 1899 . . 3 (𝜑 → (∃𝑦(𝑦𝐴 ∧ (𝑧 = {⟨𝐵, 𝑦⟩} ∧ 𝑤 = (𝑧𝐵))) ↔ ∃𝑦(𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}))))
34 eleq1w 2865 . . . . . 6 (𝑦 = 𝑤 → (𝑦𝐴𝑤𝐴))
35 opeq2 4711 . . . . . . . 8 (𝑦 = 𝑤 → ⟨𝐵, 𝑦⟩ = ⟨𝐵, 𝑤⟩)
3635sneqd 4484 . . . . . . 7 (𝑦 = 𝑤 → {⟨𝐵, 𝑦⟩} = {⟨𝐵, 𝑤⟩})
3736eqeq2d 2805 . . . . . 6 (𝑦 = 𝑤 → (𝑧 = {⟨𝐵, 𝑦⟩} ↔ 𝑧 = {⟨𝐵, 𝑤⟩}))
3834, 37anbi12d 630 . . . . 5 (𝑦 = 𝑤 → ((𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩}) ↔ (𝑤𝐴𝑧 = {⟨𝐵, 𝑤⟩})))
3938equsexvw 1988 . . . 4 (∃𝑦(𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩})) ↔ (𝑤𝐴𝑧 = {⟨𝐵, 𝑤⟩}))
4039a1i 11 . . 3 (𝜑 → (∃𝑦(𝑦 = 𝑤 ∧ (𝑦𝐴𝑧 = {⟨𝐵, 𝑦⟩})) ↔ (𝑤𝐴𝑧 = {⟨𝐵, 𝑤⟩})))
4117, 33, 403bitrd 306 . 2 (𝜑 → ((𝑧 ∈ (𝐴𝑚 {𝐵}) ∧ 𝑤 = (𝑧𝐵)) ↔ (𝑤𝐴𝑧 = {⟨𝐵, 𝑤⟩})))
421, 3, 5, 7, 41en2d 8393 1 (𝜑 → (𝐴𝑚 {𝐵}) ≈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wex 1761  wcel 2081  wrex 3106  Vcvv 3437  {csn 4472  cop 4478   class class class wbr 4962  cfv 6225  (class class class)co 7016  𝑚 cmap 8256  cen 8354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-map 8258  df-en 8358
This theorem is referenced by:  mapsnen  8437  map2xp  8534  mapdom3  8536  ackbij1lem5  9492  pwxpndom2  9933  hashmap  13644  mpct  41004
  Copyright terms: Public domain W3C validator