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