Theorem ltnmul

Description: Characterize less-than a natural product. (Contributed by Scott Fenton, 15-Jul-2026)

	Ref	Expression
Assertion	ltnmul	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) = ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) )
2	1	eleq2d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) ↔ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
3	2	2ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) ↔ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
4	3	onnminsb	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) } → ¬ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
5	4	3ad2ant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) } → ¬ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
6		nmulval	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐵 ·no 𝐶 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) } )
7	6	eleq2d	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) } ) )
8	7	3adant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ 𝐴 ∈ ∩ { 𝑥 ∈ On ∣ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝑥 +no ( 𝑏 ·no 𝑐 ) ) } ) )
9		simpl1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐴 ∈ On )
10		simp2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐵 ∈ On )
11		simpl	⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → 𝑏 ∈ 𝐵 )
12		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ On )
13	10 11 12	syl2an	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑏 ∈ On )
14		simp3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
15		simpr	⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ 𝐶 )
16		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ On )
17	14 15 16	syl2an	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝑐 ∈ On )
18	13 17	nmulcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ·no 𝑐 ) ∈ On )
19	9 18	naddcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ On )
20		simpl3	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐶 ∈ On )
21	13 20	nmulcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝑏 ·no 𝐶 ) ∈ On )
22		simpl2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → 𝐵 ∈ On )
23	22 17	nmulcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐵 ·no 𝑐 ) ∈ On )
24	21 23	naddcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ On )
25		ontri1	⊢ ( ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ On ∧ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ On ) → ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ↔ ¬ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
26	19 24 25	syl2anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ↔ ¬ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
27	26	2rexbidva	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ¬ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
28		rexnal2	⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ¬ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ↔ ¬ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) )
29	27 28	bitrdi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ↔ ¬ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ) )
30	5 8 29	3imtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ) )
31		nmuladdel	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) )
32	31	3adantl1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) )
33	22 20	nmulcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐵 ·no 𝐶 ) ∈ On )
34	33 18	naddcld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ∈ On )
35		ontr2	⊢ ( ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ On ∧ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ∈ On ) → ( ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∧ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) → ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) )
36	19 34 35	syl2anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∧ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) → ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) )
37	32 36	mpan2d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) → ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) )
38		naddel1	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ·no 𝐶 ) ∈ On ∧ ( 𝑏 ·no 𝑐 ) ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) )
39	9 33 18 38	syl3anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ∈ ( ( 𝐵 ·no 𝐶 ) +no ( 𝑏 ·no 𝑐 ) ) ) )
40	37 39	sylibrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) → 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ) )
41	40	rexlimdvva	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) → 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ) )
42	30 41	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ ( 𝐵 ·no 𝐶 ) ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ( 𝐴 +no ( 𝑏 ·no 𝑐 ) ) ⊆ ( ( 𝑏 ·no 𝐶 ) +no ( 𝐵 ·no 𝑐 ) ) ) )