∀ {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}},
  c.IsRegular →
    Cardinal.mk ι < c →
      c ≠ Cardinal.aleph0 →
        (∀ (i : ι), ∀ b < c.ord, f i b < c.ord) → ∀ {a : Ordinal.{u}}, a < c.ord → Ordinal.derivFamily f a < c.ord