Metamath Proof Explorer

Theorem isfmlasuc

Description: The characterization of a Godel formula of height at least 1. (Contributed by AV, 14-Oct-2023)

Ref Expression
Assertion isfmlasuc 
|- ( ( N e. _om /\ F e. V ) -> ( F e. ( Fmla ` suc N ) <-> ( F e. ( Fmla ` N ) \/ E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) ) )

Proof

Step Hyp Ref Expression
1 fmlasuc 
 |-  ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) )
2 1 adantr 
 |-  ( ( N e. _om /\ F e. V ) -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) )
3 2 eleq2d 
 |-  ( ( N e. _om /\ F e. V ) -> ( F e. ( Fmla ` suc N ) <-> F e. ( ( Fmla ` N ) u. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) ) )
4 elun 
 |-  ( F e. ( ( Fmla ` N ) u. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) <-> ( F e. ( Fmla ` N ) \/ F e. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) )
5 4 a1i 
 |-  ( ( N e. _om /\ F e. V ) -> ( F e. ( ( Fmla ` N ) u. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) <-> ( F e. ( Fmla ` N ) \/ F e. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) ) )
6 eqeq1 
 |-  ( f = F -> ( f = ( u |g v ) <-> F = ( u |g v ) ) )
7 6 rexbidv 
 |-  ( f = F -> ( E. v e. ( Fmla ` N ) f = ( u |g v ) <-> E. v e. ( Fmla ` N ) F = ( u |g v ) ) )
8 eqeq1 
 |-  ( f = F -> ( f = A.g i u <-> F = A.g i u ) )
9 8 rexbidv 
 |-  ( f = F -> ( E. i e. _om f = A.g i u <-> E. i e. _om F = A.g i u ) )
10 7 9 orbi12d 
 |-  ( f = F -> ( ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) <-> ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) )
11 10 rexbidv 
 |-  ( f = F -> ( E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) <-> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) )
12 11 elabg 
 |-  ( F e. V -> ( F e. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } <-> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) )
13 12 adantl 
 |-  ( ( N e. _om /\ F e. V ) -> ( F e. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } <-> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) )
14 13 orbi2d 
 |-  ( ( N e. _om /\ F e. V ) -> ( ( F e. ( Fmla ` N ) \/ F e. { f | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) f = ( u |g v ) \/ E. i e. _om f = A.g i u ) } ) <-> ( F e. ( Fmla ` N ) \/ E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) ) )
15 3 5 14 3bitrd 
 |-  ( ( N e. _om /\ F e. V ) -> ( F e. ( Fmla ` suc N ) <-> ( F e. ( Fmla ` N ) \/ E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) F = ( u |g v ) \/ E. i e. _om F = A.g i u ) ) ) )