Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ackbij.f | |
|
ackbij.g | |
||
Assertion | ackbij2lem4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ackbij.f | |
|
2 | ackbij.g | |
|
3 | fveq2 | |
|
4 | 3 | sseq2d | |
5 | fveq2 | |
|
6 | 5 | sseq2d | |
7 | fveq2 | |
|
8 | 7 | sseq2d | |
9 | fveq2 | |
|
10 | 9 | sseq2d | |
11 | ssidd | |
|
12 | 1 2 | ackbij2lem3 | |
13 | 12 | ad2antrr | |
14 | sstr2 | |
|
15 | 13 14 | syl5com | |
16 | 4 6 8 10 11 15 | findsg | |