Description: Lemma for isfin3-2 . Remove hypotheses from isf32lem10 . (Contributed by Stefan O'Rear, 17-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | isf32lem11 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | suceq | |
|
3 | 2 | fveq2d | |
4 | fveq2 | |
|
5 | 3 4 | sseq12d | |
6 | 5 | cbvralvw | |
7 | 6 | biimpi | |
8 | 7 | 3ad2ant2 | |
9 | simp3 | |
|
10 | suceq | |
|
11 | 10 | fveq2d | |
12 | fveq2 | |
|
13 | 11 12 | psseq12d | |
14 | 13 | cbvrabv | |
15 | eqid | |
|
16 | eqid | |
|
17 | eqid | |
|
18 | 1 8 9 14 15 16 17 | isf32lem10 | |
19 | 18 | impcom | |