theorem power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ Cardinal.aleph0) (hb : b < Cardinal.aleph0) : a ^ b ≤ Cardinal.aleph0