∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N),
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).dom = ⨆ x, (S x).dom