Theorem mapsnend

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)

	Ref	Expression
Hypotheses	mapsnend.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	mapsnend.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	mapsnend	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mapsnend.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		mapsnend.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		ovexd	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) ∈ V )
4		fvexd	⊢ ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) → ( 𝑧 ‘ 𝐵 ) ∈ V )
5	4	a1i	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) → ( 𝑧 ‘ 𝐵 ) ∈ V ) )
6		snex	⊢ { ⟨ 𝐵 , 𝑤 ⟩ } ∈ V
7	6	2a1i	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 → { ⟨ 𝐵 , 𝑤 ⟩ } ∈ V ) )
8	1 2	mapsnd	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } } )
9	8	abeq2d	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) ↔ ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) )
10	9	anbi1d	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) )
11		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) )
12	11	bicomi	⊢ ( ( ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) )
13	12	a1i	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ 𝐴 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) )
14		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) )
15	14	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) ) )
16	10 13 15	3bitrd	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) ) )
17		fveq1	⊢ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝑧 ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) )
18		vex	⊢ 𝑦 ∈ V
19		fvsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑦 ∈ V ) → ( { ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) = 𝑦 )
20	2 18 19	sylancl	⊢ ( 𝜑 → ( { ⟨ 𝐵 , 𝑦 ⟩ } ‘ 𝐵 ) = 𝑦 )
21	17 20	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → ( 𝑧 ‘ 𝐵 ) = 𝑦 )
22	21	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → ( 𝑤 = ( 𝑧 ‘ 𝐵 ) ↔ 𝑤 = 𝑦 ) )
23		equcom	⊢ ( 𝑤 = 𝑦 ↔ 𝑦 = 𝑤 )
24	22 23	bitrdi	⊢ ( ( 𝜑 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) → ( 𝑤 = ( 𝑧 ‘ 𝐵 ) ↔ 𝑦 = 𝑤 ) )
25	24	pm5.32da	⊢ ( 𝜑 → ( ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑦 = 𝑤 ) ) )
26	25	anbi2d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑦 = 𝑤 ) ) ) )
27		anass	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ∧ 𝑦 = 𝑤 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑦 = 𝑤 ) ) )
28	27	a1i	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ∧ 𝑦 = 𝑤 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑦 = 𝑤 ) ) ) )
29		ancom	⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ∧ 𝑦 = 𝑤 ) ↔ ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) )
30	29	a1i	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ∧ 𝑦 = 𝑤 ) ↔ ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) ) )
31	26 28 30	3bitr2d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) ↔ ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) ) )
32	31	exbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ) ↔ ∃ 𝑦 ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) ) )
33		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
34		opeq2	⊢ ( 𝑦 = 𝑤 → ⟨ 𝐵 , 𝑦 ⟩ = ⟨ 𝐵 , 𝑤 ⟩ )
35	34	sneqd	⊢ ( 𝑦 = 𝑤 → { ⟨ 𝐵 , 𝑦 ⟩ } = { ⟨ 𝐵 , 𝑤 ⟩ } )
36	35	eqeq2d	⊢ ( 𝑦 = 𝑤 → ( 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ↔ 𝑧 = { ⟨ 𝐵 , 𝑤 ⟩ } ) )
37	33 36	anbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑤 ⟩ } ) ) )
38	37	equsexvw	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑤 ⟩ } ) )
39	38	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 = 𝑤 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑦 ⟩ } ) ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑤 ⟩ } ) ) )
40	16 32 39	3bitrd	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 ↑m { 𝐵 } ) ∧ 𝑤 = ( 𝑧 ‘ 𝐵 ) ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑧 = { ⟨ 𝐵 , 𝑤 ⟩ } ) ) )
41	3 1 5 7 40	en2d	⊢ ( 𝜑 → ( 𝐴 ↑m { 𝐵 } ) ≈ 𝐴 )