Metamath Proof Explorer

Theorem lltropt

Description: The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024) (Revised by Scott Fenton, 21-Feb-2025)

Ref Expression
Assertion lltropt 
|- ( _Left ` A ) <

Proof

Step Hyp Ref Expression
1 ssltleft 
 |-  ( A e. No -> ( _Left ` A ) <
2 ssltright 
 |-  ( A e. No -> { A } <
3 snnzg 
 |-  ( A e. No -> { A } =/= (/) )
4 sslttr 
 |-  ( ( ( _Left ` A ) < ( _Left ` A ) <
5 1 2 3 4 syl3anc 
 |-  ( A e. No -> ( _Left ` A ) <
6 0elpw 
 |-  (/) e. ~P No
7 nulssgt 
 |-  ( (/) e. ~P No -> (/) <
8 6 7 mp1i 
 |-  ( -. A e. No -> (/) <
9 leftf 
 |-  _Left : No --> ~P No
10 9 fdmi 
 |-  dom _Left = No
11 10 eleq2i 
 |-  ( A e. dom _Left <-> A e. No )
12 ndmfv 
 |-  ( -. A e. dom _Left -> ( _Left ` A ) = (/) )
13 11 12 sylnbir 
 |-  ( -. A e. No -> ( _Left ` A ) = (/) )
14 rightf 
 |-  _Right : No --> ~P No
15 14 fdmi 
 |-  dom _Right = No
16 15 eleq2i 
 |-  ( A e. dom _Right <-> A e. No )
17 ndmfv 
 |-  ( -. A e. dom _Right -> ( _Right ` A ) = (/) )
18 16 17 sylnbir 
 |-  ( -. A e. No -> ( _Right ` A ) = (/) )
19 8 13 18 3brtr4d 
 |-  ( -. A e. No -> ( _Left ` A ) <
20 5 19 pm2.61i 
 |-  ( _Left ` A ) <