Theorem mapsnd 6963

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.)

Hypotheses

Ref	Expression
mapsnd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
mapsnd.2	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
mapsnd	⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}})

Distinct variable groups:   𝐴,𝑓,𝑦   𝐵,𝑓,𝑦   𝜑,𝑓,𝑦

Allowed substitution hints:   𝑉(𝑦,𝑓)   𝑊(𝑦,𝑓)

Proof of Theorem mapsnd

Step	Hyp	Ref	Expression
1		mapsnd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		mapsnd.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		snexg 4319	. . . . 5 ⊢ (𝐵 ∈ 𝑊 → {𝐵} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝜑 → {𝐵} ∈ V)
5	1, 4	elmapd 6929	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ 𝑓:{𝐵}⟶𝐴))
6		ffn 5531	. . . . . . . . 9 ⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓 Fn {𝐵})
7		snidg 3737	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵})
8	2, 7	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ {𝐵})
9		fneu 5485	. . . . . . . . 9 ⊢ ((𝑓 Fn {𝐵} ∧ 𝐵 ∈ {𝐵}) → ∃!𝑦 𝐵𝑓𝑦)
10	6, 8, 9	syl2anr 290	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃!𝑦 𝐵𝑓𝑦)
11		euabsn 3780	. . . . . . . . 9 ⊢ (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦})
12		imasng 5150	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑊 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦})
13	2, 12	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑓 “ {𝐵}) = {𝑦 ∣ 𝐵𝑓𝑦})
14		fdm 5537	. . . . . . . . . . . . . 14 ⊢ (𝑓:{𝐵}⟶𝐴 → dom 𝑓 = {𝐵})
15	14	imaeq2d 5124	. . . . . . . . . . . . 13 ⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ {𝐵}))
16		imadmrn 5134	. . . . . . . . . . . . 13 ⊢ (𝑓 “ dom 𝑓) = ran 𝑓
17	15, 16	eqtr3di 2286	. . . . . . . . . . . 12 ⊢ (𝑓:{𝐵}⟶𝐴 → (𝑓 “ {𝐵}) = ran 𝑓)
18	13, 17	sylan9req 2292	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → {𝑦 ∣ 𝐵𝑓𝑦} = ran 𝑓)
19	18	eqeq1d 2247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ({𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ran 𝑓 = {𝑦}))
20	19	exbidv 1878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (∃𝑦{𝑦 ∣ 𝐵𝑓𝑦} = {𝑦} ↔ ∃𝑦ran 𝑓 = {𝑦}))
21	11, 20	bitrid 192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (∃!𝑦 𝐵𝑓𝑦 ↔ ∃𝑦ran 𝑓 = {𝑦}))
22	10, 21	mpbid 147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦ran 𝑓 = {𝑦})
23		frn 5540	. . . . . . . . . . . . 13 ⊢ (𝑓:{𝐵}⟶𝐴 → ran 𝑓 ⊆ 𝐴)
24	23	sseld 3247	. . . . . . . . . . . 12 ⊢ (𝑓:{𝐵}⟶𝐴 → (𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴))
25		vsnid 3740	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ {𝑦}
26		eleq2 2302	. . . . . . . . . . . . 13 ⊢ (ran 𝑓 = {𝑦} → (𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ {𝑦}))
27	25, 26	mpbiri 168	. . . . . . . . . . . 12 ⊢ (ran 𝑓 = {𝑦} → 𝑦 ∈ ran 𝑓)
28	24, 27	impel 280	. . . . . . . . . . 11 ⊢ ((𝑓:{𝐵}⟶𝐴 ∧ ran 𝑓 = {𝑦}) → 𝑦 ∈ 𝐴)
29	28	adantll 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑦 ∈ 𝐴)
30		ffrn 5543	. . . . . . . . . . . . . 14 ⊢ (𝑓:{𝐵}⟶𝐴 → 𝑓:{𝐵}⟶ran 𝑓)
31		feq3 5516	. . . . . . . . . . . . . 14 ⊢ (ran 𝑓 = {𝑦} → (𝑓:{𝐵}⟶ran 𝑓 ↔ 𝑓:{𝐵}⟶{𝑦}))
32	30, 31	syl5ibcom 155	. . . . . . . . . . . . 13 ⊢ (𝑓:{𝐵}⟶𝐴 → (ran 𝑓 = {𝑦} → 𝑓:{𝐵}⟶{𝑦}))
33	32	imp 124	. . . . . . . . . . . 12 ⊢ ((𝑓:{𝐵}⟶𝐴 ∧ ran 𝑓 = {𝑦}) → 𝑓:{𝐵}⟶{𝑦})
34	33	adantll 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑓:{𝐵}⟶{𝑦})
35	2	ad2antrr 492	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝐵 ∈ 𝑊)
36		vex 2824	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
37		fsng 5875	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V) → (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {⟨𝐵, 𝑦⟩}))
38	35, 36, 37	sylancl 417	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → (𝑓:{𝐵}⟶{𝑦} ↔ 𝑓 = {⟨𝐵, 𝑦⟩}))
39	34, 38	mpbid 147	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → 𝑓 = {⟨𝐵, 𝑦⟩})
40	29, 39	jca 306	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) ∧ ran 𝑓 = {𝑦}) → (𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}))
41	40	ex 115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (ran 𝑓 = {𝑦} → (𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩})))
42	41	eximdv 1933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → (∃𝑦ran 𝑓 = {𝑦} → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩})))
43	22, 42	mpd 13	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}))
44		df-rex 2534	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩} ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}))
45	43, 44	sylibr 134	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:{𝐵}⟶𝐴) → ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩})
46	45	ex 115	. . . 4 ⊢ (𝜑 → (𝑓:{𝐵}⟶𝐴 → ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}))
47		f1osng 5680	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V) → {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦})
48	2, 36, 47	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦})
49	48	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦})
50		f1oeq1 5625	. . . . . . . . . . 11 ⊢ (𝑓 = {⟨𝐵, 𝑦⟩} → (𝑓:{𝐵}–1-1-onto→{𝑦} ↔ {⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦}))
51	50	bicomd 141	. . . . . . . . . 10 ⊢ (𝑓 = {⟨𝐵, 𝑦⟩} → ({⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦} ↔ 𝑓:{𝐵}–1-1-onto→{𝑦}))
52	51	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → ({⟨𝐵, 𝑦⟩}:{𝐵}–1-1-onto→{𝑦} ↔ 𝑓:{𝐵}–1-1-onto→{𝑦}))
53	49, 52	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → 𝑓:{𝐵}–1-1-onto→{𝑦})
54		f1of 5637	. . . . . . . 8 ⊢ (𝑓:{𝐵}–1-1-onto→{𝑦} → 𝑓:{𝐵}⟶{𝑦})
55	53, 54	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → 𝑓:{𝐵}⟶{𝑦})
56	55	3adant2 1047	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → 𝑓:{𝐵}⟶{𝑦})
57		snssi 3857	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴)
58	57	3ad2ant2 1050	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → {𝑦} ⊆ 𝐴)
59	56, 58	fssd 5545	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = {⟨𝐵, 𝑦⟩}) → 𝑓:{𝐵}⟶𝐴)
60	59	rexlimdv3a 2670	. . . 4 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩} → 𝑓:{𝐵}⟶𝐴))
61	46, 60	impbid 129	. . 3 ⊢ (𝜑 → (𝑓:{𝐵}⟶𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}))
62	5, 61	bitrd 188	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝐴 ↑𝑚 {𝐵}) ↔ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}))
63	62	eqabdv 2369	1 ⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}})

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009   = wceq 1402  ∃wex 1545  ∃!weu 2086   ∈ wcel 2209  {cab 2224  ∃wrex 2529  Vcvv 2821   ⊆ wss 3220  {csn 3708  ⟨cop 3711   class class class wbr 4128  dom cdm 4772  ran crn 4773   “ cima 4775   Fn wfn 5370  ⟶wf 5371  –1-1-onto→wf1o 5374  (class class class)co 6078   ↑_𝑚 cmap 6915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-ov 6081  df-oprab 6082  df-mpo 6083  df-map 6917

This theorem is referenced by:  mapsnend  7092