Step |
Hyp |
Ref |
Expression |
1 |
|
relexpsucrd.1 |
|- ( ph -> Rel R ) |
2 |
|
relexpsucrd.2 |
|- ( ph -> N e. NN0 ) |
3 |
|
simpr |
|- ( ( ph /\ R e. _V ) -> R e. _V ) |
4 |
1
|
adantr |
|- ( ( ph /\ R e. _V ) -> Rel R ) |
5 |
2
|
adantr |
|- ( ( ph /\ R e. _V ) -> N e. NN0 ) |
6 |
|
relexpsucr |
|- ( ( R e. _V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) |
7 |
3 4 5 6
|
syl3anc |
|- ( ( ph /\ R e. _V ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) |
8 |
7
|
ex |
|- ( ph -> ( R e. _V -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) ) |
9 |
|
reldmrelexp |
|- Rel dom ^r |
10 |
9
|
ovprc1 |
|- ( -. R e. _V -> ( R ^r ( N + 1 ) ) = (/) ) |
11 |
9
|
ovprc1 |
|- ( -. R e. _V -> ( R ^r N ) = (/) ) |
12 |
11
|
coeq1d |
|- ( -. R e. _V -> ( ( R ^r N ) o. R ) = ( (/) o. R ) ) |
13 |
|
co01 |
|- ( (/) o. R ) = (/) |
14 |
12 13
|
eqtr2di |
|- ( -. R e. _V -> (/) = ( ( R ^r N ) o. R ) ) |
15 |
10 14
|
eqtrd |
|- ( -. R e. _V -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) |
16 |
8 15
|
pm2.61d1 |
|- ( ph -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) |