diff --git a/Mathlib.lean b/Mathlib.lean
index 624f35d65fc813..5037a0fff72b4d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5696,6 +5696,7 @@ public import Mathlib.ModelTheory.Bundled
 public import Mathlib.ModelTheory.Complexity
 public import Mathlib.ModelTheory.Definability
 public import Mathlib.ModelTheory.DirectLimit
+public import Mathlib.ModelTheory.ElementaryChain
 public import Mathlib.ModelTheory.ElementaryMaps
 public import Mathlib.ModelTheory.ElementarySubstructures
 public import Mathlib.ModelTheory.Encoding
@@ -7177,6 +7178,7 @@ public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 public import Mathlib.SetTheory.Cardinal.Continuum
 public import Mathlib.SetTheory.Cardinal.CountableCover
 public import Mathlib.SetTheory.Cardinal.Defs
+public import Mathlib.SetTheory.Cardinal.DirectLimit
 public import Mathlib.SetTheory.Cardinal.Divisibility
 public import Mathlib.SetTheory.Cardinal.ENNReal
 public import Mathlib.SetTheory.Cardinal.ENat
diff --git a/Mathlib/ModelTheory/ElementaryChain.lean b/Mathlib/ModelTheory/ElementaryChain.lean
new file mode 100644
index 00000000000000..ee99dec227fa2a
--- /dev/null
+++ b/Mathlib/ModelTheory/ElementaryChain.lean
@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2026 Zikang Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zikang Yu
+-/
+module
+
+public import Mathlib.ModelTheory.DirectLimit
+public import Mathlib.ModelTheory.ElementaryMaps
+public import Mathlib.SetTheory.Cardinal.DirectLimit
+
+/-!
+# Elementary chains
+
+This file defines elementary chains without choosing a common ambient structure. Their unions are
+constructed as direct limits of the underlying directed systems of first-order embeddings.
+
+## Main definitions
+
+- `FirstOrder.Language.ElementaryChain`: A system of structures whose transition maps are
+  elementary embeddings.
+- `FirstOrder.Language.ElementaryChain.ofNatSucc`: The elementary chain generated by a sequence of
+  elementary embeddings between successive stages.
+- `FirstOrder.Language.ElementaryChain.Limit`: The direct limit of an elementary chain.
+- `FirstOrder.Language.ElementaryChain.toLimitElementary`: The canonical elementary embedding of a
+  stage into the limit.
+- `FirstOrder.Language.ElementaryChain.liftElementary`: The elementary lift of a compatible
+  cocone.
+
+## Main results
+
+- `FirstOrder.Language.ElementaryChain.realize_toLimit`: Bounded formulas are preserved and
+  reflected by the canonical maps into the limit.
+- `FirstOrder.Language.ElementaryChain.limit_models`: A theory modeled by a stage is modeled by the
+  limit.
+-/
+
+@[expose] public section
+
+universe u v w w'
+
+namespace FirstOrder
+
+namespace Language
+
+open scoped Cardinal
+
+/-- A system of `L`-structures whose transition maps are elementary embeddings. -/
+structure ElementaryChain (L : Language.{u, v}) (ι : Type w) [Preorder ι] where
+  /-- The structure at each stage of the chain. -/
+  carrier : ι → Type w'
+  [struc : ∀ i, L.Structure (carrier i)]
+  /-- The elementary embedding from stage `i` to stage `j` when `i ≤ j`. -/
+  map : ∀ i j, i ≤ j → carrier i ↪ₑ[L] carrier j
+  map_self : ∀ i x, map i i le_rfl x = x
+  map_map : ∀ i j k (hij : i ≤ j) (hjk : j ≤ k) (x : carrier i),
+    map j k hjk (map i j hij x) = map i k (hij.trans hjk) x
+
+attribute [instance] ElementaryChain.struc
+
+namespace ElementaryEmbedding
+
+variable {L : Language.{u, v}} {M : ℕ → Type w'} [∀ n, L.Structure (M n)]
+
+/-- Compose a sequence of elementary embeddings along an interval of natural numbers. -/
+noncomputable def natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
+    (m n : ℕ) (h : m ≤ n) : M m ↪ₑ[L] M n :=
+  Nat.leRecOn h (@fun k g ↦ (f k).comp g) (refl L _)
+
+private theorem coe_natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
+    (m n : ℕ) (h : m ≤ n) :
+    (natLERec f m n h : M m → M n) =
+      DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) m n h := by
+  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
+  ext x
+  induction k with
+  | zero => simp [natLERec, DirectedSystem.natLERec, Nat.leRecOn_self]
+  | succ k ih =>
+    simp only [natLERec, DirectedSystem.coe_natLERec]
+    rw [Nat.leRecOn_succ le_self_add, Nat.leRecOn_succ le_self_add]
+    specialize ih (Nat.le_add_right m k)
+    simp only [natLERec, DirectedSystem.coe_natLERec] at ih
+    exact congrArg (f (m + k)) ih
+
+/-- Iterated composition over a reflexive natural-number interval is the identity. -/
+@[simp]
+theorem natLERec_self (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
+    natLERec f n n le_rfl x = x := by
+  simp [natLERec, Nat.leRecOn_self]
+
+/-- Iterated composition over one successor step is the supplied elementary embedding. -/
+@[simp]
+theorem natLERec_succ (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
+    natLERec f n (n + 1) (Nat.le_succ n) x = f n x := by
+  simp [natLERec, Nat.leRecOn]
+
+/-- Iterated elementary embeddings compose coherently across adjacent intervals. -/
+theorem natLERec_trans {f : ∀ n, M n ↪ₑ[L] M (n + 1)}
+    {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : M i) :
+    natLERec f j k hjk (natLERec f i j hij x) = natLERec f i k (hij.trans hjk) x := by
+  simpa only [coe_natLERec] using
+    DirectedSystem.map_map
+      (fun i j h ↦ DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) i j h) hij hjk x
+
+end ElementaryEmbedding
+
+namespace ElementaryChain
+
+variable {L : Language.{u, v}} {ι : Type w} [Preorder ι]
+
+/-- Construct a countable elementary chain by composing elementary embeddings between successive
+stages. -/
+noncomputable def ofNatSucc (M : ℕ → Type w') [∀ n, L.Structure (M n)]
+    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) : ElementaryChain L ℕ where
+  carrier := M
+  map := ElementaryEmbedding.natLERec f
+  map_self := ElementaryEmbedding.natLERec_self f
+  map_map := fun _ _ _ hij hjk x ↦ ElementaryEmbedding.natLERec_trans hij hjk x
+
+/-- The transition map of `ofNatSucc` between successive stages is the supplied elementary
+embedding. -/
+@[simp]
+theorem ofNatSucc_map_succ (M : ℕ → Type w') [∀ n, L.Structure (M n)]
+    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) :
+    (ofNatSucc M f).map n (n + 1) (Nat.le_succ n) = f n := by
+  ext x
+  exact ElementaryEmbedding.natLERec_succ f n x
+
+/-- The underlying first-order embeddings form a directed system. -/
+instance toEmbeddingDirectedSystem (C : ElementaryChain L ι) :
+    DirectedSystem C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) where
+  map_self i x := C.map_self i x
+  map_map k j i hij hjk x := C.map_map i j k hij hjk x
+
+variable [IsDirectedOrder ι]
+
+/-- The abstract union of an elementary chain, constructed without an ambient structure. -/
+abbrev Limit (C : ElementaryChain L ι) :=
+  L.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding)
+
+variable [Nonempty ι]
+
+/-- The canonical first-order embedding of a stage into the direct limit. -/
+noncomputable def toLimit (C : ElementaryChain L ι) (i : ι) : C.carrier i ↪[L] C.Limit :=
+  DirectLimit.of L ι C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) i
+
+/-- The canonical maps commute with the transition maps. -/
+@[simp]
+theorem toLimit_map (C : ElementaryChain L ι) {i j : ι} (hij : i ≤ j) (x : C.carrier i) :
+    C.toLimit j (C.map i j hij x) = C.toLimit i x := by
+  unfold toLimit
+  exact DirectLimit.of_f
+
+/-- Every element of the direct limit is represented by an element of some stage. -/
+theorem exists_toLimit (C : ElementaryChain L ι) (z : C.Limit) :
+    ∃ (i : ι) (x : C.carrier i), C.toLimit i x = z := by
+  simpa [toLimit] using DirectLimit.exists_of z
+
+private def limitEquiv (C : ElementaryChain L ι) :
+    C.Limit ≃
+      _root_.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) :=
+  Quotient.congrRight fun _ _ ↦ Iff.rfl
+
+omit [Nonempty ι] in
+/-- An infinite cardinal bounding the index type and every stage also bounds the limit. -/
+theorem mk_limit_le_of_lift_mk_le (C : ElementaryChain L ι) {κ : Cardinal.{max w w'}}
+    (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w'} #ι ≤ κ)
+    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) ≤ κ) :
+    #(C.Limit) ≤ κ := by
+  rw [(limitEquiv C).cardinal_eq]
+  exact _root_.DirectLimit.mk_le_of_aleph0_le
+    (fun i j h ↦ (C.map i j h).toEmbedding) κ hκ hι hC
+
+/-- If every stage has cardinality `κ` and the index type has cardinality at most `κ`, then the
+limit also has cardinality `κ`. -/
+theorem mk_limit_eq_of_forall_lift_mk_eq (C : ElementaryChain L ι)
+    (κ : Cardinal.{max w w'}) (hι : Cardinal.lift.{w'} #ι ≤ κ)
+    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) = κ) :
+    #(C.Limit) = κ := by
+  rw [(limitEquiv C).cardinal_eq]
+  apply _root_.DirectLimit.mk_eq_of_forall_lift_mk_eq
+    (fun i j h ↦ (C.map i j h).toEmbedding) κ hι hC
+  exact _root_.DirectLimit.mk_injective _ fun i j h ↦ (C.map i j h).injective
+
+/-- Realization of bounded formulas is preserved and reflected by a canonical map into the direct
+limit. -/
+theorem realize_toLimit (C : ElementaryChain L ι) {α : Type*} {n : ℕ}
+    (φ : L.BoundedFormula α n) (i : ι) (v : α → C.carrier i)
+    (xs : Fin n → C.carrier i) :
+    φ.Realize (C.toLimit i ∘ v) (C.toLimit i ∘ xs) ↔ φ.Realize v xs := by
+  induction φ generalizing i with
+  | falsum => rfl
+  | equal t₁ t₂ =>
+    simp [BoundedFormula.Realize, ← Sum.comp_elim]
+  | rel R ts =>
+    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
+    exact StrongHomClass.map_rel (C.toLimit i) R
+      (fun i ↦ Term.realize (Sum.elim v xs) (ts i))
+  | imp φ ψ ihφ ihψ =>
+    simp [BoundedFormula.Realize, ihφ, ihψ]
+  | @all n φ ih =>
+    simp only [BoundedFormula.realize_all, Nat.succ_eq_add_one]
+    constructor <;> intro h x
+    · simpa [← Fin.comp_snoc, ih i v (Fin.snoc xs x)] using h (C.toLimit i x)
+    · obtain ⟨j, xj, rfl⟩ := C.exists_toLimit x
+      obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
+      rw [← BoundedFormula.Realize,
+        ← (C.map i k hik).map_boundedFormula φ.all v xs, BoundedFormula.Realize] at h
+      specialize h (C.map j k hjk xj)
+      specialize ih k (C.map i k hik ∘ v)
+        (Fin.snoc (C.map i k hik ∘ xs) (C.map j k hjk xj))
+      rw [← ih, Fin.comp_snoc] at h
+      convert h using 1 <;> simp [Function.comp_def, C.toLimit_map]
+
+/-- The canonical map from each stage to the direct limit is elementary. -/
+noncomputable def toLimitElementary (C : ElementaryChain L ι) (i : ι) :
+    C.carrier i ↪ₑ[L] C.Limit where
+  toFun := C.toLimit i
+  map_formula' := fun n φ v ↦ by
+    change BoundedFormula.Realize φ (C.toLimit i ∘ v) default ↔
+      BoundedFormula.Realize φ v default
+    convert C.realize_toLimit φ i v default
+
+/-- A finite family of elements of the direct limit can be lifted to a common stage of the chain.
+-/
+theorem exists_finite_common_stage (C : ElementaryChain L ι) {α : Type*} [Finite α]
+    (x : α → C.Limit) : ∃ (i : ι) (z : α → C.carrier i), C.toLimit i ∘ z = x := by
+  obtain ⟨i, z, hz⟩ := DirectLimit.exists_quotient_mk'_sigma_mk'_eq C.carrier
+    (fun i j h ↦ (C.map i j h).toEmbedding) x
+  exact ⟨i, z, by simpa [toLimit, Function.comp_def] using hz.symm⟩
+
+/-- A compatible cocone of elementary embeddings induces an elementary embedding from the direct
+limit. This is the elementary version of `Language.DirectLimit.lift`. -/
+noncomputable def liftElementary (C : ElementaryChain L ι) {P : Type*} [L.Structure P]
+    (g : ∀ i, C.carrier i ↪ₑ[L] P)
+    (comm : ∀ i j (hij : i ≤ j) (x : C.carrier i), g j (C.map i j hij x) = g i x) :
+    C.Limit ↪ₑ[L] P :=
+  let F : C.Limit ↪[L] P := Language.DirectLimit.lift L ι C.carrier
+    (fun i j h ↦ (C.map i j h).toEmbedding)
+    (fun i ↦ (g i).toEmbedding)
+    (by intro i j hij x; simpa using comm i j hij x)
+  { toFun := F
+    map_formula' := by
+      intro n φ x
+      obtain ⟨i, z, hz⟩ := C.exists_finite_common_stage x
+      have hF_lift : ∀ a : C.carrier i, F (C.toLimit i a) = g i a := by
+        intro a
+        simp [F, toLimit]
+      have h_eq : F ∘ x = (g i : C.carrier i → P) ∘ z := by
+        ext k
+        calc
+          F (x k) = F (C.toLimit i (z k)) := by simp [← hz]
+          _ = g i (z k) := hF_lift (z k)
+      rw [h_eq]
+      exact ((g i).map_formula' φ z).trans <| by
+        rw [← hz]
+        exact ((C.toLimitElementary i).map_formula' φ z).symm }
+
+/-- If some stage is a model of `T`, then the direct limit is also a model of `T`. -/
+theorem limit_models (C : ElementaryChain L ι) (T : L.Theory)
+    (hT : ∃ i, C.carrier i ⊨ T) : C.Limit ⊨ T := by
+  obtain ⟨i, hi⟩ := hT
+  exact ((C.toLimitElementary i).theory_model_iff T).1 hi
+
+end ElementaryChain
+
+end Language
+
+end FirstOrder
diff --git a/Mathlib/Order/DirectedInverseSystem.lean b/Mathlib/Order/DirectedInverseSystem.lean
index 468e2e921a06d6..d70ce590de1c6e 100644
--- a/Mathlib/Order/DirectedInverseSystem.lean
+++ b/Mathlib/Order/DirectedInverseSystem.lean
@@ -185,6 +185,17 @@ theorem lift_injective (h : ∀ i, Function.Injective (ih i)) :
 
 end lift
 
+/-- If `m` is an upper bound for the index type, then the direct limit is equivalent to the
+component at `m`. -/
+def equivOfForallLE (m : ι) (hm : ∀ i, i ≤ m) : DirectLimit F f ≃ F m where
+  toFun := DirectLimit.lift f (fun i x ↦ f i m (hm i) x) (by simp [map_map'])
+  invFun := fun x ↦ ⟦⟨m,x⟩⟧
+  left_inv := by
+    intro z
+    induction z using DirectLimit.induction with
+    | _ i x => simp only [lift_def, mk_apply]
+  right_inv := fun _ ↦ by simp only [lift_def, map_self']
+
 section map
 
 variable (ih : ∀ i, F₁ i → F₂ i) (compat : ∀ i j h x, f₂ i j h (ih i x) = ih j (f₁ i j h x))
diff --git a/Mathlib/SetTheory/Cardinal/DirectLimit.lean b/Mathlib/SetTheory/Cardinal/DirectLimit.lean
new file mode 100644
index 00000000000000..030c453fe309cd
--- /dev/null
+++ b/Mathlib/SetTheory/Cardinal/DirectLimit.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Zikang Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zikang Yu
+-/
+module
+
+public import Mathlib.Data.Fintype.Order
+public import Mathlib.Order.DirectedInverseSystem
+public import Mathlib.SetTheory.Cardinal.Arithmetic
+
+/-!
+# Cardinality of direct limits
+
+This file gives upper and lower bounds for the cardinality of a direct limit of types.
+
+## Main statements
+
+* `DirectLimit.mk_le_sum`: the cardinality of a direct limit is at most the sum of the
+  cardinalities of its components.
+* `DirectLimit.mk_le_of_aleph0_le`: an infinite common bound for the index type and the
+  components is also a bound for the direct limit.
+* `DirectLimit.iSup_lift_mk_le_mk`: when the canonical maps are injective, the supremum of the
+  component cardinalities is at most the cardinality of the direct limit.
+* `DirectLimit.mk_eq_iSup_lift_mk`: when that supremum is greater than the cardinality of the
+  index type and the canonical maps are injective, it equals the cardinality of the direct limit.
+* `DirectLimit.mk_eq_of_forall_lift_mk_eq`: when all components have the same cardinality, under
+  the corresponding bound and injectivity assumptions, so does the direct limit.
+-/
+
+@[expose] public section
+
+open Cardinal Function
+
+universe u v w
+
+namespace DirectLimit
+
+variable {ι : Type u} [Preorder ι] {F : ι → Type v}
+variable {T : ∀ ⦃i j : ι⦄, i ≤ j → Sort w} (f : ∀ i j (h : i ≤ j), T h)
+variable [∀ ⦃i j⦄ (h : i ≤ j), FunLike (T h) (F i) (F j)]
+variable [DirectedSystem F (f · · ·)] [IsDirectedOrder ι]
+
+/-- The cardinality of a direct limit is at most the sum of the cardinalities of its
+components. -/
+theorem mk_le_sum : #(DirectLimit F (f · · ·)) ≤ Cardinal.sum fun i ↦ #(F i) :=
+  mk_quotient_le.trans_eq (mk_sigma F)
+
+/-- An infinite cardinal that bounds the cardinality of the index type and all components also
+bounds the cardinality of the direct limit. -/
+theorem mk_le_of_aleph0_le (c : Cardinal.{max u v}) (hc : ℵ₀ ≤ c)
+    (hι : Cardinal.lift.{v} #ι ≤ c) (hF : ∀ i, Cardinal.lift.{u} #(F i) ≤ c) :
+    #(DirectLimit F (f · · ·)) ≤ c :=
+  (mk_le_sum f).trans <| (sum_le_lift_mk_mul_iSup_lift _).trans <|
+    Cardinal.mul_le_of_le hc hι (ciSup_le' hF)
+
+/-- If all canonical maps into a direct limit are injective, then the supremum of the
+cardinalities of the components is at most the cardinality of the direct limit. -/
+theorem iSup_lift_mk_le_mk
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    (⨆ i, Cardinal.lift.{u} #(F i)) ≤ #(DirectLimit F (f · · ·)) := by
+  refine ciSup_le' fun i ↦ ?_
+  have := lift_mk_le_lift_mk_of_injective (h i)
+  simp [DirectLimit]
+  rwa [Cardinal.lift_umax, Cardinal.lift_id'.{v,u}] at this
+
+/-- If all canonical maps into a direct limit are injective and the supremum of the component
+cardinalities is greater than the cardinality of the index type, then it equals the cardinality
+of the direct limit. -/
+theorem mk_eq_iSup_lift_mk
+    (hι : Cardinal.lift.{v} #ι ≤ ⨆ i, Cardinal.lift.{u} #(F i))
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    #(DirectLimit F (f · · ·)) = ⨆ i, Cardinal.lift.{u} #(F i) := by
+  refine le_antisymm ?_ (iSup_lift_mk_le_mk f h)
+  by_cases! hc : ℵ₀ ≤ ⨆ i, lift.{u, v} #(F i)
+  · exact mk_le_of_aleph0_le f _ hc hι fun i ↦ le_ciSup Cardinal.bddAbove_of_small i
+  · haveI : Finite ι := mk_lt_aleph0_iff.mp (lift_lt_aleph0.mp (hι.trans_lt hc))
+    cases isEmpty_or_nonempty ι with
+    | inl hle =>
+      simp
+    | inr hlne =>
+      obtain ⟨m, hm⟩ := Finite.exists_le (id : ι → ι)
+      have he := (equivOfForallLE f m hm).lift_cardinal_eq
+      rw [Cardinal.lift_id'.{v,u}, Cardinal.lift_umax.{v,u}] at he
+      rw [he]
+      exact le_ciSup Cardinal.bddAbove_of_small m
+
+/-- If all components have the same cardinality `c`, the cardinality of the index type is at most
+`c`, and all canonical maps are injective, then the direct limit also has cardinality `c`. -/
+theorem mk_eq_of_forall_lift_mk_eq [Nonempty ι] (c : Cardinal.{max u v})
+    (hι : Cardinal.lift.{v} #ι ≤ c) (hF : ∀ i, Cardinal.lift.{u} #(F i) = c)
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    #(DirectLimit F (f · · ·)) = c := by
+  simpa only [hF, ciSup_const] using
+    mk_eq_iSup_lift_mk f (by simpa only [hF, ciSup_const]) h
+
+end DirectLimit