Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.iff_mem_negneg (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~~p ∈ Ω.theory ↔ p ∈ Ω.theory
Tactic:
simp [membership_iff]
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ ↔ Ω.theory *⊢[L]! p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ ↔ Ω.theory *⊢[L]! p
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
. intro h; exact dne'! h;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
. intro h; exact dni'! h;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! p
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! p

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! p
Tactic:
exact dne'! h
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ω.theory *⊢[L]! p → Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω.theory *⊢[L]! p
⊢ Ω.theory *⊢[L]! (p ⟶ ⊥) ⟶ ⊥
Tactic:
exact dni'! h
State after:
no goals