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 )