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 e. _om -> ( Fmla ` N ) C_ ( Fmla ` suc N ) )

Proof

Step Hyp Ref Expression
1 ssun1
 |-  ( Fmla ` N ) C_ ( ( Fmla ` N ) u. { x | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } )
2 fmlasuc
 |-  ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { x | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) )
3 1 2 sseqtrrid
 |-  ( N e. _om -> ( Fmla ` N ) C_ ( Fmla ` suc N ) )