Theorem mapsnd

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)

	Ref	Expression
Hypotheses	mapsnd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	mapsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	mapsnd	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } } )

Proof

Step	Hyp	Ref	Expression
1		mapsnd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		mapsnd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		snex	⊢ { 𝐵 } ∈ V
4	3	a1i	⊢ ( 𝜑 → { 𝐵 } ∈ V )
5	1 4	elmapd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 ↑m { 𝐵 } ) ↔ 𝑓 : { 𝐵 } ⟶ 𝐴 ) )
6		ffn	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → 𝑓 Fn { 𝐵 } )
7		snidg	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 } )
8	2 7	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 } )
9		fneu	⊢ ( ( 𝑓 Fn { 𝐵 } ∧ 𝐵 ∈ { 𝐵 } ) → ∃! 𝑦 𝐵 𝑓 𝑦 )
10	6 8 9	syl2anr	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃! 𝑦 𝐵 𝑓 𝑦 )
11		euabsn	⊢ ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } )
12		frel	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → Rel 𝑓 )
13		relimasn	⊢ ( Rel 𝑓 → ( 𝑓 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝑓 𝑦 } )
14	12 13	syl	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝑓 𝑦 } )
15		fdm	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → dom 𝑓 = { 𝐵 } )
16	15	imaeq2d	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ { 𝐵 } ) )
17		imadmrn	⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
18	16 17	eqtr3di	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑓 “ { 𝐵 } ) = ran 𝑓 )
19	14 18	eqtr3d	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → { 𝑦 ∣ 𝐵 𝑓 𝑦 } = ran 𝑓 )
20	19	eqeq1d	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } ↔ ran 𝑓 = { 𝑦 } ) )
21	20	exbidv	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ∃ 𝑦 { 𝑦 ∣ 𝐵 𝑓 𝑦 } = { 𝑦 } ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
22	11 21	bitrid	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ∃! 𝑦 𝐵 𝑓 𝑦 ↔ ∃ 𝑦 ran 𝑓 = { 𝑦 } ) )
24	10 23	mpbid	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ran 𝑓 = { 𝑦 } )
25		frn	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ran 𝑓 ⊆ 𝐴 )
26	25	sseld	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( 𝑦 ∈ ran 𝑓 → 𝑦 ∈ 𝐴 ) )
27		vsnid	⊢ 𝑦 ∈ { 𝑦 }
28		eleq2	⊢ ( ran 𝑓 = { 𝑦 } → ( 𝑦 ∈ ran 𝑓 ↔ 𝑦 ∈ { 𝑦 } ) )
29	27 28	mpbiri	⊢ ( ran 𝑓 = { 𝑦 } → 𝑦 ∈ ran 𝑓 )
30	26 29	impel	⊢ ( ( 𝑓 : { 𝐵 } ⟶ 𝐴 ∧ ran 𝑓 = { 𝑦 } ) → 𝑦 ∈ 𝐴 )
31	30	adantll	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑦 ∈ 𝐴 )
32		ffrn	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → 𝑓 : { 𝐵 } ⟶ ran 𝑓 )
33		feq3	⊢ ( ran 𝑓 = { 𝑦 } → ( 𝑓 : { 𝐵 } ⟶ ran 𝑓 ↔ 𝑓 : { 𝐵 } ⟶ { 𝑦 } ) )
34	32 33	syl5ibcom	⊢ ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ( ran 𝑓 = { 𝑦 } → 𝑓 : { 𝐵 } ⟶ { 𝑦 } ) )
35	34	imp	⊢ ( ( 𝑓 : { 𝐵 } ⟶ 𝐴 ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
36	35	adantll	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
37	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝐵 ∈ 𝑊 )
38		vex	⊢ 𝑦 ∈ V
39		fsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V ) → ( 𝑓 : { 𝐵 } ⟶ { 𝑦 } ↔ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
40	37 38 39	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → ( 𝑓 : { 𝐵 } ⟶ { 𝑦 } ↔ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
41	36 40	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } )
42	31 41	jca	⊢ ( ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) ∧ ran 𝑓 = { 𝑦 } ) → ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
43	42	ex	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ran 𝑓 = { 𝑦 } → ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) )
44	43	eximdv	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ( ∃ 𝑦 ran 𝑓 = { 𝑦 } → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) )
45	24 44	mpd	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
46		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
47	45 46	sylibr	⊢ ( ( 𝜑 ∧ 𝑓 : { 𝐵 } ⟶ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } )
48	47	ex	⊢ ( 𝜑 → ( 𝑓 : { 𝐵 } ⟶ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
49		f1osng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V ) → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
50	2 38 49	sylancl	⊢ ( 𝜑 → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } )
52		f1oeq1	⊢ ( 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
53	52	bicomd	⊢ ( 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → ( { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
54	53	adantl	⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → ( { ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐵 } –1-1-onto→ { 𝑦 } ↔ 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } ) )
55	51 54	mpbid	⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } )
56		f1of	⊢ ( 𝑓 : { 𝐵 } –1-1-onto→ { 𝑦 } → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
58	57	3adant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ { 𝑦 } )
59		snssi	⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ⊆ 𝐴 )
60	59	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → { 𝑦 } ⊆ 𝐴 )
61	58 60	fssd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → 𝑓 : { 𝐵 } ⟶ 𝐴 )
62	61	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } → 𝑓 : { 𝐵 } ⟶ 𝐴 ) )
63	48 62	impbid	⊢ ( 𝜑 → ( 𝑓 : { 𝐵 } ⟶ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
64	5 63	bitrd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 ↑m { 𝐵 } ) ↔ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
65	64	eqabdv	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) = { 𝑓 ∣ ∃ 𝑦 ∈ 𝐴 𝑓 = { ⟨ 𝐵 , 𝑦 ⟩ } } )