Metamath Proof Explorer

Theorem mulsproplem9

Description: Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-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 𝑒 ) ) ) ) ) )
mulsproplem9.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
mulsproplem9.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion mulsproplem9 ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )

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 mulsproplem9.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 mulsproplem9.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
4 eqid ⊢ ( 𝑝 ∈ ( L ‘ 𝐴 ) , 𝑞 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) = ( 𝑝 ∈ ( L ‘ 𝐴 ) , 𝑞 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
5 4 rnmpo ⊢ ran ( 𝑝 ∈ ( L ‘ 𝐴 ) , 𝑞 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) = { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) }
6 fvex ⊢ ( L ‘ 𝐴 ) ∈ V
7 fvex ⊢ ( L ‘ 𝐵 ) ∈ V
8 6 7 mpoex ⊢ ( 𝑝 ∈ ( L ‘ 𝐴 ) , 𝑞 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V
9 8 rnex ⊢ ran ( 𝑝 ∈ ( L ‘ 𝐴 ) , 𝑞 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) ∈ V
10 5 9 eqeltrri ⊢ { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∈ V
11 eqid ⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) , 𝑠 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) = ( 𝑟 ∈ ( R ‘ 𝐴 ) , 𝑠 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
12 11 rnmpo ⊢ ran ( 𝑟 ∈ ( R ‘ 𝐴 ) , 𝑠 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) = { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) }
13 fvex ⊢ ( R ‘ 𝐴 ) ∈ V
14 fvex ⊢ ( R ‘ 𝐵 ) ∈ V
15 13 14 mpoex ⊢ ( 𝑟 ∈ ( R ‘ 𝐴 ) , 𝑠 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V
16 15 rnex ⊢ ran ( 𝑟 ∈ ( R ‘ 𝐴 ) , 𝑠 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∈ V
17 12 16 eqeltrri ⊢ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ∈ V
18 10 17 unex ⊢ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∈ V
19 18 a1i ⊢ ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∈ V )
20 eqid ⊢ ( 𝑡 ∈ ( L ‘ 𝐴 ) , 𝑢 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) = ( 𝑡 ∈ ( L ‘ 𝐴 ) , 𝑢 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
21 20 rnmpo ⊢ ran ( 𝑡 ∈ ( L ‘ 𝐴 ) , 𝑢 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) = { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) }
22 6 14 mpoex ⊢ ( 𝑡 ∈ ( L ‘ 𝐴 ) , 𝑢 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V
23 22 rnex ⊢ ran ( 𝑡 ∈ ( L ‘ 𝐴 ) , 𝑢 ∈ ( R ‘ 𝐵 ) ↦ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∈ V
24 21 23 eqeltrri ⊢ { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∈ V
25 eqid ⊢ ( 𝑣 ∈ ( R ‘ 𝐴 ) , 𝑤 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) = ( 𝑣 ∈ ( R ‘ 𝐴 ) , 𝑤 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
26 25 rnmpo ⊢ ran ( 𝑣 ∈ ( R ‘ 𝐴 ) , 𝑤 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) = { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) }
27 13 7 mpoex ⊢ ( 𝑣 ∈ ( R ‘ 𝐴 ) , 𝑤 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V
28 27 rnex ⊢ ran ( 𝑣 ∈ ( R ‘ 𝐴 ) , 𝑤 ∈ ( L ‘ 𝐵 ) ↦ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ∈ V
29 26 28 eqeltrri ⊢ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ∈ V
30 24 29 unex ⊢ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ∈ V
31 30 a1i ⊢ ( 𝜑 → ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ∈ V )
32 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
33 leftssold ⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
34 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
35 33 34 sselid ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑝 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
36 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
37 32 35 36 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑝 ·s 𝐵 ) ∈ No )
38 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
39 leftssold ⊢ ( L ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
40 simprr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
41 39 40 sselid ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑞 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
42 32 38 41 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑞 ) ∈ No )
43 37 42 addscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) ∈ No )
44 32 35 41 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑝 ·s 𝑞 ) ∈ No )
45 43 44 subscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No )
46 eleq1 ⊢ ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑔 ∈ No ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No ) )
47 45 46 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑔 ∈ No ) )
48 47 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑔 ∈ No ) )
49 48 abssdv ⊢ ( 𝜑 → { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ⊆ No )
50 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
51 rightssold ⊢ ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
52 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
53 51 52 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑟 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
54 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
55 50 53 54 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑟 ·s 𝐵 ) ∈ No )
56 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
57 rightssold ⊢ ( R ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
58 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
59 57 58 sselid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑠 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
60 50 56 59 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑠 ) ∈ No )
61 55 60 addscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) ∈ No )
62 50 53 59 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑟 ·s 𝑠 ) ∈ No )
63 61 62 subscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No )
64 eleq1 ⊢ ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ℎ ∈ No ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No ) )
65 63 64 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ℎ ∈ No ) )
66 65 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ℎ ∈ No ) )
67 66 abssdv ⊢ ( 𝜑 → { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ⊆ No )
68 49 67 unssd ⊢ ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ⊆ No )
69 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
70 simprl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
71 33 70 sselid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑡 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
72 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
73 69 71 72 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑡 ·s 𝐵 ) ∈ No )
74 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
75 simprr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
76 57 75 sselid ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑢 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
77 69 74 76 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑢 ) ∈ No )
78 73 77 addscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) ∈ No )
79 69 71 76 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑡 ·s 𝑢 ) ∈ No )
80 78 79 subscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No )
81 eleq1 ⊢ ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( 𝑖 ∈ No ↔ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No ) )
82 80 81 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑖 ∈ No ) )
83 82 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑖 ∈ No ) )
84 83 abssdv ⊢ ( 𝜑 → { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ⊆ No )
85 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
86 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
87 51 86 sselid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑣 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
88 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
89 85 87 88 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑣 ·s 𝐵 ) ∈ No )
90 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
91 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
92 39 91 sselid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑤 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
93 85 90 92 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑤 ) ∈ No )
94 89 93 addscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) ∈ No )
95 85 87 92 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑣 ·s 𝑤 ) ∈ No )
96 94 95 subscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No )
97 eleq1 ⊢ ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( 𝑗 ∈ No ↔ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No ) )
98 96 97 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑗 ∈ No ) )
99 98 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑗 ∈ No ) )
100 99 abssdv ⊢ ( 𝜑 → { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ⊆ No )
101 84 100 unssd ⊢ ( 𝜑 → ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ⊆ No )
102 elun ⊢ ( 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( 𝑥 ∈ { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∨ 𝑥 ∈ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) )
103 vex ⊢ 𝑥 ∈ V
104 eqeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
105 104 2rexbidv ⊢ ( 𝑔 = 𝑥 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
106 103 105 elab ⊢ ( 𝑥 ∈ { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ↔ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
107 eqeq1 ⊢ ( ℎ = 𝑥 → ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
108 107 2rexbidv ⊢ ( ℎ = 𝑥 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
109 103 108 elab ⊢ ( 𝑥 ∈ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
110 106 109 orbi12i ⊢ ( ( 𝑥 ∈ { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∨ 𝑥 ∈ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
111 102 110 bitri ⊢ ( 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ↔ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
112 elun ⊢ ( 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( 𝑦 ∈ { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∨ 𝑦 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )
113 vex ⊢ 𝑦 ∈ V
114 eqeq1 ⊢ ( 𝑖 = 𝑦 → ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
115 114 2rexbidv ⊢ ( 𝑖 = 𝑦 → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
116 113 115 elab ⊢ ( 𝑦 ∈ { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ↔ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
117 eqeq1 ⊢ ( 𝑗 = 𝑦 → ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
118 117 2rexbidv ⊢ ( 𝑗 = 𝑦 → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
119 113 118 elab ⊢ ( 𝑦 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ↔ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
120 116 119 orbi12i ⊢ ( ( 𝑦 ∈ { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∨ 𝑦 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
121 112 120 bitri ⊢ ( 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ↔ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
122 111 121 anbi12i ⊢ ( ( 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∧ 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) ↔ ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∧ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) )
123 anddi ⊢ ( ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∨ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) ∧ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∨ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ↔ ( ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ∨ ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ) )
124 122 123 bitri ⊢ ( ( 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∧ 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) ↔ ( ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ∨ ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ) )
125 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
126 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
127 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
128 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
129 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
130 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
131 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
132 125 126 127 128 129 130 131 mulsproplem5 ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
133 breq2 ⊢ ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
134 132 133 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
135 134 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
136 135 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
137 breq1 ⊢ ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑥 <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
138 137 imbi2d ⊢ ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ↔ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) ) )
139 136 138 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
140 139 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
141 140 impd ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) → 𝑥 <s 𝑦 ) )
142 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
143 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
144 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
145 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
146 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
147 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
148 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
149 142 143 144 145 146 147 148 mulsproplem6 ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
150 breq2 ⊢ ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
151 149 150 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
152 151 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
153 152 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
154 137 imbi2d ⊢ ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ↔ ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) ) )
155 153 154 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
156 155 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
157 156 impd ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) → 𝑥 <s 𝑦 ) )
158 141 157 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) → 𝑥 <s 𝑦 ) )
159 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
160 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
161 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
162 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
163 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
164 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
165 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
166 159 160 161 162 163 164 165 mulsproplem7 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
167 breq2 ⊢ ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
168 166 167 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
169 168 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
170 169 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
171 breq1 ⊢ ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( 𝑥 <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
172 171 imbi2d ⊢ ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ↔ ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) ) )
173 170 172 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
174 173 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
175 174 impd ⊢ ( 𝜑 → ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) → 𝑥 <s 𝑦 ) )
176 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
177 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
178 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
179 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
180 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
181 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
182 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
183 176 177 178 179 180 181 182 mulsproplem8 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
184 breq2 ⊢ ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
185 183 184 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
186 185 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
187 186 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
188 171 imbi2d ⊢ ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ↔ ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) ) )
189 187 188 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
190 189 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
191 190 impd ⊢ ( 𝜑 → ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) → 𝑥 <s 𝑦 ) )
192 175 191 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) → 𝑥 <s 𝑦 ) )
193 158 192 jaod ⊢ ( 𝜑 → ( ( ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ∨ ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) ∨ ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) ) ) → 𝑥 <s 𝑦 ) )
194 124 193 biimtrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∧ 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) → 𝑥 <s 𝑦 ) )
195 194 3impib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ∧ 𝑦 ∈ ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) → 𝑥 <s 𝑦 )
196 19 31 68 101 195 ssltd ⊢ ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) <<s ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) )