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

Step

Hyp

Ref

Expression

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

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

1 2

sseqtrrid

 |-  ( N e. _om -> ( Fmla ` N ) C_ ( Fmla ` suc N ) )