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