Metamath Proof Explorer

Theorem ssltmul1

Description: One surreal set less-than relationship for cuts of A and B . (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses ssltmul1.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
ssltmul1.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
ssltmul1.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
ssltmul1.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion ssltmul1 ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } )

Proof

Step Hyp Ref Expression
1 ssltmul1.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2 ssltmul1.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3 ssltmul1.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4 ssltmul1.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5 eqid ⊢ ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) = ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
6 5 rnmpo ⊢ ran ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) }
7 ssltex1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
8 1 7 syl ⊢ ( 𝜑 → 𝐿 ∈ V )
9 ssltex1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ∈ V )
10 2 9 syl ⊢ ( 𝜑 → 𝑀 ∈ V )
11 5 mpoexg ⊢ ( ( 𝐿 ∈ V ∧ 𝑀 ∈ V ) → ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V )
12 8 10 11 syl2anc ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V )
13 rnexg ⊢ ( ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V → ran ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V )
14 12 13 syl ⊢ ( 𝜑 → ran ( 𝑝 ∈ 𝐿 , 𝑞 ∈ 𝑀 ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V )
15 6 14 eqeltrrid ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∈ V )
16 eqid ⊢ ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) = ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
17 16 rnmpo ⊢ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) = { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) }
18 ssltex2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
19 1 18 syl ⊢ ( 𝜑 → 𝑅 ∈ V )
20 ssltex2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ∈ V )
21 2 20 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
22 16 mpoexg ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V )
23 19 21 22 syl2anc ⊢ ( 𝜑 → ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V )
24 rnexg ⊢ ( ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V → ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V )
25 23 24 syl ⊢ ( 𝜑 → ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V )
26 17 25 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ∈ V )
27 15 26 unexd ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∈ V )
28 snex ⊢ { ( 𝐴 ·s 𝐵 ) } ∈ V
29 28 a1i ⊢ ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } ∈ V )
30 ssltss1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
31 1 30 syl ⊢ ( 𝜑 → 𝐿 ⊆ No )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐿 ⊆ No )
33 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑝 ∈ 𝐿 )
34 32 33 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑝 ∈ No )
35 2 scutcld ⊢ ( 𝜑 → ( 𝑀 |s 𝑆 ) ∈ No )
36 4 35 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ No )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐵 ∈ No )
38 34 37 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝑝 ·s 𝐵 ) ∈ No )
39 1 scutcld ⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) ∈ No )
40 3 39 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ No )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐴 ∈ No )
42 ssltss1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ⊆ No )
43 2 42 syl ⊢ ( 𝜑 → 𝑀 ⊆ No )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑀 ⊆ No )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑞 ∈ 𝑀 )
46 44 45 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑞 ∈ No )
47 41 46 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝑞 ) ∈ No )
48 38 47 addscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) ∈ No )
49 34 46 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝑝 ·s 𝑞 ) ∈ No )
50 48 49 subscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No )
51 eleq1 ⊢ ( 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑎 ∈ No ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No ) )
52 50 51 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑎 ∈ No ) )
53 52 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑎 ∈ No ) )
54 53 abssdv ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ⊆ No )
55 ssltss2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
56 1 55 syl ⊢ ( 𝜑 → 𝑅 ⊆ No )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑅 ⊆ No )
58 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑟 ∈ 𝑅 )
59 57 58 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑟 ∈ No )
60 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐵 ∈ No )
61 59 60 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑟 ·s 𝐵 ) ∈ No )
62 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐴 ∈ No )
63 ssltss2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ⊆ No )
64 2 63 syl ⊢ ( 𝜑 → 𝑆 ⊆ No )
65 64 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑆 ⊆ No )
66 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑠 ∈ 𝑆 )
67 65 66 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑠 ∈ No )
68 62 67 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝑠 ) ∈ No )
69 61 68 addscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) ∈ No )
70 59 67 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑟 ·s 𝑠 ) ∈ No )
71 69 70 subscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No )
72 eleq1 ⊢ ( 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( 𝑏 ∈ No ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No ) )
73 71 72 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → 𝑏 ∈ No ) )
74 73 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → 𝑏 ∈ No ) )
75 74 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ⊆ No )
76 54 75 unssd ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ⊆ No )
77 40 36 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
78 77 snssd ⊢ ( 𝜑 → { ( 𝐴 ·s 𝐵 ) } ⊆ No )
79 elun ⊢ ( 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( 𝑥 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∨ 𝑥 ∈ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) )
80 vex ⊢ 𝑥 ∈ V
81 eqeq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
82 81 2rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
83 80 82 elab ⊢ ( 𝑥 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ↔ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
84 eqeq1 ⊢ ( 𝑏 = 𝑥 → ( 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
85 84 2rexbidv ⊢ ( 𝑏 = 𝑥 → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
86 80 85 elab ⊢ ( 𝑥 ∈ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
87 83 86 orbi12i ⊢ ( ( 𝑥 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∨ 𝑥 ∈ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
88 79 87 bitri ⊢ ( 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
89 38 47 49 addsubsd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) = ( ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) +s ( 𝐴 ·s 𝑞 ) ) )
90 scutcut ⊢ ( 𝐿 <<s 𝑅 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
91 1 90 syl ⊢ ( 𝜑 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
92 91 simp2d ⊢ ( 𝜑 → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
93 92 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
94 ovex ⊢ ( 𝐿 |s 𝑅 ) ∈ V
95 94 snid ⊢ ( 𝐿 |s 𝑅 ) ∈ { ( 𝐿 |s 𝑅 ) }
96 3 95 eqeltrdi ⊢ ( 𝜑 → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
98 93 33 97 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑝 <s 𝐴 )
99 scutcut ⊢ ( 𝑀 <<s 𝑆 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
100 2 99 syl ⊢ ( 𝜑 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
101 100 simp2d ⊢ ( 𝜑 → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
102 101 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
103 ovex ⊢ ( 𝑀 |s 𝑆 ) ∈ V
104 103 snid ⊢ ( 𝑀 |s 𝑆 ) ∈ { ( 𝑀 |s 𝑆 ) }
105 4 104 eqeltrdi ⊢ ( 𝜑 → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
106 105 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
107 102 45 106 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → 𝑞 <s 𝐵 )
108 34 41 46 37 98 107 sltmuld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑞 ) ) )
109 38 49 subscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No )
110 77 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
111 109 47 110 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) +s ( 𝐴 ·s 𝑞 ) ) <s ( 𝐴 ·s 𝐵 ) ↔ ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑞 ) ) ) )
112 108 111 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( ( 𝑝 ·s 𝐵 ) -s ( 𝑝 ·s 𝑞 ) ) +s ( 𝐴 ·s 𝑞 ) ) <s ( 𝐴 ·s 𝐵 ) )
113 89 112 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( 𝐴 ·s 𝐵 ) )
114 breq1 ⊢ ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑥 <s ( 𝐴 ·s 𝐵 ) ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( 𝐴 ·s 𝐵 ) ) )
115 113 114 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐿 ∧ 𝑞 ∈ 𝑀 ) ) → ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
116 115 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
117 61 68 70 addsubsd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) = ( ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) +s ( 𝐴 ·s 𝑠 ) ) )
118 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐿 <<s 𝑅 )
119 118 90 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
120 119 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
121 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐴 = ( 𝐿 |s 𝑅 ) )
122 121 95 eqeltrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
123 120 122 58 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐴 <s 𝑟 )
124 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑀 <<s 𝑆 )
125 124 99 syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
126 125 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
127 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐵 = ( 𝑀 |s 𝑆 ) )
128 127 104 eqeltrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐵 ∈ { ( 𝑀 |s 𝑆 ) } )
129 126 128 66 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐵 <s 𝑠 )
130 62 59 60 67 123 129 sltmuld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝐴 ·s 𝑠 ) -s ( 𝐴 ·s 𝐵 ) ) <s ( ( 𝑟 ·s 𝑠 ) -s ( 𝑟 ·s 𝐵 ) ) )
131 61 70 subscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No )
132 77 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
133 131 68 132 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) +s ( 𝐴 ·s 𝑠 ) ) <s ( 𝐴 ·s 𝐵 ) ↔ ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑠 ) ) ) )
134 61 70 132 68 sltsubsub2bd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝑠 ) ) ↔ ( ( 𝐴 ·s 𝑠 ) -s ( 𝐴 ·s 𝐵 ) ) <s ( ( 𝑟 ·s 𝑠 ) -s ( 𝑟 ·s 𝐵 ) ) ) )
135 133 134 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) +s ( 𝐴 ·s 𝑠 ) ) <s ( 𝐴 ·s 𝐵 ) ↔ ( ( 𝐴 ·s 𝑠 ) -s ( 𝐴 ·s 𝐵 ) ) <s ( ( 𝑟 ·s 𝑠 ) -s ( 𝑟 ·s 𝐵 ) ) ) )
136 130 135 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ·s 𝐵 ) -s ( 𝑟 ·s 𝑠 ) ) +s ( 𝐴 ·s 𝑠 ) ) <s ( 𝐴 ·s 𝐵 ) )
137 117 136 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( 𝐴 ·s 𝐵 ) )
138 breq1 ⊢ ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( 𝑥 <s ( 𝐴 ·s 𝐵 ) ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( 𝐴 ·s 𝐵 ) ) )
139 137 138 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
140 139 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
141 116 140 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
142 88 141 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
143 142 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ) → 𝑥 <s ( 𝐴 ·s 𝐵 ) )
144 velsn ⊢ ( 𝑦 ∈ { ( 𝐴 ·s 𝐵 ) } ↔ 𝑦 = ( 𝐴 ·s 𝐵 ) )
145 breq2 ⊢ ( 𝑦 = ( 𝐴 ·s 𝐵 ) → ( 𝑥 <s 𝑦 ↔ 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
146 144 145 sylbi ⊢ ( 𝑦 ∈ { ( 𝐴 ·s 𝐵 ) } → ( 𝑥 <s 𝑦 ↔ 𝑥 <s ( 𝐴 ·s 𝐵 ) ) )
147 143 146 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ) → ( 𝑦 ∈ { ( 𝐴 ·s 𝐵 ) } → 𝑥 <s 𝑦 ) )
148 147 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∧ 𝑦 ∈ { ( 𝐴 ·s 𝐵 ) } ) → 𝑥 <s 𝑦 )
149 27 29 76 78 148 ssltd ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑝 ∈ 𝐿 ∃ 𝑞 ∈ 𝑀 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s { ( 𝐴 ·s 𝐵 ) } )