Metamath Proof Explorer

Theorem onnolt

Description: If a surreal ordinal is less than a given surreal, then it is simpler. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion onnolt 
|- ( ( A e. On_s /\ B e. No /\ A  ( bday ` A ) e. ( bday ` B ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. On_s /\ B e. No ) /\ ( bday ` B ) e. ( bday ` A ) ) -> B e. No )
2 onsno 
 |-  ( A e. On_s -> A e. No )
3 2 adantr 
 |-  ( ( A e. On_s /\ B e. No ) -> A e. No )
4 3 adantr 
 |-  ( ( ( A e. On_s /\ B e. No ) /\ ( bday ` B ) e. ( bday ` A ) ) -> A e. No )
5 bdayelon 
 |-  ( bday ` A ) e. On
6 simpr 
 |-  ( ( A e. On_s /\ B e. No ) -> B e. No )
7 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ B e. No ) -> ( B e. ( _Old ` ( bday ` A ) ) <-> ( bday ` B ) e. ( bday ` A ) ) )
8 5 6 7 sylancr 
 |-  ( ( A e. On_s /\ B e. No ) -> ( B e. ( _Old ` ( bday ` A ) ) <-> ( bday ` B ) e. ( bday ` A ) ) )
9 onsleft 
 |-  ( A e. On_s -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
10 9 eleq2d 
 |-  ( A e. On_s -> ( B e. ( _Old ` ( bday ` A ) ) <-> B e. ( _Left ` A ) ) )
11 10 adantr 
 |-  ( ( A e. On_s /\ B e. No ) -> ( B e. ( _Old ` ( bday ` A ) ) <-> B e. ( _Left ` A ) ) )
12 8 11 bitr3d 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( bday ` B ) e. ( bday ` A ) <-> B e. ( _Left ` A ) ) )
13 leftlt 
 |-  ( B e. ( _Left ` A ) -> B
14 12 13 biimtrdi 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( bday ` B ) e. ( bday ` A ) -> B
15 14 imp 
 |-  ( ( ( A e. On_s /\ B e. No ) /\ ( bday ` B ) e. ( bday ` A ) ) -> B
16 1 4 15 sltled 
 |-  ( ( ( A e. On_s /\ B e. No ) /\ ( bday ` B ) e. ( bday ` A ) ) -> B <_s A )
17 16 ex 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( bday ` B ) e. ( bday ` A ) -> B <_s A ) )
18 leftssold 
 |-  ( _Left ` B ) C_ ( _Old ` ( bday ` B ) )
19 fveq2 
 |-  ( ( bday ` B ) = ( bday ` A ) -> ( _Old ` ( bday ` B ) ) = ( _Old ` ( bday ` A ) ) )
20 19 3ad2ant3 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( _Old ` ( bday ` B ) ) = ( _Old ` ( bday ` A ) ) )
21 9 3ad2ant1 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
22 20 21 eqtrd 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( _Old ` ( bday ` B ) ) = ( _Left ` A ) )
23 18 22 sseqtrid 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( _Left ` B ) C_ ( _Left ` A ) )
24 simp2 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> B e. No )
25 2 3ad2ant1 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> A e. No )
26 simp3 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( bday ` B ) = ( bday ` A ) )
27 slelss 
 |-  ( ( B e. No /\ A e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( B <_s A <-> ( _Left ` B ) C_ ( _Left ` A ) ) )
28 24 25 26 27 syl3anc 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> ( B <_s A <-> ( _Left ` B ) C_ ( _Left ` A ) ) )
29 23 28 mpbird 
 |-  ( ( A e. On_s /\ B e. No /\ ( bday ` B ) = ( bday ` A ) ) -> B <_s A )
30 29 3expia 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( bday ` B ) = ( bday ` A ) -> B <_s A ) )
31 17 30 jaod 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( ( bday ` B ) e. ( bday ` A ) \/ ( bday ` B ) = ( bday ` A ) ) -> B <_s A ) )
32 bdayelon 
 |-  ( bday ` B ) e. On
33 32 5 onsseli 
 |-  ( ( bday ` B ) C_ ( bday ` A ) <-> ( ( bday ` B ) e. ( bday ` A ) \/ ( bday ` B ) = ( bday ` A ) ) )
34 ontri1 
 |-  ( ( ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` B ) C_ ( bday ` A ) <-> -. ( bday ` A ) e. ( bday ` B ) ) )
35 32 5 34 mp2an 
 |-  ( ( bday ` B ) C_ ( bday ` A ) <-> -. ( bday ` A ) e. ( bday ` B ) )
36 33 35 bitr3i 
 |-  ( ( ( bday ` B ) e. ( bday ` A ) \/ ( bday ` B ) = ( bday ` A ) ) <-> -. ( bday ` A ) e. ( bday ` B ) )
37 36 a1i 
 |-  ( ( A e. On_s /\ B e. No ) -> ( ( ( bday ` B ) e. ( bday ` A ) \/ ( bday ` B ) = ( bday ` A ) ) <-> -. ( bday ` A ) e. ( bday ` B ) ) )
38 slenlt 
 |-  ( ( B e. No /\ A e. No ) -> ( B <_s A <-> -. A
39 6 3 38 syl2anc 
 |-  ( ( A e. On_s /\ B e. No ) -> ( B <_s A <-> -. A
40 31 37 39 3imtr3d 
 |-  ( ( A e. On_s /\ B e. No ) -> ( -. ( bday ` A ) e. ( bday ` B ) -> -. A
41 40 con4d 
 |-  ( ( A e. On_s /\ B e. No ) -> ( A  ( bday ` A ) e. ( bday ` B ) ) )
42 41 3impia 
 |-  ( ( A e. On_s /\ B e. No /\ A  ( bday ` A ) e. ( bday ` B ) )