Metamath Proof Explorer

Theorem nmuladdss

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

Ref Expression
Assertion nmuladdss ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 onsseleq ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐶 ⊆ 𝐴 ↔ ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ⊆ 𝐴 ↔ ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) ) )
3 onsseleq ⊢ ( ( 𝐷 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐷 ⊆ 𝐵 ↔ ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) ) )
4 3 ancoms ⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐷 ⊆ 𝐵 ↔ ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) ) )
5 2 4 bi2anan9 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝐵 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ↔ ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) ∧ ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) ) ) )
6 5 an4s ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ↔ ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) ∧ ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) ) ) )
7 nmulcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) ∈ On )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐴 ·no 𝐵 ) ∈ On )
9 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
10 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝐵 ) → 𝐷 ∈ On )
11 nmulcl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 ·no 𝐷 ) ∈ On )
12 9 10 11 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ 𝐴 ) ∧ ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐶 ·no 𝐷 ) ∈ On )
13 12 an4s ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐶 ·no 𝐷 ) ∈ On )
14 8 13 naddcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ∈ On )
15 ontr ⊢ ( ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ∈ On → Tr ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → Tr ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
17 nmuladdel ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
18 trss ⊢ ( Tr ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) → ( ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
19 16 17 18 sylc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
20 19 adantlr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
21 20 expr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 ∈ 𝐵 → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
22 simplll ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → 𝐴 ∈ On )
23 simpllr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ On )
24 22 23 nmulcld ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐴 ·no 𝐵 ) ∈ On )
25 simplrl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ On )
26 25 23 nmulcld ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ·no 𝐵 ) ∈ On )
27 naddcom ⊢ ( ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ ( 𝐶 ·no 𝐵 ) ∈ On ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐵 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐵 ) ) )
28 24 26 27 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐵 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐵 ) ) )
29 28 eqimsscd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐵 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐵 ) ) )
30 oveq2 ⊢ ( 𝐷 = 𝐵 → ( 𝐴 ·no 𝐷 ) = ( 𝐴 ·no 𝐵 ) )
31 30 oveq2d ⊢ ( 𝐷 = 𝐵 → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐵 ) ) )
32 oveq2 ⊢ ( 𝐷 = 𝐵 → ( 𝐶 ·no 𝐷 ) = ( 𝐶 ·no 𝐵 ) )
33 32 oveq2d ⊢ ( 𝐷 = 𝐵 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐵 ) ) )
34 31 33 sseq12d ⊢ ( 𝐷 = 𝐵 → ( ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ↔ ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐵 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐵 ) ) ) )
35 29 34 syl5ibrcom ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 = 𝐵 → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
36 21 35 jaod ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
37 36 ex ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ 𝐴 → ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) ) )
38 ssid ⊢ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) )
39 38 2a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ) )
40 oveq1 ⊢ ( 𝐶 = 𝐴 → ( 𝐶 ·no 𝐵 ) = ( 𝐴 ·no 𝐵 ) )
41 40 oveq1d ⊢ ( 𝐶 = 𝐴 → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) )
42 oveq1 ⊢ ( 𝐶 = 𝐴 → ( 𝐶 ·no 𝐷 ) = ( 𝐴 ·no 𝐷 ) )
43 42 oveq2d ⊢ ( 𝐶 = 𝐴 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) )
44 41 43 sseq12d ⊢ ( 𝐶 = 𝐴 → ( ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ↔ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ) )
45 44 imbi2d ⊢ ( 𝐶 = 𝐴 → ( ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) ↔ ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ) ) )
46 39 45 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 = 𝐴 → ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) ) )
47 37 46 jaod ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) → ( ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) ) )
48 47 impd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 = 𝐴 ) ∧ ( 𝐷 ∈ 𝐵 ∨ 𝐷 = 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
49 6 48 sylbid ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
50 49 3impia ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ⊆ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )