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 )