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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₁ = Ω₂
Tactic:
exact equality_def.mpr $ Set.eq_of_subset_of_subset
  (by intro p hp; exact h p hp)
  (by
    intro p;
    contrapose;
    intro hp;
    apply iff_mem_neg.mp;
    apply h;
    apply iff_mem_neg.mpr hp;
  )
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₁.theory ⊆ Ω₂.theory
Tactic:
intro p hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact h p hp
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
⊢ Ω₂.theory ⊆ Ω₁.theory
Tactic:
intro p
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → p ∈ Ω₁.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∈ Ω₂.theory → p ∈ Ω₁.theory
Tactic:
contrapose
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∉ Ω₁.theory → p ∉ Ω₂.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
⊢ p ∉ Ω₁.theory → p ∉ Ω₂.theory
Tactic:
intro hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ p ∉ Ω₂.theory
Tactic:
apply iff_mem_neg.mp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₂.theory
Tactic:
apply h
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₁.theory

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
h : ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
p : Formula α
hp : p ∉ Ω₁.theory
⊢ ~p ∈ Ω₁.theory
Tactic:
apply iff_mem_neg.mpr hp
State after:
no goals