This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqabrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 ↑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 { 𝐵 } ) ≈ 𝐴 )