Metamath Proof Explorer

Theorem precsexlem10

Description: Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025)

Ref Expression
Hypotheses precsexlem.1 ⊢ 𝐹 = rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ )
precsexlem.2 ⊢ 𝐿 = ( 1st ∘ 𝐹 )
precsexlem.3 ⊢ 𝑅 = ( 2nd ∘ 𝐹 )
precsexlem.4 ⊢ ( 𝜑 → 𝐴 ∈ No )
precsexlem.5 ⊢ ( 𝜑 → 0s <s 𝐴 )
precsexlem.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
Assertion precsexlem10 ( 𝜑 → ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) )

Proof

Step Hyp Ref Expression
1 precsexlem.1 ⊢ 𝐹 = rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ )
2 precsexlem.2 ⊢ 𝐿 = ( 1st ∘ 𝐹 )
3 precsexlem.3 ⊢ 𝑅 = ( 2nd ∘ 𝐹 )
4 precsexlem.4 ⊢ ( 𝜑 → 𝐴 ∈ No )
5 precsexlem.5 ⊢ ( 𝜑 → 0s <s 𝐴 )
6 precsexlem.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
7 fo1st ⊢ 1st : V –onto→ V
8 fofun ⊢ ( 1st : V –onto→ V → Fun 1st )
9 7 8 ax-mp ⊢ Fun 1st
10 rdgfun ⊢ Fun rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ )
11 1 funeqi ⊢ ( Fun 𝐹 ↔ Fun rec ( ( 𝑝 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑙 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑟 ⦌ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) , ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⟩ ) , ⟨ { 0s } , ∅ ⟩ ) )
12 10 11 mpbir ⊢ Fun 𝐹
13 funco ⊢ ( ( Fun 1st ∧ Fun 𝐹 ) → Fun ( 1st ∘ 𝐹 ) )
14 9 12 13 mp2an ⊢ Fun ( 1st ∘ 𝐹 )
15 2 funeqi ⊢ ( Fun 𝐿 ↔ Fun ( 1st ∘ 𝐹 ) )
16 14 15 mpbir ⊢ Fun 𝐿
17 dcomex ⊢ ω ∈ V
18 17 funimaex ⊢ ( Fun 𝐿 → ( 𝐿 “ ω ) ∈ V )
19 16 18 ax-mp ⊢ ( 𝐿 “ ω ) ∈ V
20 19 uniex ⊢ ∪ ( 𝐿 “ ω ) ∈ V
21 20 a1i ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) ∈ V )
22 fo2nd ⊢ 2nd : V –onto→ V
23 fofun ⊢ ( 2nd : V –onto→ V → Fun 2nd )
24 22 23 ax-mp ⊢ Fun 2nd
25 funco ⊢ ( ( Fun 2nd ∧ Fun 𝐹 ) → Fun ( 2nd ∘ 𝐹 ) )
26 24 12 25 mp2an ⊢ Fun ( 2nd ∘ 𝐹 )
27 3 funeqi ⊢ ( Fun 𝑅 ↔ Fun ( 2nd ∘ 𝐹 ) )
28 26 27 mpbir ⊢ Fun 𝑅
29 17 funimaex ⊢ ( Fun 𝑅 → ( 𝑅 “ ω ) ∈ V )
30 28 29 ax-mp ⊢ ( 𝑅 “ ω ) ∈ V
31 30 uniex ⊢ ∪ ( 𝑅 “ ω ) ∈ V
32 31 a1i ⊢ ( 𝜑 → ∪ ( 𝑅 “ ω ) ∈ V )
33 funiunfv ⊢ ( Fun 𝐿 → ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) = ∪ ( 𝐿 “ ω ) )
34 16 33 ax-mp ⊢ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) = ∪ ( 𝐿 “ ω )
35 1 2 3 4 5 6 precsexlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) )
36 35 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ( 𝐿 ‘ 𝑖 ) ⊆ No )
37 36 iunssd ⊢ ( 𝜑 → ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) ⊆ No )
38 34 37 eqsstrrid ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) ⊆ No )
39 funiunfv ⊢ ( Fun 𝑅 → ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) = ∪ ( 𝑅 “ ω ) )
40 28 39 ax-mp ⊢ ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) = ∪ ( 𝑅 “ ω )
41 35 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ( 𝑅 ‘ 𝑖 ) ⊆ No )
42 41 iunssd ⊢ ( 𝜑 → ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) ⊆ No )
43 40 42 eqsstrrid ⊢ ( 𝜑 → ∪ ( 𝑅 “ ω ) ⊆ No )
44 34 eleq2i ⊢ ( 𝑏 ∈ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) ↔ 𝑏 ∈ ∪ ( 𝐿 “ ω ) )
45 eliun ⊢ ( 𝑏 ∈ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ω 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) )
46 44 45 bitr3i ⊢ ( 𝑏 ∈ ∪ ( 𝐿 “ ω ) ↔ ∃ 𝑖 ∈ ω 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) )
47 funiunfv ⊢ ( Fun 𝑅 → ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) = ∪ ( 𝑅 “ ω ) )
48 28 47 ax-mp ⊢ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) = ∪ ( 𝑅 “ ω )
49 48 eleq2i ⊢ ( 𝑐 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ 𝑐 ∈ ∪ ( 𝑅 “ ω ) )
50 eliun ⊢ ( 𝑐 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) )
51 49 50 bitr3i ⊢ ( 𝑐 ∈ ∪ ( 𝑅 “ ω ) ↔ ∃ 𝑗 ∈ ω 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) )
52 46 51 anbi12i ⊢ ( ( 𝑏 ∈ ∪ ( 𝐿 “ ω ) ∧ 𝑐 ∈ ∪ ( 𝑅 “ ω ) ) ↔ ( ∃ 𝑖 ∈ ω 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ω 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) )
53 reeanv ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) ↔ ( ∃ 𝑖 ∈ ω 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ ∃ 𝑗 ∈ ω 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) )
54 52 53 bitr4i ⊢ ( ( 𝑏 ∈ ∪ ( 𝐿 “ ω ) ∧ 𝑐 ∈ ∪ ( 𝑅 “ ω ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) )
55 omun ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∪ 𝑗 ) ∈ ω )
56 ssun1 ⊢ 𝑖 ⊆ ( 𝑖 ∪ 𝑗 )
57 1 2 3 precsexlem6 ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ∧ 𝑖 ⊆ ( 𝑖 ∪ 𝑗 ) ) → ( 𝐿 ‘ 𝑖 ) ⊆ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) )
58 56 57 mp3an3 ⊢ ( ( 𝑖 ∈ ω ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝐿 ‘ 𝑖 ) ⊆ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) )
59 55 58 syldan ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝐿 ‘ 𝑖 ) ⊆ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝐿 ‘ 𝑖 ) ⊆ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) )
61 60 sseld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) → 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ) )
62 simpr ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → 𝑗 ∈ ω )
63 ssun2 ⊢ 𝑗 ⊆ ( 𝑖 ∪ 𝑗 )
64 1 2 3 precsexlem7 ⊢ ( ( 𝑗 ∈ ω ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ∧ 𝑗 ⊆ ( 𝑖 ∪ 𝑗 ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) )
65 63 64 mp3an3 ⊢ ( ( 𝑗 ∈ ω ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝑅 ‘ 𝑗 ) ⊆ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) )
66 62 55 65 syl2anc ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ 𝑗 ) ⊆ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) )
67 66 sseld ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) → 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) → 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) )
69 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → 𝐴 ∈ No )
70 1 2 3 4 5 6 precsexlem8 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ⊆ No ∧ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ⊆ No ) )
71 70 simpld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ⊆ No )
72 71 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ) → 𝑏 ∈ No )
73 72 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → 𝑏 ∈ No )
74 69 73 mulscld ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( 𝐴 ·s 𝑏 ) ∈ No )
75 70 simprd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ⊆ No )
76 75 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) → 𝑐 ∈ No )
77 76 adantrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → 𝑐 ∈ No )
78 69 77 mulscld ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( 𝐴 ·s 𝑐 ) ∈ No )
79 74 78 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( ( 𝐴 ·s 𝑏 ) ∈ No ∧ ( 𝐴 ·s 𝑐 ) ∈ No ) )
80 1 2 3 4 5 6 precsexlem9 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( ∀ 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
81 80 simpld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ∀ 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ( 𝐴 ·s 𝑏 ) <s 1s )
82 rsp ⊢ ( ∀ 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ( 𝐴 ·s 𝑏 ) <s 1s → ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) → ( 𝐴 ·s 𝑏 ) <s 1s ) )
83 81 82 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) → ( 𝐴 ·s 𝑏 ) <s 1s ) )
84 80 simprd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ∀ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) 1s <s ( 𝐴 ·s 𝑐 ) )
85 rsp ⊢ ( ∀ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) 1s <s ( 𝐴 ·s 𝑐 ) → ( 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑐 ) ) )
86 84 85 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑐 ) ) )
87 83 86 anim12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) → ( ( 𝐴 ·s 𝑏 ) <s 1s ∧ 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
88 87 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( ( 𝐴 ·s 𝑏 ) <s 1s ∧ 1s <s ( 𝐴 ·s 𝑐 ) ) )
89 1no ⊢ 1s ∈ No
90 ltstr ⊢ ( ( ( 𝐴 ·s 𝑏 ) ∈ No ∧ 1s ∈ No ∧ ( 𝐴 ·s 𝑐 ) ∈ No ) → ( ( ( 𝐴 ·s 𝑏 ) <s 1s ∧ 1s <s ( 𝐴 ·s 𝑐 ) ) → ( 𝐴 ·s 𝑏 ) <s ( 𝐴 ·s 𝑐 ) ) )
91 89 90 mp3an2 ⊢ ( ( ( 𝐴 ·s 𝑏 ) ∈ No ∧ ( 𝐴 ·s 𝑐 ) ∈ No ) → ( ( ( 𝐴 ·s 𝑏 ) <s 1s ∧ 1s <s ( 𝐴 ·s 𝑐 ) ) → ( 𝐴 ·s 𝑏 ) <s ( 𝐴 ·s 𝑐 ) ) )
92 79 88 91 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( 𝐴 ·s 𝑏 ) <s ( 𝐴 ·s 𝑐 ) )
93 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → 0s <s 𝐴 )
94 73 77 69 93 ltmuls2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → ( 𝑏 <s 𝑐 ↔ ( 𝐴 ·s 𝑏 ) <s ( 𝐴 ·s 𝑐 ) ) )
95 92 94 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) ∧ ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) ) → 𝑏 <s 𝑐 )
96 95 ex ⊢ ( ( 𝜑 ∧ ( 𝑖 ∪ 𝑗 ) ∈ ω ) → ( ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) → 𝑏 <s 𝑐 ) )
97 55 96 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑏 ∈ ( 𝐿 ‘ ( 𝑖 ∪ 𝑗 ) ) ∧ 𝑐 ∈ ( 𝑅 ‘ ( 𝑖 ∪ 𝑗 ) ) ) → 𝑏 <s 𝑐 ) )
98 61 68 97 syl2and ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) → 𝑏 <s 𝑐 ) )
99 98 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ∧ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) ) → 𝑏 <s 𝑐 ) )
100 54 99 biimtrid ⊢ ( 𝜑 → ( ( 𝑏 ∈ ∪ ( 𝐿 “ ω ) ∧ 𝑐 ∈ ∪ ( 𝑅 “ ω ) ) → 𝑏 <s 𝑐 ) )
101 100 3impib ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ ( 𝐿 “ ω ) ∧ 𝑐 ∈ ∪ ( 𝑅 “ ω ) ) → 𝑏 <s 𝑐 )
102 21 32 38 43 101 sltsd ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) )