Step |
Hyp |
Ref |
Expression |
1 |
|
rtrclind.1 |
|- ( et -> Rel R ) |
2 |
|
rtrclind.2 |
|- ( et -> S e. V ) |
3 |
|
rtrclind.3 |
|- ( et -> X e. W ) |
4 |
|
rtrclind.4 |
|- ( i = S -> ( ph <-> ch ) ) |
5 |
|
rtrclind.5 |
|- ( i = x -> ( ph <-> ps ) ) |
6 |
|
rtrclind.6 |
|- ( i = j -> ( ph <-> th ) ) |
7 |
|
rtrclind.7 |
|- ( x = X -> ( ps <-> ta ) ) |
8 |
|
rtrclind.8 |
|- ( et -> ch ) |
9 |
|
rtrclind.9 |
|- ( et -> ( j R x -> ( th -> ps ) ) ) |
10 |
1
|
dfrtrcl2 |
|- ( et -> ( t* ` R ) = ( t*rec ` R ) ) |
11 |
1
|
dfrtrclrec2 |
|- ( et -> ( S ( t*rec ` R ) X <-> E. n e. NN0 S ( R ^r n ) X ) ) |
12 |
11
|
biimpac |
|- ( ( S ( t*rec ` R ) X /\ et ) -> E. n e. NN0 S ( R ^r n ) X ) |
13 |
|
simprl |
|- ( ( S ( t*rec ` R ) X /\ ( et /\ ( S ( R ^r n ) X /\ n e. NN0 ) ) ) -> et ) |
14 |
|
simprrr |
|- ( ( S ( t*rec ` R ) X /\ ( et /\ ( S ( R ^r n ) X /\ n e. NN0 ) ) ) -> n e. NN0 ) |
15 |
|
simprrl |
|- ( ( S ( t*rec ` R ) X /\ ( et /\ ( S ( R ^r n ) X /\ n e. NN0 ) ) ) -> S ( R ^r n ) X ) |
16 |
1 2 3 4 5 6 7 8 9
|
relexpind |
|- ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) |
17 |
13 14 15 16
|
syl3c |
|- ( ( S ( t*rec ` R ) X /\ ( et /\ ( S ( R ^r n ) X /\ n e. NN0 ) ) ) -> ta ) |
18 |
17
|
anassrs |
|- ( ( ( S ( t*rec ` R ) X /\ et ) /\ ( S ( R ^r n ) X /\ n e. NN0 ) ) -> ta ) |
19 |
18
|
expcom |
|- ( ( S ( R ^r n ) X /\ n e. NN0 ) -> ( ( S ( t*rec ` R ) X /\ et ) -> ta ) ) |
20 |
19
|
expcom |
|- ( n e. NN0 -> ( S ( R ^r n ) X -> ( ( S ( t*rec ` R ) X /\ et ) -> ta ) ) ) |
21 |
20
|
rexlimiv |
|- ( E. n e. NN0 S ( R ^r n ) X -> ( ( S ( t*rec ` R ) X /\ et ) -> ta ) ) |
22 |
12 21
|
mpcom |
|- ( ( S ( t*rec ` R ) X /\ et ) -> ta ) |
23 |
22
|
expcom |
|- ( et -> ( S ( t*rec ` R ) X -> ta ) ) |
24 |
|
breq |
|- ( ( t* ` R ) = ( t*rec ` R ) -> ( S ( t* ` R ) X <-> S ( t*rec ` R ) X ) ) |
25 |
24
|
imbi1d |
|- ( ( t* ` R ) = ( t*rec ` R ) -> ( ( S ( t* ` R ) X -> ta ) <-> ( S ( t*rec ` R ) X -> ta ) ) ) |
26 |
23 25
|
syl5ibr |
|- ( ( t* ` R ) = ( t*rec ` R ) -> ( et -> ( S ( t* ` R ) X -> ta ) ) ) |
27 |
10 26
|
mpcom |
|- ( et -> ( S ( t* ` R ) X -> ta ) ) |