Theorem mulsproplem4

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and a member of the old set of B 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 𝑒 ) ) ) ) ) )
	mulsproplem4.1	⊢ ( 𝜑 → 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
	mulsproplem4.2	⊢ ( 𝜑 → 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
Assertion	mulsproplem4	⊢ ( 𝜑 → ( 𝑋 ·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		mulsproplem4.1	⊢ ( 𝜑 → 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
3		mulsproplem4.2	⊢ ( 𝜑 → 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
4		oldssno	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
5	4 2	sselid	⊢ ( 𝜑 → 𝑋 ∈ No )
6		oldssno	⊢ ( O ‘ ( bday ‘ 𝐵 ) ) ⊆ No
7	6 3	sselid	⊢ ( 𝜑 → 𝑌 ∈ No )
8		0sno	⊢ 0s ∈ No
9	8	a1i	⊢ ( 𝜑 → 0s ∈ No )
10		bday0s	⊢ ( bday ‘ 0s ) = ∅
11	10 10	oveq12i	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ( ∅ +no ∅ )
12		0elon	⊢ ∅ ∈ On
13		naddrid	⊢ ( ∅ ∈ On → ( ∅ +no ∅ ) = ∅ )
14	12 13	ax-mp	⊢ ( ∅ +no ∅ ) = ∅
15	11 14	eqtri	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ∅
16	15 15	uneq12i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ( ∅ ∪ ∅ )
17		un0	⊢ ( ∅ ∪ ∅ ) = ∅
18	16 17	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ∅
19	18 18	uneq12i	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ( ∅ ∪ ∅ )
20	19 17	eqtri	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ∅
21	20	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 ‘ 𝑌 ) ) ∪ ∅ )
22		un0	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ∅ ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) )
23	21 22	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 ‘ 𝑌 ) )
24		oldbdayim	⊢ ( 𝑋 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) )
25	2 24	syl	⊢ ( 𝜑 → ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) )
26		oldbdayim	⊢ ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) )
27	3 26	syl	⊢ ( 𝜑 → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) )
28		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
29		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
30		naddel12	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
31	28 29 30	mp2an	⊢ ( ( ( bday ‘ 𝑋 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
32	25 27 31	syl2anc	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
33		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 ‘ 𝐸 ) ) ) ) ) )
34	32 33	syl	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
35	23 34	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 ‘ 𝐸 ) ) ) ) ) )
36	1 5 7 9 9 9 9 35	mulsproplem1	⊢ ( 𝜑 → ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 0s <s 0s ∧ 0s <s 0s ) → ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) <s ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) ) ) )
37	36	simpld	⊢ ( 𝜑 → ( 𝑋 ·s 𝑌 ) ∈ No )