I want to suggest to provide a special symbol ` 0o `for the ordinal number 0, which actually is the empty set `(/) `, see ~0elon and df-1o. It would be just a synonym for ` (/) `:
` df-0o $a |- 0o = (/) $. ` With such a symbol, the theorems in the context of ordinal numbers can be written in a more intuitive way. For example ` map0e $p |- ( A e. V -> ( A ^m (/) ) = 1o )` could be written as map0e $p |- ( A e. V -> ( A ^m 0o ) = 1o ) Was this already proposed/discussed before? What do others think about it? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c6bc77ee-56cd-458c-a176-3f616e0c862an%40googlegroups.com.
