L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | φ ∈ p} = Set.univ ↔ LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]
no goals
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
simp