Metamath Proof Explorer

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 )