{J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      (W : CategoryTheory.MorphismProperty J) →
        (P : CategoryTheory.ObjectProperty J) →
          (∀ {i j : J} {f : i ⟶ j}, W f → P i) →
            (∀ {i j : J} {f : i ⟶ j}, W f → P j) →
              W.HasCardinalLT κ →
                P.HasCardinalLT κ → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ