Theorem ssltleft

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

	Ref	Expression
Assertion	ssltleft	|- ( A e. No -> ( _L ` A ) <

Proof

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