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 ) |
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 ) |