exact ⟨y, lt_of_mem_rng hy, hy, fun y' _ h' ↦ uniq y' h'⟩
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
hm : IsMapping m
x : M
hx : x ∈ domain m
y : M
hy : ⟪x, y⟫ ∈ m
uniq : ∀ (y_1 : M), (fun y => ⟪x, y⟫ ∈ m) y_1 → y_1 = y
⊢ ∃ y < m, ⟪x, y⟫ ∈ m ∧ ∀ y' < m, ⟪x, y'⟫ ∈ m → y' = y
no goals