Description: Lemma for nosepne . (Contributed by Scott Fenton, 24-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | nosepnelem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sltval2 | |
|
2 | fvex | |
|
3 | fvex | |
|
4 | 2 3 | brtp | |
5 | 1n0 | |
|
6 | simpl | |
|
7 | simpr | |
|
8 | 6 7 | neeq12d | |
9 | 5 8 | mpbiri | |
10 | df-2o | |
|
11 | df-1o | |
|
12 | 10 11 | eqeq12i | |
13 | 1on | |
|
14 | 0elon | |
|
15 | suc11 | |
|
16 | 13 14 15 | mp2an | |
17 | 12 16 | bitri | |
18 | 17 | necon3bii | |
19 | 5 18 | mpbir | |
20 | 19 | necomi | |
21 | simpl | |
|
22 | simpr | |
|
23 | 21 22 | neeq12d | |
24 | 20 23 | mpbiri | |
25 | 2on | |
|
26 | 25 | elexi | |
27 | 26 | prid2 | |
28 | 27 | nosgnn0i | |
29 | simpl | |
|
30 | simpr | |
|
31 | 29 30 | neeq12d | |
32 | 28 31 | mpbiri | |
33 | 9 24 32 | 3jaoi | |
34 | 4 33 | sylbi | |
35 | 1 34 | syl6bi | |
36 | 35 | 3impia | |