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 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
34 33 leftoldd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑝 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
35 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
36 32 34 35 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑝 ·s 𝐵 ) ∈ No )
37 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
39 38 leftoldd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → 𝑞 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
40 32 37 39 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑞 ) ∈ No )
41 36 40 addscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) ∈ No )
42 32 34 39 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑝 ·s 𝑞 ) ∈ No )
43 41 42 subscld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No )
44 eleq1 ⊢ ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑔 ∈ No ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∈ No ) )
45 43 44 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑔 ∈ No ) )
46 45 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → 𝑔 ∈ No ) )
47 46 abssdv ⊢ ( 𝜑 → { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ⊆ No )
48 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 𝑒 ) ) ) ) ) )
49 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
50 49 rightoldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑟 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
51 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
52 48 50 51 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑟 ·s 𝐵 ) ∈ No )
53 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
54 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
55 54 rightoldd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → 𝑠 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
56 48 53 55 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑠 ) ∈ No )
57 52 56 addscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) ∈ No )
58 48 50 55 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑟 ·s 𝑠 ) ∈ No )
59 57 58 subscld ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No )
60 eleq1 ⊢ ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ℎ ∈ No ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∈ No ) )
61 59 60 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ℎ ∈ No ) )
62 61 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ℎ ∈ No ) )
63 62 abssdv ⊢ ( 𝜑 → { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ⊆ No )
64 47 63 unssd ⊢ ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) ⊆ No )
65 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 𝑒 ) ) ) ) ) )
66 simprl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
67 66 leftoldd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑡 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
68 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
69 65 67 68 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑡 ·s 𝐵 ) ∈ No )
70 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
71 simprr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
72 71 rightoldd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → 𝑢 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
73 65 70 72 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑢 ) ∈ No )
74 69 73 addscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) ∈ No )
75 65 67 72 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑡 ·s 𝑢 ) ∈ No )
76 74 75 subscld ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No )
77 eleq1 ⊢ ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( 𝑖 ∈ No ↔ ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ∈ No ) )
78 76 77 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑖 ∈ No ) )
79 78 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑖 ∈ No ) )
80 79 abssdv ⊢ ( 𝜑 → { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ⊆ No )
81 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 𝑒 ) ) ) ) ) )
82 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
83 82 rightoldd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑣 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
84 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
85 81 83 84 mulsproplem2 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑣 ·s 𝐵 ) ∈ No )
86 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
87 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
88 87 leftoldd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → 𝑤 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
89 81 86 88 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑤 ) ∈ No )
90 85 89 addscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) ∈ No )
91 81 83 88 mulsproplem4 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑣 ·s 𝑤 ) ∈ No )
92 90 91 subscld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No )
93 eleq1 ⊢ ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( 𝑗 ∈ No ↔ ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ∈ No ) )
94 92 93 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑗 ∈ No ) )
95 94 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑗 ∈ No ) )
96 95 abssdv ⊢ ( 𝜑 → { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ⊆ No )
97 80 96 unssd ⊢ ( 𝜑 → ( { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ⊆ No )
98 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 𝑠 ) ) } ) )
99 vex ⊢ 𝑥 ∈ V
100 eqeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
101 100 2rexbidv ⊢ ( 𝑔 = 𝑥 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
102 99 101 elab ⊢ ( 𝑥 ∈ { 𝑔 ∣ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑔 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ↔ ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
103 eqeq1 ⊢ ( ℎ = 𝑥 → ( ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
104 103 2rexbidv ⊢ ( ℎ = 𝑥 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
105 99 104 elab ⊢ ( 𝑥 ∈ { ℎ ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) ℎ = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
106 102 105 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 𝑠 ) ) ) )
107 98 106 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 𝑠 ) ) ) )
108 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 𝑤 ) ) } ) )
109 vex ⊢ 𝑦 ∈ V
110 eqeq1 ⊢ ( 𝑖 = 𝑦 → ( 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
111 110 2rexbidv ⊢ ( 𝑖 = 𝑦 → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
112 109 111 elab ⊢ ( 𝑦 ∈ { 𝑖 ∣ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑖 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ↔ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
113 eqeq1 ⊢ ( 𝑗 = 𝑦 → ( 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
114 113 2rexbidv ⊢ ( 𝑗 = 𝑦 → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
115 109 114 elab ⊢ ( 𝑦 ∈ { 𝑗 ∣ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑗 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ↔ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
116 112 115 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 𝑤 ) ) ) )
117 108 116 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 𝑤 ) ) ) )
118 107 117 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 𝑤 ) ) ) ) )
119 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 𝑤 ) ) ) ) ) )
120 118 119 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 𝑤 ) ) ) ) ) )
121 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 𝑒 ) ) ) ) ) )
122 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
123 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
124 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
125 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
126 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
127 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
128 121 122 123 124 125 126 127 mulsproplem5 ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
129 breq2 ⊢ ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
130 128 129 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
131 130 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
132 131 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
133 breq1 ⊢ ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( 𝑥 <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
134 133 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 𝑦 ) ) )
135 132 134 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
136 135 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
137 136 impd ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) → 𝑥 <s 𝑦 ) )
138 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 𝑒 ) ) ) ) ) )
139 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
140 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
141 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑝 ∈ ( L ‘ 𝐴 ) )
142 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( L ‘ 𝐵 ) )
143 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
144 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
145 138 139 140 141 142 143 144 mulsproplem6 ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
146 breq2 ⊢ ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ↔ ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
147 145 146 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
148 147 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
149 148 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) <s 𝑦 ) )
150 133 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 𝑦 ) ) )
151 149 150 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( L ‘ 𝐴 ) ∧ 𝑞 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
152 151 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
153 152 impd ⊢ ( 𝜑 → ( ( ∃ 𝑝 ∈ ( L ‘ 𝐴 ) ∃ 𝑞 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) → 𝑥 <s 𝑦 ) )
154 137 153 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 𝑦 ) )
155 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 𝑒 ) ) ) ) ) )
156 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
157 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
158 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
159 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
160 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑡 ∈ ( L ‘ 𝐴 ) )
161 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → 𝑢 ∈ ( R ‘ 𝐵 ) )
162 155 156 157 158 159 160 161 mulsproplem7 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
163 breq2 ⊢ ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) )
164 162 163 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
165 164 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) ∧ ( 𝑡 ∈ ( L ‘ 𝐴 ) ∧ 𝑢 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
166 165 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
167 breq1 ⊢ ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( 𝑥 <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
168 167 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 𝑦 ) ) )
169 166 168 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
170 169 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) → 𝑥 <s 𝑦 ) ) )
171 170 impd ⊢ ( 𝜑 → ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑡 ∈ ( L ‘ 𝐴 ) ∃ 𝑢 ∈ ( R ‘ 𝐵 ) 𝑦 = ( ( ( 𝑡 ·s 𝐵 ) +s ( 𝐴 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ) → 𝑥 <s 𝑦 ) )
172 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 𝑒 ) ) ) ) ) )
173 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐴 ∈ No )
174 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝐵 ∈ No )
175 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ( R ‘ 𝐴 ) )
176 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑠 ∈ ( R ‘ 𝐵 ) )
177 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑣 ∈ ( R ‘ 𝐴 ) )
178 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → 𝑤 ∈ ( L ‘ 𝐵 ) )
179 172 173 174 175 176 177 178 mulsproplem8 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
180 breq2 ⊢ ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ↔ ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) )
181 179 180 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
182 181 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) ∧ ( 𝑣 ∈ ( R ‘ 𝐴 ) ∧ 𝑤 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
183 182 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) <s 𝑦 ) )
184 167 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 𝑦 ) ) )
185 183 184 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( R ‘ 𝐴 ) ∧ 𝑠 ∈ ( R ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
186 185 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) → ( ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) → 𝑥 <s 𝑦 ) ) )
187 186 impd ⊢ ( 𝜑 → ( ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑥 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ∧ ∃ 𝑣 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ ( L ‘ 𝐵 ) 𝑦 = ( ( ( 𝑣 ·s 𝐵 ) +s ( 𝐴 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ) → 𝑥 <s 𝑦 ) )
188 171 187 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 𝑦 ) )
189 154 188 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 𝑦 ) )
190 120 189 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 𝑦 ) )
191 190 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 𝑦 )
192 19 31 64 97 191 sltsd ⊢ ( 𝜑 → ( { 𝑔 ∣ ∃ 𝑝 ∈ ( 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 𝑤 ) ) } ) )