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 ) ) |
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 ) ) |