Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | f1otrkg.p | |
|
f1otrkg.d | |
||
f1otrkg.i | |
||
f1otrkg.b | |
||
f1otrkg.e | |
||
f1otrkg.j | |
||
f1otrkg.f | |
||
f1otrkg.1 | |
||
f1otrkg.2 | |
||
f1otrgitv.x | |
||
f1otrgitv.y | |
||
Assertion | f1otrgds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1otrkg.p | |
|
2 | f1otrkg.d | |
|
3 | f1otrkg.i | |
|
4 | f1otrkg.b | |
|
5 | f1otrkg.e | |
|
6 | f1otrkg.j | |
|
7 | f1otrkg.f | |
|
8 | f1otrkg.1 | |
|
9 | f1otrkg.2 | |
|
10 | f1otrgitv.x | |
|
11 | f1otrgitv.y | |
|
12 | 8 | ralrimivva | |
13 | oveq1 | |
|
14 | fveq2 | |
|
15 | 14 | oveq1d | |
16 | 13 15 | eqeq12d | |
17 | oveq2 | |
|
18 | fveq2 | |
|
19 | 18 | oveq2d | |
20 | 17 19 | eqeq12d | |
21 | 16 20 | rspc2v | |
22 | 10 11 21 | syl2anc | |
23 | 12 22 | mpd | |