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	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ 𝑁 ) ⊆ ( Fmla ‘ suc 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ ( Fmla ‘ 𝑁 ) ⊆ ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } )
2		fmlasuc	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) )
3	1 2	sseqtrrid	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ 𝑁 ) ⊆ ( Fmla ‘ suc 𝑁 ) )