Step |
Hyp |
Ref |
Expression |
1 |
|
naryfval.i |
|
2 |
|
simpr |
|
3 |
|
oveq2 |
|
4 |
3 1
|
eqtr4di |
|
5 |
4
|
adantr |
|
6 |
2 5
|
oveq12d |
|
7 |
2 6
|
oveq12d |
|
8 |
|
df-naryf |
Could not format -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) : No typesetting found for |- -aryF = ( n e. NN0 , x e. _V |-> ( x ^m ( x ^m ( 0 ..^ n ) ) ) ) with typecode |- |
9 |
|
ovex |
|
10 |
7 8 9
|
ovmpoa |
Could not format ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |- |
11 |
10
|
ex |
Could not format ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) : No typesetting found for |- ( N e. NN0 -> ( X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) ) with typecode |- |
12 |
|
simpr |
|
13 |
|
df-naryf |
Could not format -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) : No typesetting found for |- -aryF = ( x e. NN0 , n e. _V |-> ( n ^m ( n ^m ( 0 ..^ x ) ) ) ) with typecode |- |
14 |
13
|
mpondm0 |
Could not format ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. ( N e. NN0 /\ X e. _V ) -> ( N -aryF X ) = (/) ) with typecode |- |
15 |
12 14
|
nsyl5 |
Could not format ( -. X e. _V -> ( N -aryF X ) = (/) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = (/) ) with typecode |- |
16 |
|
simpl |
|
17 |
|
df-map |
|
18 |
17
|
mpondm0 |
|
19 |
16 18
|
nsyl5 |
|
20 |
15 19
|
eqtr4d |
Could not format ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( -. X e. _V -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |- |
21 |
11 20
|
pm2.61d1 |
Could not format ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) : No typesetting found for |- ( N e. NN0 -> ( N -aryF X ) = ( X ^m ( X ^m I ) ) ) with typecode |- |