∀ {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}},
  BddAbove (Set.range f) →
    BddAbove (Set.range f') →
      ∀ (g : ι → ι'),
        (∀ (i : ι), Cardinal.lift.{v', v} (f i) ≤ Cardinal.lift.{v, v'} (f' (g i))) →
          Cardinal.lift.{v', v} (iSup f) ≤ Cardinal.lift.{v, v'} (iSup f')