α β : Type u
a b c : Cardinal
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ (x : Cardinal), x < b → a ^ x ≤ c

case h
α β : Type u
a b c : Cardinal
⊢ BddAbove (range fun c => a ^ ↑c)
α β : Type u
a b c : Cardinal
⊢ a ^< b ≤ c ↔ ∀ (x : Cardinal), x < b → a ^ x ≤ c
rw [powerlt, ciSup_le_iff']
no goals
α β : Type u
a b c : Cardinal
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ (x : Cardinal), x < b → a ^ x ≤ c
simp
case h
α β : Type u
a b c : Cardinal
⊢ BddAbove (HPow.hPow a '' Iio b)
case h
α β : Type u
a b c : Cardinal
⊢ BddAbove (range fun c => a ^ ↑c)
rw [← image_eq_range]
no goals
case h
α β : Type u
a b c : Cardinal
⊢ BddAbove (HPow.hPow a '' Iio b)
exact bddAbove_image.{u, u} _ bddAbove_Iio