Description: Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | noextend.1 | |
|
Assertion | noextend | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noextend.1 | |
|
2 | nofun | |
|
3 | dmexg | |
|
4 | funsng | |
|
5 | 3 1 4 | sylancl | |
6 | 1 | elexi | |
7 | 6 | dmsnop | |
8 | 7 | ineq2i | |
9 | nodmord | |
|
10 | ordirr | |
|
11 | 9 10 | syl | |
12 | disjsn | |
|
13 | 11 12 | sylibr | |
14 | 8 13 | eqtrid | |
15 | funun | |
|
16 | 2 5 14 15 | syl21anc | |
17 | 7 | uneq2i | |
18 | dmun | |
|
19 | df-suc | |
|
20 | 17 18 19 | 3eqtr4i | |
21 | nodmon | |
|
22 | suceloni | |
|
23 | 21 22 | syl | |
24 | 20 23 | eqeltrid | |
25 | rnun | |
|
26 | rnsnopg | |
|
27 | 3 26 | syl | |
28 | 27 | uneq2d | |
29 | 25 28 | eqtrid | |
30 | norn | |
|
31 | snssi | |
|
32 | 1 31 | mp1i | |
33 | 30 32 | unssd | |
34 | 29 33 | eqsstrd | |
35 | elno2 | |
|
36 | 16 24 34 35 | syl3anbrc | |