L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S) ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S) ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
refine'
  ⟨fun h =>
    ⟨⟨L[[α]].completeTheory h.some, (subset_union_left _ S).trans completeTheory.subset,
        completeTheory.isMaximal (L[[α]]) h.some⟩,
      (subset_union_right ((L.lhomWithConstants α).onTheory T) _).trans completeTheory.subset⟩,
    _⟩
case intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
p : CompleteType T α
hp : p ∈ {p | S ⊆ ↑p}
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
rintro ⟨p, hp⟩
no goals
case intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
p : CompleteType T α
hp : p ∈ {p | S ⊆ ↑p}
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
exact p.isMaximal.1.mono (union_subset p.subset hp)