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 No L A s A

Proof

Step Hyp Ref Expression
1 fvexd A No L A V
2 snex A V
3 2 a1i A No A V
4 leftf L : No 𝒫 No
5 4 ffvelrni A No L A 𝒫 No
6 5 elpwid A No L A No
7 snssi A No A No
8 velsn y A y = A
9 leftval L A = x Old bday A | x < s A
10 9 a1i A No L A = x Old bday A | x < s A
11 10 eleq2d A No x L A x x Old bday A | x < s A
12 rabid x x Old bday A | x < s A x Old bday A x < s A
13 11 12 bitrdi A No x L A x Old bday A x < s A
14 13 simplbda A No x L A x < s A
15 breq2 y = A x < s y x < s A
16 14 15 syl5ibr y = A A No x L A x < s y
17 16 expd y = A A No x L A x < s y
18 8 17 sylbi y A A No x L A x < s y
19 18 3imp231 A No x L A y A x < s y
20 1 3 6 7 19 ssltd A No L A s A