α : Type ?u.298606
β : Type ?u.298609
γ : Type ?u.298612
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Cardinal
hs : BddAbove s
a : Ordinal
⊢ (∀ (x : Cardinal), x ∈ s → x ≤ card a) ↔ ∀ (x : Ordinal), x ∈ ord '' s → x ≤ a
α : Type ?u.298606
β : Type ?u.298609
γ : Type ?u.298612
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Cardinal
hs : BddAbove s
a : Ordinal
⊢ ord (sSup s) ≤ a ↔ sSup (ord '' s) ≤ a
rw [csSup_le_iff'
    (bddAbove_iff_small.2 (@small_image _ _ _ s (Cardinal.bddAbove_iff_small.1 hs))),
  ord_le, csSup_le_iff' hs]
no goals
α : Type ?u.298606
β : Type ?u.298609
γ : Type ?u.298612
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
s : Set Cardinal
hs : BddAbove s
a : Ordinal
⊢ (∀ (x : Cardinal), x ∈ s → x ≤ card a) ↔ ∀ (x : Ordinal), x ∈ ord '' s → x ≤ a
simp [ord_le]