exact Set.eq_empty_iff_forall_not_mem.mp l₅ x ⟨l₆,l₄⟩
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
l₅ : lindenbaumExtension t (generatedDisjunctions x) ∩ generatedDisjunctions x = ∅
l₆ : x ∈ lindenbaumExtension t (generatedDisjunctions x)
⊢ False
no goals