Theorem: LO.FirstOrder.Arith.Theory.iSigma₀_subset_EA (Logic/FirstOrder/Arith/EA/Basic.lean)

State before:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐈𝚺₀ ⊆ 𝐄𝐀
Tactic:
simp only [Theory.iSigma, Theory.indH, Theory.add_def, Set.image_union, Set.union_assoc]
State after:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪
      ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy 𝚺 0) ⊆
    ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪ (𝐄𝐗𝐏 ∪ indScheme ℒₒᵣ(exp) (Hierarchy 𝚺 0))

State before:
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪
      ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy 𝚺 0) ⊆
    ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪ (𝐄𝐗𝐏 ∪ indScheme ℒₒᵣ(exp) (Hierarchy 𝚺 0))
Tactic:
exact Set.union_subset_union_right _ (Set.subset_union_of_subset_right Theory.coe_indH_subset_indH _)
State after:
no goals