Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ackbij.f | |
|
Assertion | ackbij1lem12 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ackbij.f | |
|
2 | 1 | ackbij1lem10 | |
3 | 1 | ackbij1lem11 | |
4 | ffvelcdm | |
|
5 | 2 3 4 | sylancr | |
6 | difssd | |
|
7 | 1 | ackbij1lem11 | |
8 | 6 7 | syldan | |
9 | ffvelcdm | |
|
10 | 2 8 9 | sylancr | |
11 | nnaword1 | |
|
12 | 5 10 11 | syl2anc | |
13 | disjdif | |
|
14 | 13 | a1i | |
15 | 1 | ackbij1lem9 | |
16 | 3 8 14 15 | syl3anc | |
17 | undif | |
|
18 | 17 | biimpi | |
19 | 18 | adantl | |
20 | 19 | fveq2d | |
21 | 16 20 | eqtr3d | |
22 | 12 21 | sseqtrd | |