Step |
Hyp |
Ref |
Expression |
1 |
|
relexpind.1 |
|- ( et -> Rel R ) |
2 |
|
relexpind.2 |
|- ( et -> S e. V ) |
3 |
|
relexpind.3 |
|- ( et -> X e. W ) |
4 |
|
relexpind.4 |
|- ( i = S -> ( ph <-> ch ) ) |
5 |
|
relexpind.5 |
|- ( i = x -> ( ph <-> ps ) ) |
6 |
|
relexpind.6 |
|- ( i = j -> ( ph <-> th ) ) |
7 |
|
relexpind.7 |
|- ( x = X -> ( ps <-> ta ) ) |
8 |
|
relexpind.8 |
|- ( et -> ch ) |
9 |
|
relexpind.9 |
|- ( et -> ( j R x -> ( th -> ps ) ) ) |
10 |
|
breq2 |
|- ( x = X -> ( S ( R ^r n ) x <-> S ( R ^r n ) X ) ) |
11 |
10
|
imbi1d |
|- ( x = X -> ( ( S ( R ^r n ) x -> ta ) <-> ( S ( R ^r n ) X -> ta ) ) ) |
12 |
11
|
imbi2d |
|- ( x = X -> ( ( n e. NN0 -> ( S ( R ^r n ) x -> ta ) ) <-> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) |
13 |
12
|
imbi2d |
|- ( x = X -> ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ta ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) ) |
14 |
|
imbi2 |
|- ( ( ps <-> ta ) -> ( ( S ( R ^r n ) x -> ps ) <-> ( S ( R ^r n ) x -> ta ) ) ) |
15 |
14
|
imbi2d |
|- ( ( ps <-> ta ) -> ( ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) <-> ( n e. NN0 -> ( S ( R ^r n ) x -> ta ) ) ) ) |
16 |
15
|
imbi2d |
|- ( ( ps <-> ta ) -> ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ta ) ) ) ) ) |
17 |
16
|
bibi1d |
|- ( ( ps <-> ta ) -> ( ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) <-> ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ta ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) ) ) |
18 |
13 17
|
syl5ibr |
|- ( ( ps <-> ta ) -> ( x = X -> ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) ) ) |
19 |
7 18
|
mpcom |
|- ( x = X -> ( ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) <-> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) ) |
20 |
1 2 4 5 6 8 9
|
relexpindlem |
|- ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) ) |
21 |
19 20
|
vtoclg |
|- ( X e. W -> ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) ) |
22 |
3 21
|
mpcom |
|- ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) ) |