Metamath Proof Explorer

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 fvexd 
 |-  ( A e. No -> ( _L ` A ) e. _V )
2 snex 
 |-  { A } e. _V
3 2 a1i 
 |-  ( A e. No -> { A } e. _V )
4 leftf 
 |-  _L : No --> ~P No
5 4 ffvelrni 
 |-  ( A e. No -> ( _L ` A ) e. ~P No )
6 5 elpwid 
 |-  ( A e. No -> ( _L ` A ) C_ No )
7 snssi 
 |-  ( A e. No -> { A } C_ No )
8 velsn 
 |-  ( y e. { A } <-> y = A )
9 leftval 
 |-  ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
10 9 a1i 
 |-  ( A e. No -> ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
11 10 eleq2d 
 |-  ( A e. No -> ( x e. ( _L ` A ) <-> x e. { x e. ( _Old ` ( bday ` A ) ) | x
12 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` A ) ) | x  ( x e. ( _Old ` ( bday ` A ) ) /\ x
13 11 12 bitrdi 
 |-  ( A e. No -> ( x e. ( _L ` A ) <-> ( x e. ( _Old ` ( bday ` A ) ) /\ x
14 13 simplbda 
 |-  ( ( A e. No /\ x e. ( _L ` A ) ) -> x
15 breq2 
 |-  ( y = A -> ( x  x
16 14 15 syl5ibr 
 |-  ( y = A -> ( ( A e. No /\ x e. ( _L ` A ) ) -> x
17 16 expd 
 |-  ( y = A -> ( A e. No -> ( x e. ( _L ` A ) -> x
18 8 17 sylbi 
 |-  ( y e. { A } -> ( A e. No -> ( x e. ( _L ` A ) -> x
19 18 3imp231 
 |-  ( ( A e. No /\ x e. ( _L ` A ) /\ y e. { A } ) -> x
20 1 3 6 7 19 ssltd 
 |-  ( A e. No -> ( _L ` A ) <