apply hSur
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h✝ : ¬F₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ w₁, f w₁ = w₂
no goals