Metamath Proof Explorer

Theorem fmlasssuc

Description: The Godel formulas of height N are a subset of the Godel formulas of height N + 1 . (Contributed by AV, 20-Oct-2023)

Ref Expression
Assertion fmlasssuc ⊢ N ∈ ω → Fmla ⁡ N ⊆ Fmla ⁡ suc ⁡ N

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ Fmla ⁡ N ⊆ Fmla ⁡ N ∪ x | ∃ u ∈ Fmla ⁡ N ∃ v ∈ Fmla ⁡ N x = u ⊼ 𝑔 v ∨ ∃ i ∈ ω x = ∀ 𝑔 i u
2 fmlasuc ⊢ N ∈ ω → Fmla ⁡ suc ⁡ N = Fmla ⁡ N ∪ x | ∃ u ∈ Fmla ⁡ N ∃ v ∈ Fmla ⁡ N x = u ⊼ 𝑔 v ∨ ∃ i ∈ ω x = ∀ 𝑔 i u
3 1 2 sseqtrrid ⊢ N ∈ ω → Fmla ⁡ N ⊆ Fmla ⁡ suc ⁡ N