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

Metamath Proof Explorer

Theorem snmapen

Description: Set exponentiation: a singleton to any set is equinumerous to that singleton. (Contributed by NM, 17-Dec-2003) (Revised by AV, 17-Jul-2022)

Ref Expression
Assertion snmapen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } )

Proof

Step Hyp Ref Expression
1 ovexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ∈ V )
2 snex ⊢ { 𝐴 } ∈ V
3 2 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 } ∈ V )
4 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
5 4 a1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) → 𝐴 ∈ 𝑉 ) )
6 2 a1i ⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ V )
7 6 anim1ci ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ 𝑊 ∧ { 𝐴 } ∈ V ) )
8 xpexg ⊢ ( ( 𝐵 ∈ 𝑊 ∧ { 𝐴 } ∈ V ) → ( 𝐵 × { 𝐴 } ) ∈ V )
9 7 8 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { 𝐴 } ) ∈ V )
10 9 a1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑦 ∈ { 𝐴 } → ( 𝐵 × { 𝐴 } ) ∈ V ) )
11 velsn ⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
12 11 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 ) )
13 elmapg ⊢ ( ( { 𝐴 } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ↔ 𝑥 : 𝐵 ⟶ { 𝐴 } ) )
14 6 13 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ↔ 𝑥 : 𝐵 ⟶ { 𝐴 } ) )
15 fconst2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 : 𝐵 ⟶ { 𝐴 } ↔ 𝑥 = ( 𝐵 × { 𝐴 } ) ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 : 𝐵 ⟶ { 𝐴 } ↔ 𝑥 = ( 𝐵 × { 𝐴 } ) ) )
17 14 16 bitr2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 = ( 𝐵 × { 𝐴 } ) ↔ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) )
18 12 17 anbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑦 ∈ { 𝐴 } ∧ 𝑥 = ( 𝐵 × { 𝐴 } ) ) ↔ ( 𝑦 = 𝐴 ∧ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) ) )
19 ancom ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) ↔ ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ∧ 𝑦 = 𝐴 ) )
20 18 19 bitr2di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑦 ∈ { 𝐴 } ∧ 𝑥 = ( 𝐵 × { 𝐴 } ) ) ) )
21 1 3 5 10 20 en2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } )