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