Metamath Proof Explorer

Theorem nmuladdss

Description: Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026)

Ref Expression
Assertion nmuladdss 
|- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) )

Proof

Step Hyp Ref Expression
1 onsseleq 
 |-  ( ( C e. On /\ A e. On ) -> ( C C_ A <-> ( C e. A \/ C = A ) ) )
2 1 ancoms 
 |-  ( ( A e. On /\ C e. On ) -> ( C C_ A <-> ( C e. A \/ C = A ) ) )
3 onsseleq 
 |-  ( ( D e. On /\ B e. On ) -> ( D C_ B <-> ( D e. B \/ D = B ) ) )
4 3 ancoms 
 |-  ( ( B e. On /\ D e. On ) -> ( D C_ B <-> ( D e. B \/ D = B ) ) )
5 2 4 bi2anan9 
 |-  ( ( ( A e. On /\ C e. On ) /\ ( B e. On /\ D e. On ) ) -> ( ( C C_ A /\ D C_ B ) <-> ( ( C e. A \/ C = A ) /\ ( D e. B \/ D = B ) ) ) )
6 5 an4s 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C C_ A /\ D C_ B ) <-> ( ( C e. A \/ C = A ) /\ ( D e. B \/ D = B ) ) ) )
7 nmulcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )
8 7 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( A .no B ) e. On )
9 onelon 
 |-  ( ( A e. On /\ C e. A ) -> C e. On )
10 onelon 
 |-  ( ( B e. On /\ D e. B ) -> D e. On )
11 nmulcl 
 |-  ( ( C e. On /\ D e. On ) -> ( C .no D ) e. On )
12 9 10 11 syl2an 
 |-  ( ( ( A e. On /\ C e. A ) /\ ( B e. On /\ D e. B ) ) -> ( C .no D ) e. On )
13 12 an4s 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( C .no D ) e. On )
14 8 13 naddcld 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( A .no B ) +no ( C .no D ) ) e. On )
15 ontr 
 |-  ( ( ( A .no B ) +no ( C .no D ) ) e. On -> Tr ( ( A .no B ) +no ( C .no D ) ) )
16 14 15 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> Tr ( ( A .no B ) +no ( C .no D ) ) )
17 nmuladdel 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) )
18 trss 
 |-  ( Tr ( ( A .no B ) +no ( C .no D ) ) -> ( ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
19 16 17 18 sylc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) )
20 19 adantlr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) )
21 20 expr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D e. B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
22 simplll 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> A e. On )
23 simpllr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> B e. On )
24 22 23 nmulcld 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( A .no B ) e. On )
25 simplrl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> C e. On )
26 25 23 nmulcld 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( C .no B ) e. On )
27 naddcom 
 |-  ( ( ( A .no B ) e. On /\ ( C .no B ) e. On ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) )
28 24 26 27 syl2anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( A .no B ) +no ( C .no B ) ) = ( ( C .no B ) +no ( A .no B ) ) )
29 28 eqimsscd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) )
30 oveq2 
 |-  ( D = B -> ( A .no D ) = ( A .no B ) )
31 30 oveq2d 
 |-  ( D = B -> ( ( C .no B ) +no ( A .no D ) ) = ( ( C .no B ) +no ( A .no B ) ) )
32 oveq2 
 |-  ( D = B -> ( C .no D ) = ( C .no B ) )
33 32 oveq2d 
 |-  ( D = B -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( C .no B ) ) )
34 31 33 sseq12d 
 |-  ( D = B -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( C .no B ) +no ( A .no B ) ) C_ ( ( A .no B ) +no ( C .no B ) ) ) )
35 29 34 syl5ibrcom 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( D = B -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
36 21 35 jaod 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) /\ C e. A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
37 36 ex 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C e. A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) )
38 ssid 
 |-  ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) )
39 38 2a1i 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) )
40 oveq1 
 |-  ( C = A -> ( C .no B ) = ( A .no B ) )
41 40 oveq1d 
 |-  ( C = A -> ( ( C .no B ) +no ( A .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) )
42 oveq1 
 |-  ( C = A -> ( C .no D ) = ( A .no D ) )
43 42 oveq2d 
 |-  ( C = A -> ( ( A .no B ) +no ( C .no D ) ) = ( ( A .no B ) +no ( A .no D ) ) )
44 41 43 sseq12d 
 |-  ( C = A -> ( ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) <-> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) )
45 44 imbi2d 
 |-  ( C = A -> ( ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) <-> ( ( D e. B \/ D = B ) -> ( ( A .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( A .no D ) ) ) ) )
46 39 45 syl5ibrcom 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( C = A -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) )
47 37 46 jaod 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C e. A \/ C = A ) -> ( ( D e. B \/ D = B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) ) )
48 47 impd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( C e. A \/ C = A ) /\ ( D e. B \/ D = B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
49 6 48 sylbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( C C_ A /\ D C_ B ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) ) )
50 49 3impia 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) /\ ( C C_ A /\ D C_ B ) ) -> ( ( C .no B ) +no ( A .no D ) ) C_ ( ( A .no B ) +no ( C .no D ) ) )