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 𝐵 ) ≈ { 𝐴 } )