Metamath Proof Explorer


Theorem fmla

Description: The set of all valid Godel formulas. (Contributed by AV, 20-Sep-2023)

Ref Expression
Assertion fmla
|- ( Fmla ` _om ) = U_ n e. _om ( Fmla ` n )

Proof

Step Hyp Ref Expression
1 df-fmla
 |-  Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )
2 1 fveq1i
 |-  ( Fmla ` _om ) = ( ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) ` _om )
3 omex
 |-  _om e. _V
4 eqidd
 |-  ( _om e. _V -> ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) )
5 fveq2
 |-  ( n = _om -> ( ( (/) Sat (/) ) ` n ) = ( ( (/) Sat (/) ) ` _om ) )
6 5 dmeqd
 |-  ( n = _om -> dom ( ( (/) Sat (/) ) ` n ) = dom ( ( (/) Sat (/) ) ` _om ) )
7 6 adantl
 |-  ( ( _om e. _V /\ n = _om ) -> dom ( ( (/) Sat (/) ) ` n ) = dom ( ( (/) Sat (/) ) ` _om ) )
8 sucidg
 |-  ( _om e. _V -> _om e. suc _om )
9 fvex
 |-  ( ( (/) Sat (/) ) ` _om ) e. _V
10 9 dmex
 |-  dom ( ( (/) Sat (/) ) ` _om ) e. _V
11 10 a1i
 |-  ( _om e. _V -> dom ( ( (/) Sat (/) ) ` _om ) e. _V )
12 4 7 8 11 fvmptd
 |-  ( _om e. _V -> ( ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) ` _om ) = dom ( ( (/) Sat (/) ) ` _om ) )
13 3 12 ax-mp
 |-  ( ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) ` _om ) = dom ( ( (/) Sat (/) ) ` _om )
14 3 sucid
 |-  _om e. suc _om
15 satf0sucom
 |-  ( _om e. suc _om -> ( ( (/) Sat (/) ) ` _om ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` _om ) )
16 14 15 ax-mp
 |-  ( ( (/) Sat (/) ) ` _om ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` _om )
17 limom
 |-  Lim _om
18 rdglim2a
 |-  ( ( _om e. _V /\ Lim _om ) -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` _om ) = U_ n e. _om ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) )
19 3 17 18 mp2an
 |-  ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` _om ) = U_ n e. _om ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n )
20 16 19 eqtri
 |-  ( ( (/) Sat (/) ) ` _om ) = U_ n e. _om ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n )
21 20 dmeqi
 |-  dom ( ( (/) Sat (/) ) ` _om ) = dom U_ n e. _om ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n )
22 dmiun
 |-  dom U_ n e. _om ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) = U_ n e. _om dom ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n )
23 elelsuc
 |-  ( n e. _om -> n e. suc _om )
24 fmlafv
 |-  ( n e. suc _om -> ( Fmla ` n ) = dom ( ( (/) Sat (/) ) ` n ) )
25 23 24 syl
 |-  ( n e. _om -> ( Fmla ` n ) = dom ( ( (/) Sat (/) ) ` n ) )
26 satf0sucom
 |-  ( n e. suc _om -> ( ( (/) Sat (/) ) ` n ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) )
27 23 26 syl
 |-  ( n e. _om -> ( ( (/) Sat (/) ) ` n ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) )
28 27 dmeqd
 |-  ( n e. _om -> dom ( ( (/) Sat (/) ) ` n ) = dom ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) )
29 25 28 eqtr2d
 |-  ( n e. _om -> dom ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) = ( Fmla ` n ) )
30 29 iuneq2i
 |-  U_ n e. _om dom ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` n ) = U_ n e. _om ( Fmla ` n )
31 21 22 30 3eqtri
 |-  dom ( ( (/) Sat (/) ) ` _om ) = U_ n e. _om ( Fmla ` n )
32 2 13 31 3eqtri
 |-  ( Fmla ` _om ) = U_ n e. _om ( Fmla ` n )