Description: Lemma for cantnf . (Contributed by Mario Carneiro, 28-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cantnfs.s | |
|
cantnfs.a | |
||
cantnfs.b | |
||
oemapval.t | |
||
cantnf.c | |
||
cantnf.s | |
||
cantnf.e | |
||
Assertion | cantnflem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cantnfs.s | |
|
2 | cantnfs.a | |
|
3 | cantnfs.b | |
|
4 | oemapval.t | |
|
5 | cantnf.c | |
|
6 | cantnf.s | |
|
7 | cantnf.e | |
|
8 | oecl | |
|
9 | 2 3 8 | syl2anc | |
10 | onelon | |
|
11 | 9 5 10 | syl2anc | |
12 | ondif1 | |
|
13 | 11 7 12 | sylanbrc | |
14 | 13 | eldifbd | |
15 | ssel | |
|
16 | 5 15 | syl5com | |
17 | 14 16 | mtod | |
18 | oe0m | |
|
19 | 3 18 | syl | |
20 | difss | |
|
21 | 19 20 | eqsstrdi | |
22 | oveq1 | |
|
23 | 22 | sseq1d | |
24 | 21 23 | syl5ibrcom | |
25 | oe1m | |
|
26 | eqimss | |
|
27 | 3 25 26 | 3syl | |
28 | oveq1 | |
|
29 | 28 | sseq1d | |
30 | 27 29 | syl5ibrcom | |
31 | 24 30 | jaod | |
32 | 17 31 | mtod | |
33 | elpri | |
|
34 | df2o3 | |
|
35 | 33 34 | eleq2s | |
36 | 32 35 | nsyl | |
37 | 2 36 | eldifd | |
38 | 37 13 | jca | |