Description: Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of Mendelson p. 255. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 14-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | map0e | |- ( A e. V -> ( A ^m (/) ) = 1o ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapdm0 | |- ( A e. V -> ( A ^m (/) ) = { (/) } ) |
|
| 2 | df1o2 | |- 1o = { (/) } |
|
| 3 | 1 2 | eqtr4di | |- ( A e. V -> ( A ^m (/) ) = 1o ) |