Cardinality of Subobject

If X ⟶ Y is a monomorphism, and the cardinality of Subobject Y is < κ, then the cardinality of Subobject X is also < κ.

theorem CategoryTheory.Subobject.hasCardinalLT_of_mono {C : Type u} [Category.{v, u} C] {Y : C} {κ : Cardinal.{w}} (h : HasCardinalLT (Subobject Y) κ) {X : C} (f : X ⟶ Y) [Mono f] : HasCardinalLT (Subobject X) κ