Metamath Proof Explorer

Theorem nmulle

Description: A condition for bounding a natural product above. Converse of ltnmul . (Contributed by Scott Fenton, 16-Jul-2026)

Ref Expression
Assertion nmulle ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmulcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) ∈ On )
2 ontri1 ⊢ ( ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ⊆ 𝐶 ↔ ¬ 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ) )
3 1 2 stoic3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ⊆ 𝐶 ↔ ¬ 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ) )
4 ltnmul ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ) )
5 4 3coml ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ) )
6 simpl3 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐶 ∈ On )
7 simp1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐴 ∈ On )
8 simpl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐴 )
9 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ On )
10 7 8 9 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ On )
11 simp2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐵 ∈ On )
12 simpr ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
13 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ On )
14 11 12 13 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ On )
15 10 14 nmulcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ·no 𝑏 ) ∈ On )
16 6 15 naddcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ∈ On )
17 simpl2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐵 ∈ On )
18 10 17 nmulcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ·no 𝐵 ) ∈ On )
19 simpl1 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐴 ∈ On )
20 19 14 nmulcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐴 ·no 𝑏 ) ∈ On )
21 18 20 naddcld ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ On )
22 ontri1 ⊢ ( ( ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ∈ On ∧ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ On ) → ( ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ↔ ¬ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )
23 16 21 22 syl2anc ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ↔ ¬ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )
24 23 2rexbidva ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ¬ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )
25 rexnal2 ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ¬ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ↔ ¬ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) )
26 24 25 bitrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ⊆ ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ↔ ¬ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )
27 5 26 bitr2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ↔ 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ) )
28 27 con1bid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ¬ 𝐶 ∈ ( 𝐴 ·no 𝐵 ) ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )
29 3 28 bitrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝐶 +no ( 𝑎 ·no 𝑏 ) ) ) )