Theorem cardinal.ord_card_unbounded'

refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467) …

feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987) …