Metamath Proof Explorer

Theorem nmulss1

Description: Natural multiplication preserves less-than or equal. (Contributed by Scott Fenton, 15-Jul-2026)

Ref Expression
Assertion nmulss1 ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐴 ) ⊆ ( 𝐶 ·no 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐶 ∈ On )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ On )
3 0elon ⊢ ∅ ∈ On
4 3 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∅ ∈ On )
5 simpl1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ On )
6 0ss ⊢ ∅ ⊆ 𝐶
7 6 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∅ ⊆ 𝐶 )
8 simpr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
9 nmuladdss ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ∅ ∈ On ∧ 𝐴 ∈ On ) ∧ ( ∅ ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) ⊆ ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) )
10 1 2 4 5 7 8 9 syl222anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) ⊆ ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) )
11 nmull0 ⊢ ( 𝐵 ∈ On → ( ∅ ·no 𝐵 ) = ∅ )
12 2 11 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∅ ·no 𝐵 ) = ∅ )
13 12 oveq1d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) = ( ∅ +no ( 𝐶 ·no 𝐴 ) ) )
14 1 5 nmulcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐴 ) ∈ On )
15 naddlid ⊢ ( ( 𝐶 ·no 𝐴 ) ∈ On → ( ∅ +no ( 𝐶 ·no 𝐴 ) ) = ( 𝐶 ·no 𝐴 ) )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∅ +no ( 𝐶 ·no 𝐴 ) ) = ( 𝐶 ·no 𝐴 ) )
17 13 16 eqtr2d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐴 ) = ( ( ∅ ·no 𝐵 ) +no ( 𝐶 ·no 𝐴 ) ) )
18 nmull0 ⊢ ( 𝐴 ∈ On → ( ∅ ·no 𝐴 ) = ∅ )
19 5 18 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ∅ ·no 𝐴 ) = ∅ )
20 19 oveq2d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) = ( ( 𝐶 ·no 𝐵 ) +no ∅ ) )
21 1 2 nmulcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐵 ) ∈ On )
22 naddrid ⊢ ( ( 𝐶 ·no 𝐵 ) ∈ On → ( ( 𝐶 ·no 𝐵 ) +no ∅ ) = ( 𝐶 ·no 𝐵 ) )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐶 ·no 𝐵 ) +no ∅ ) = ( 𝐶 ·no 𝐵 ) )
24 20 23 eqtr2d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐵 ) = ( ( 𝐶 ·no 𝐵 ) +no ( ∅ ·no 𝐴 ) ) )
25 10 17 24 3sstr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ·no 𝐴 ) ⊆ ( 𝐶 ·no 𝐵 ) )