Theorem nmuladdel

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = ( 𝐴 ·no 𝐵 ) → ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) )
2	1	eleq2d	⊢ ( 𝑥 = ( 𝐴 ·no 𝐵 ) → ( ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) ↔ ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) ) )
3	2	2ralbidv	⊢ ( 𝑥 = ( 𝐴 ·no 𝐵 ) → ( ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) ↔ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) ) )
4		nmulval	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } )
5		ssrab2	⊢ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ⊆ On
6		nmulcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) ∈ On )
7	4 6	eqeltrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ∈ On )
8		rabn0	⊢ ( { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ≠ ∅ ↔ ∃ 𝑥 ∈ On ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) )
9		onintrab2	⊢ ( ∃ 𝑥 ∈ On ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) ↔ ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ∈ On )
10	8 9	bitri	⊢ ( { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ≠ ∅ ↔ ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ∈ On )
11	7 10	sylibr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ≠ ∅ )
12		onint	⊢ ( ( { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ⊆ On ∧ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ≠ ∅ ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ∈ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } )
13	5 11 12	sylancr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } ∈ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } )
14	4 13	eqeltrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) ∈ { 𝑥 ∈ On ∣ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( 𝑥 +no ( 𝑐 ·no 𝑑 ) ) } )
15	3 14	elrabrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) )
16		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 ·no 𝐵 ) = ( 𝐶 ·no 𝐵 ) )
17	16	oveq1d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) )
18		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 ·no 𝑑 ) = ( 𝐶 ·no 𝑑 ) )
19	18	oveq2d	⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝑑 ) ) )
20	17 19	eleq12d	⊢ ( 𝑐 = 𝐶 → ( ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) ↔ ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝑑 ) ) ) )
21		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐴 ·no 𝑑 ) = ( 𝐴 ·no 𝐷 ) )
22	21	oveq2d	⊢ ( 𝑑 = 𝐷 → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) )
23		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐶 ·no 𝑑 ) = ( 𝐶 ·no 𝐷 ) )
24	23	oveq2d	⊢ ( 𝑑 = 𝐷 → ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝑑 ) ) = ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
25	22 24	eleq12d	⊢ ( 𝑑 = 𝐷 → ( ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝑑 ) ) ↔ ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) ) )
26	20 25	rspc2va	⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
27	26	ancoms	⊢ ( ( ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐵 ( ( 𝑐 ·no 𝐵 ) +no ( 𝐴 ·no 𝑑 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝑐 ·no 𝑑 ) ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )
28	15 27	sylan	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ·no 𝐵 ) +no ( 𝐴 ·no 𝐷 ) ) ∈ ( ( 𝐴 ·no 𝐵 ) +no ( 𝐶 ·no 𝐷 ) ) )