Theorem mulsproplem2

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and B itself is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
	mulsproplem2.1	⊢ ( 𝜑 → 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
	mulsproplem2.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mulsproplem2	⊢ ( 𝜑 → ( 𝑋 ·s 𝐵 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
2		mulsproplem2.1	⊢ ( 𝜑 → 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
3		mulsproplem2.2	⊢ ( 𝜑 → 𝐵 ∈ No )
4		oldssno	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
5	4 2	sselid	⊢ ( 𝜑 → 𝑋 ∈ No )
6		0sno	⊢ 0s ∈ No
7	6	a1i	⊢ ( 𝜑 → 0s ∈ No )
8		bday0s	⊢ ( bday ‘ 0s ) = ∅
9	8 8	oveq12i	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ( ∅ +no ∅ )
10		0elon	⊢ ∅ ∈ On
11		naddrid	⊢ ( ∅ ∈ On → ( ∅ +no ∅ ) = ∅ )
12	10 11	ax-mp	⊢ ( ∅ +no ∅ ) = ∅
13	9 12	eqtri	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ∅
14	13 13	uneq12i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ( ∅ ∪ ∅ )
15		un0	⊢ ( ∅ ∪ ∅ ) = ∅
16	14 15	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ∅
17	16 16	uneq12i	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ( ∅ ∪ ∅ )
18	17 15	eqtri	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ∅
19	18	uneq2i	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∪ ∅ )
20		un0	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∪ ∅ ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) )
21	19 20	eqtri	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) )
22		oldbdayim	⊢ ( 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) )
23	2 22	syl	⊢ ( 𝜑 → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) )
24		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
25		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
26		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
27		naddel1	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
28	24 25 26 27	mp3an	⊢ ( ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
29	23 28	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
30		elun1	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
31	29 30	syl	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
32	21 31	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
33	1 5 3 7 7 7 7 32	mulsproplem1	⊢ ( 𝜑 → ( ( 𝑋 ·s 𝐵 ) ∈ No ∧ ( ( 0s <s 0s ∧ 0s <s 0s ) → ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) <s ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) ) ) )
34	33	simpld	⊢ ( 𝜑 → ( 𝑋 ·s 𝐵 ) ∈ No )