Metamath Proof Explorer


Theorem nomaxmo

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 

Proof

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
 |-  ( `'  E* x e. S A. y e. S -. y `' 
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 `'  x 
11 10 notbii
 |-  ( -. y `'  -. x 
12 11 ralbii
 |-  ( A. y e. S -. y `'  A. y e. S -. x 
13 12 rmobii
 |-  ( E* x e. S A. y e. S -. y `'  E* x e. S A. y e. S -. x 
14 7 13 sylib
 |-  ( S C_ No -> E* x e. S A. y e. S -. x