Theorem ssltright

Description: A surreal is less than its right options. Theorem 0(i) of Conway p. 16. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	ssltright	|- ( A e. No -> { A } <

Proof

Step	Hyp	Ref	Expression
1		snssi	|- ( A e. No -> { A } C_ No )
2		rightf	|- _R : No --> ~P No
3	2	ffvelrni	|- ( A e. No -> ( _R ` A ) e. ~P No )
4	3	elpwid	|- ( A e. No -> ( _R ` A ) C_ No )
5		rightval	|- ( A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
6	5	eleq2d	|- ( A e. No -> ( y e. ( _R ` A ) <-> y e. { x e. ( _Old ` ( bday ` A ) ) | A
7		breq2	|- ( x = y -> ( A A
8	7	elrab	|- ( y e. { x e. ( _Old ` ( bday ` A ) ) | A ( y e. ( _Old ` ( bday ` A ) ) /\ A
9	8	simprbi	|- ( y e. { x e. ( _Old ` ( bday ` A ) ) | A A
10	6 9	syl6bi	|- ( A e. No -> ( y e. ( _R ` A ) -> A
11	10	ralrimiv	|- ( A e. No -> A. y e. ( _R ` A ) A
12		breq1	|- ( x = A -> ( x A
13	12	ralbidv	|- ( x = A -> ( A. y e. ( _R ` A ) x A. y e. ( _R ` A ) A
14	13	ralsng	|- ( A e. No -> ( A. x e. { A } A. y e. ( _R ` A ) x A. y e. ( _R ` A ) A
15	11 14	mpbird	|- ( A e. No -> A. x e. { A } A. y e. ( _R ` A ) x
16		snex	|- { A } e. _V
17		fvex	|- ( _R ` A ) e. _V
18	16 17	pm3.2i	|- ( { A } e. _V /\ ( _R ` A ) e. _V )
19		brsslt	|- ( { A } < ( ( { A } e. _V /\ ( _R ` A ) e. _V ) /\ ( { A } C_ No /\ ( _R ` A ) C_ No /\ A. x e. { A } A. y e. ( _R ` A ) x
20	18 19	mpbiran	|- ( { A } < ( { A } C_ No /\ ( _R ` A ) C_ No /\ A. x e. { A } A. y e. ( _R ` A ) x
21	1 4 15 20	syl3anbrc	|- ( A e. No -> { A } <