Metamath Proof Explorer


Theorem snmapen1

Description: Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022)

Ref Expression
Assertion snmapen1 ( ( 𝐴𝑉𝐵𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ 1o )

Proof

Step Hyp Ref Expression
1 snmapen ( ( 𝐴𝑉𝐵𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } )
2 ensn1g ( 𝐴𝑉 → { 𝐴 } ≈ 1o )
3 2 adantr ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 } ≈ 1o )
4 entr ( ( ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } ∧ { 𝐴 } ≈ 1o ) → ( { 𝐴 } ↑m 𝐵 ) ≈ 1o )
5 1 3 4 syl2anc ( ( 𝐴𝑉𝐵𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ 1o )