Description: A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | nomaxmo | |- ( S C_ No -> E* x e. S A. y e. S -. x |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sltso | |- |
|
2 | soss | |- ( S C_ No -> ( |
|
3 | 1 2 | mpi | |- ( S C_ No -> |
4 | cnvso | |- ( |
|
5 | 3 4 | sylib | |- ( S C_ No -> `' |
6 | somo | |- ( `' |
|
7 | 5 6 | syl | |- ( S C_ No -> E* x e. S A. y e. S -. y `' |
8 | vex | |- y e. _V |
|
9 | vex | |- x e. _V |
|
10 | 8 9 | brcnv | |- ( y `' |
11 | 10 | notbii | |- ( -. y `' |
12 | 11 | ralbii | |- ( A. y e. S -. y `' |
13 | 12 | rmobii | |- ( E* x e. S A. y e. S -. y `' |
14 | 7 13 | sylib | |- ( S C_ No -> E* x e. S A. y e. S -. x |