Metamath Proof Explorer

Theorem precsexlem11

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for A . (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 ) )
precsexlem.7 ⊢ 𝑌 = ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) )
Assertion precsexlem11 ( 𝜑 → ( 𝐴 ·s 𝑌 ) = 1s )

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 precsexlem.7 ⊢ 𝑌 = ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) )
8 lltropt ⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
9 4 5 0elleft ⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )
10 9 snssd ⊢ ( 𝜑 → { 0s } ⊆ ( L ‘ 𝐴 ) )
11 ssrab2 ⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ ( L ‘ 𝐴 )
12 11 a1i ⊢ ( 𝜑 → { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ ( L ‘ 𝐴 ) )
13 10 12 unssd ⊢ ( 𝜑 → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ⊆ ( L ‘ 𝐴 ) )
14 sssslt1 ⊢ ( ( ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) ∧ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ⊆ ( L ‘ 𝐴 ) ) → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) <<s ( R ‘ 𝐴 ) )
15 8 13 14 sylancr ⊢ ( 𝜑 → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) <<s ( R ‘ 𝐴 ) )
16 1 2 3 4 5 6 precsexlem10 ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) )
17 4 5 cutpos ⊢ ( 𝜑 → 𝐴 = ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) |s ( R ‘ 𝐴 ) ) )
18 7 a1i ⊢ ( 𝜑 → 𝑌 = ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) )
19 15 16 17 18 mulsunif ⊢ ( 𝜑 → ( 𝐴 ·s 𝑌 ) = ( ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) |s ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) )
20 0sno ⊢ 0s ∈ No
21 20 elexi ⊢ 0s ∈ V
22 21 snid ⊢ 0s ∈ { 0s }
23 elun1 ⊢ ( 0s ∈ { 0s } → 0s ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) )
24 22 23 ax-mp ⊢ 0s ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } )
25 peano1 ⊢ ∅ ∈ ω
26 1 2 3 precsexlem1 ⊢ ( 𝐿 ‘ ∅ ) = { 0s }
27 22 26 eleqtrri ⊢ 0s ∈ ( 𝐿 ‘ ∅ )
28 fveq2 ⊢ ( 𝑏 = ∅ → ( 𝐿 ‘ 𝑏 ) = ( 𝐿 ‘ ∅ ) )
29 28 eleq2d ⊢ ( 𝑏 = ∅ → ( 0s ∈ ( 𝐿 ‘ 𝑏 ) ↔ 0s ∈ ( 𝐿 ‘ ∅ ) ) )
30 29 rspcev ⊢ ( ( ∅ ∈ ω ∧ 0s ∈ ( 𝐿 ‘ ∅ ) ) → ∃ 𝑏 ∈ ω 0s ∈ ( 𝐿 ‘ 𝑏 ) )
31 25 27 30 mp2an ⊢ ∃ 𝑏 ∈ ω 0s ∈ ( 𝐿 ‘ 𝑏 )
32 eliun ⊢ ( 0s ∈ ∪ 𝑏 ∈ ω ( 𝐿 ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ ω 0s ∈ ( 𝐿 ‘ 𝑏 ) )
33 31 32 mpbir ⊢ 0s ∈ ∪ 𝑏 ∈ ω ( 𝐿 ‘ 𝑏 )
34 fo1st ⊢ 1st : V –onto→ V
35 fofun ⊢ ( 1st : V –onto→ V → Fun 1st )
36 34 35 ax-mp ⊢ Fun 1st
37 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 } , ∅ ⟩ )
38 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 } , ∅ ⟩ ) )
39 37 38 mpbir ⊢ Fun 𝐹
40 funco ⊢ ( ( Fun 1st ∧ Fun 𝐹 ) → Fun ( 1st ∘ 𝐹 ) )
41 36 39 40 mp2an ⊢ Fun ( 1st ∘ 𝐹 )
42 2 funeqi ⊢ ( Fun 𝐿 ↔ Fun ( 1st ∘ 𝐹 ) )
43 41 42 mpbir ⊢ Fun 𝐿
44 funiunfv ⊢ ( Fun 𝐿 → ∪ 𝑏 ∈ ω ( 𝐿 ‘ 𝑏 ) = ∪ ( 𝐿 “ ω ) )
45 43 44 ax-mp ⊢ ∪ 𝑏 ∈ ω ( 𝐿 ‘ 𝑏 ) = ∪ ( 𝐿 “ ω )
46 33 45 eleqtri ⊢ 0s ∈ ∪ ( 𝐿 “ ω )
47 addsrid ⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
48 20 47 ax-mp ⊢ ( 0s +s 0s ) = 0s
49 muls01 ⊢ ( 0s ∈ No → ( 0s ·s 0s ) = 0s )
50 20 49 ax-mp ⊢ ( 0s ·s 0s ) = 0s
51 48 50 oveq12i ⊢ ( ( 0s +s 0s ) -s ( 0s ·s 0s ) ) = ( 0s -s 0s )
52 subsid ⊢ ( 0s ∈ No → ( 0s -s 0s ) = 0s )
53 20 52 ax-mp ⊢ ( 0s -s 0s ) = 0s
54 51 53 eqtr2i ⊢ 0s = ( ( 0s +s 0s ) -s ( 0s ·s 0s ) )
55 16 scutcld ⊢ ( 𝜑 → ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) ∈ No )
56 7 55 eqeltrid ⊢ ( 𝜑 → 𝑌 ∈ No )
57 muls02 ⊢ ( 𝑌 ∈ No → ( 0s ·s 𝑌 ) = 0s )
58 56 57 syl ⊢ ( 𝜑 → ( 0s ·s 𝑌 ) = 0s )
59 muls01 ⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
60 4 59 syl ⊢ ( 𝜑 → ( 𝐴 ·s 0s ) = 0s )
61 58 60 oveq12d ⊢ ( 𝜑 → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) = ( 0s +s 0s ) )
62 61 oveq1d ⊢ ( 𝜑 → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) -s ( 0s ·s 0s ) ) = ( ( 0s +s 0s ) -s ( 0s ·s 0s ) ) )
63 54 62 eqtr4id ⊢ ( 𝜑 → 0s = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) -s ( 0s ·s 0s ) ) )
64 oveq1 ⊢ ( 𝑐 = 0s → ( 𝑐 ·s 𝑌 ) = ( 0s ·s 𝑌 ) )
65 64 oveq1d ⊢ ( 𝑐 = 0s → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) )
66 oveq1 ⊢ ( 𝑐 = 0s → ( 𝑐 ·s 𝑑 ) = ( 0s ·s 𝑑 ) )
67 65 66 oveq12d ⊢ ( 𝑐 = 0s → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) )
68 67 eqeq2d ⊢ ( 𝑐 = 0s → ( 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 0s = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) )
69 oveq2 ⊢ ( 𝑑 = 0s → ( 𝐴 ·s 𝑑 ) = ( 𝐴 ·s 0s ) )
70 69 oveq2d ⊢ ( 𝑑 = 0s → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) )
71 oveq2 ⊢ ( 𝑑 = 0s → ( 0s ·s 𝑑 ) = ( 0s ·s 0s ) )
72 70 71 oveq12d ⊢ ( 𝑑 = 0s → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) -s ( 0s ·s 0s ) ) )
73 72 eqeq2d ⊢ ( 𝑑 = 0s → ( 0s = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ↔ 0s = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) -s ( 0s ·s 0s ) ) ) )
74 68 73 rspc2ev ⊢ ( ( 0s ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 0s ∈ ∪ ( 𝐿 “ ω ) ∧ 0s = ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 0s ) ) -s ( 0s ·s 0s ) ) ) → ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
75 24 46 63 74 mp3an12i ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
76 eqeq1 ⊢ ( 𝑏 = 0s → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
77 76 2rexbidv ⊢ ( 𝑏 = 0s → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
78 21 77 elab ⊢ ( 0s ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 0s = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
79 75 78 sylibr ⊢ ( 𝜑 → 0s ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } )
80 elun1 ⊢ ( 0s ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } → 0s ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
81 79 80 syl ⊢ ( 𝜑 → 0s ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
82 eqid ⊢ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
83 82 rnmpo ⊢ ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
84 ssltex1 ⊢ ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) <<s ( R ‘ 𝐴 ) → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∈ V )
85 15 84 syl ⊢ ( 𝜑 → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∈ V )
86 ssltex1 ⊢ ( ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) → ∪ ( 𝐿 “ ω ) ∈ V )
87 16 86 syl ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) ∈ V )
88 mpoexga ⊢ ( ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∈ V ∧ ∪ ( 𝐿 “ ω ) ∈ V ) → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
89 85 87 88 syl2anc ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
90 rnexg ⊢ ( ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
91 89 90 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
92 83 91 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
93 eqid ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
94 93 rnmpo ⊢ ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
95 fvex ⊢ ( R ‘ 𝐴 ) ∈ V
96 ssltex2 ⊢ ( ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) → ∪ ( 𝑅 “ ω ) ∈ V )
97 16 96 syl ⊢ ( 𝜑 → ∪ ( 𝑅 “ ω ) ∈ V )
98 mpoexga ⊢ ( ( ( R ‘ 𝐴 ) ∈ V ∧ ∪ ( 𝑅 “ ω ) ∈ V ) → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
99 95 97 98 sylancr ⊢ ( 𝜑 → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
100 rnexg ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
101 99 100 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
102 94 101 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
103 92 102 unexd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ∈ V )
104 snex ⊢ { 1s } ∈ V
105 104 a1i ⊢ ( 𝜑 → { 1s } ∈ V )
106 ssltss1 ⊢ ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) <<s ( R ‘ 𝐴 ) → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ⊆ No )
107 15 106 syl ⊢ ( 𝜑 → ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ⊆ No )
108 107 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ) → 𝑐 ∈ No )
109 108 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑐 ∈ No )
110 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ No )
111 109 110 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
112 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝐴 ∈ No )
113 ssltss1 ⊢ ( ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) → ∪ ( 𝐿 “ ω ) ⊆ No )
114 16 113 syl ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) ⊆ No )
115 114 sselda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → 𝑑 ∈ No )
116 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑑 ∈ No )
117 112 116 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
118 111 117 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
119 109 116 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
120 118 119 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
121 eleq1 ⊢ ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → ( 𝑏 ∈ No ↔ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No ) )
122 120 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
123 122 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
124 123 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
125 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
126 125 a1i ⊢ ( 𝜑 → ( R ‘ 𝐴 ) ⊆ No )
127 126 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝑐 ∈ No )
128 127 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑐 ∈ No )
129 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ No )
130 128 129 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
131 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝐴 ∈ No )
132 ssltss2 ⊢ ( ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) → ∪ ( 𝑅 “ ω ) ⊆ No )
133 16 132 syl ⊢ ( 𝜑 → ∪ ( 𝑅 “ ω ) ⊆ No )
134 133 sselda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 𝑑 ∈ No )
135 134 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑑 ∈ No )
136 131 135 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
137 130 136 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
138 128 135 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
139 137 138 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
140 139 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
141 140 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
142 141 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
143 124 142 unssd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ⊆ No )
144 1sno ⊢ 1s ∈ No
145 snssi ⊢ ( 1s ∈ No → { 1s } ⊆ No )
146 144 145 mp1i ⊢ ( 𝜑 → { 1s } ⊆ No )
147 elun ⊢ ( 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∨ 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
148 vex ⊢ 𝑒 ∈ V
149 eqeq1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
150 149 2rexbidv ⊢ ( 𝑏 = 𝑒 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
151 148 150 elab ⊢ ( 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
152 149 2rexbidv ⊢ ( 𝑏 = 𝑒 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
153 148 152 elab ⊢ ( 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
154 151 153 orbi12i ⊢ ( ( 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∨ 𝑒 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
155 147 154 bitri ⊢ ( 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
156 elun ⊢ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ↔ ( 𝑐 ∈ { 0s } ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) )
157 velsn ⊢ ( 𝑐 ∈ { 0s } ↔ 𝑐 = 0s )
158 157 orbi1i ⊢ ( ( 𝑐 ∈ { 0s } ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ↔ ( 𝑐 = 0s ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) )
159 156 158 bitri ⊢ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ↔ ( 𝑐 = 0s ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) )
160 58 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( 0s ·s 𝑌 ) = 0s )
161 160 oveq1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 0s +s ( 𝐴 ·s 𝑑 ) ) )
162 muls02 ⊢ ( 𝑑 ∈ No → ( 0s ·s 𝑑 ) = 0s )
163 115 162 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( 0s ·s 𝑑 ) = 0s )
164 161 163 oveq12d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( ( 0s +s ( 𝐴 ·s 𝑑 ) ) -s 0s ) )
165 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → 𝐴 ∈ No )
166 165 115 mulscld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
167 addslid ⊢ ( ( 𝐴 ·s 𝑑 ) ∈ No → ( 0s +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
168 166 167 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( 0s +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
169 168 oveq1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( 0s +s ( 𝐴 ·s 𝑑 ) ) -s 0s ) = ( ( 𝐴 ·s 𝑑 ) -s 0s ) )
170 subsid1 ⊢ ( ( 𝐴 ·s 𝑑 ) ∈ No → ( ( 𝐴 ·s 𝑑 ) -s 0s ) = ( 𝐴 ·s 𝑑 ) )
171 166 170 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( 𝐴 ·s 𝑑 ) -s 0s ) = ( 𝐴 ·s 𝑑 ) )
172 164 169 171 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
173 eliun ⊢ ( 𝑑 ∈ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) )
174 funiunfv ⊢ ( Fun 𝐿 → ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) = ∪ ( 𝐿 “ ω ) )
175 43 174 ax-mp ⊢ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) = ∪ ( 𝐿 “ ω )
176 175 eleq2i ⊢ ( 𝑑 ∈ ∪ 𝑖 ∈ ω ( 𝐿 ‘ 𝑖 ) ↔ 𝑑 ∈ ∪ ( 𝐿 “ ω ) )
177 173 176 bitr3i ⊢ ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ↔ 𝑑 ∈ ∪ ( 𝐿 “ ω ) )
178 1 2 3 4 5 6 precsexlem9 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ( ∀ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑑 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
179 178 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ∀ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑑 ) <s 1s )
180 rsp ⊢ ( ∀ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑑 ) <s 1s → ( 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ( 𝐴 ·s 𝑑 ) <s 1s ) )
181 179 180 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ω ) → ( 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ( 𝐴 ·s 𝑑 ) <s 1s ) )
182 181 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ( 𝐴 ·s 𝑑 ) <s 1s ) )
183 177 182 biimtrrid ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( 𝐴 ·s 𝑑 ) <s 1s ) )
184 183 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( 𝐴 ·s 𝑑 ) <s 1s )
185 172 184 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) <s 1s )
186 185 ex ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) <s 1s ) )
187 67 breq1d ⊢ ( 𝑐 = 0s → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) <s 1s ) )
188 187 imbi2d ⊢ ( 𝑐 = 0s → ( ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) ↔ ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) <s 1s ) ) )
189 186 188 syl5ibrcom ⊢ ( 𝜑 → ( 𝑐 = 0s → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) ) )
190 scutcut ⊢ ( ∪ ( 𝐿 “ ω ) <<s ∪ ( 𝑅 “ ω ) → ( ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) ∈ No ∧ ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } ∧ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } <<s ∪ ( 𝑅 “ ω ) ) )
191 16 190 syl ⊢ ( 𝜑 → ( ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) ∈ No ∧ ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } ∧ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } <<s ∪ ( 𝑅 “ ω ) ) )
192 191 simp3d ⊢ ( 𝜑 → { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } <<s ∪ ( 𝑅 “ ω ) )
193 192 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } <<s ∪ ( 𝑅 “ ω ) )
194 ovex ⊢ ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) ∈ V
195 194 snid ⊢ ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) }
196 7 195 eqeltri ⊢ 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) }
197 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
198 peano2 ⊢ ( 𝑖 ∈ ω → suc 𝑖 ∈ ω )
199 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
200 eqid ⊢ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 )
201 oveq1 ⊢ ( 𝑥𝐿 = 𝑐 → ( 𝑥𝐿 -s 𝐴 ) = ( 𝑐 -s 𝐴 ) )
202 201 oveq1d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) )
203 202 oveq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) )
204 id ⊢ ( 𝑥𝐿 = 𝑐 → 𝑥𝐿 = 𝑐 )
205 203 204 oveq12d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) )
206 205 eqeq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) ) )
207 oveq2 ⊢ ( 𝑦𝐿 = 𝑑 → ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) )
208 207 oveq2d ⊢ ( 𝑦𝐿 = 𝑑 → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
209 208 oveq1d ⊢ ( 𝑦𝐿 = 𝑑 → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) )
210 209 eqeq2d ⊢ ( 𝑦𝐿 = 𝑑 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) )
211 206 210 rspc2ev ⊢ ( ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
212 200 211 mp3an3 ⊢ ( ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
213 212 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
214 ovex ⊢ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ V
215 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
216 215 2rexbidv ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
217 214 216 elab ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
218 213 217 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } )
219 elun1 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) )
220 elun2 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
221 218 219 220 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
222 1 2 3 precsexlem5 ⊢ ( 𝑖 ∈ ω → ( 𝑅 ‘ suc 𝑖 ) = ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
223 222 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( 𝑅 ‘ suc 𝑖 ) = ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
224 221 223 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ suc 𝑖 ) )
225 fveq2 ⊢ ( 𝑗 = suc 𝑖 → ( 𝑅 ‘ 𝑗 ) = ( 𝑅 ‘ suc 𝑖 ) )
226 225 eleq2d ⊢ ( 𝑗 = suc 𝑖 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ suc 𝑖 ) ) )
227 226 rspcev ⊢ ( ( suc 𝑖 ∈ ω ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ suc 𝑖 ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) )
228 199 224 227 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) )
229 228 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) ) )
230 eliun ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) )
231 fo2nd ⊢ 2nd : V –onto→ V
232 fofun ⊢ ( 2nd : V –onto→ V → Fun 2nd )
233 231 232 ax-mp ⊢ Fun 2nd
234 funco ⊢ ( ( Fun 2nd ∧ Fun 𝐹 ) → Fun ( 2nd ∘ 𝐹 ) )
235 233 39 234 mp2an ⊢ Fun ( 2nd ∘ 𝐹 )
236 3 funeqi ⊢ ( Fun 𝑅 ↔ Fun ( 2nd ∘ 𝐹 ) )
237 235 236 mpbir ⊢ Fun 𝑅
238 funiunfv ⊢ ( Fun 𝑅 → ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) = ∪ ( 𝑅 “ ω ) )
239 237 238 ax-mp ⊢ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) = ∪ ( 𝑅 “ ω )
240 239 eleq2i ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) )
241 230 240 bitr3i ⊢ ( ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) )
242 229 177 241 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) ) )
243 242 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) )
244 193 197 243 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 <s ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) )
245 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ No )
246 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 1s ∈ No )
247 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
248 11 247 sstri ⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ No
249 248 sseli ⊢ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 𝑐 ∈ No )
250 249 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑐 ∈ No )
251 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝐴 ∈ No )
252 250 251 subscld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑐 -s 𝐴 ) ∈ No )
253 252 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
254 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑑 ∈ No )
255 253 254 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
256 246 255 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
257 249 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑐 ∈ No )
258 breq2 ⊢ ( 𝑥 = 𝑐 → ( 0s <s 𝑥 ↔ 0s <s 𝑐 ) )
259 258 elrab ⊢ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ↔ ( 𝑐 ∈ ( L ‘ 𝐴 ) ∧ 0s <s 𝑐 ) )
260 259 simprbi ⊢ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 0s <s 𝑐 )
261 260 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 0s <s 𝑐 )
262 260 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 0s <s 𝑐 )
263 breq2 ⊢ ( 𝑥𝑂 = 𝑐 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑐 ) )
264 oveq1 ⊢ ( 𝑥𝑂 = 𝑐 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑐 ·s 𝑦 ) )
265 264 eqeq1d ⊢ ( 𝑥𝑂 = 𝑐 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑐 ·s 𝑦 ) = 1s ) )
266 265 rexbidv ⊢ ( 𝑥𝑂 = 𝑐 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s ) )
267 263 266 imbi12d ⊢ ( 𝑥𝑂 = 𝑐 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑐 → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s ) ) )
268 6 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
269 ssun1 ⊢ ( L ‘ 𝐴 ) ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
270 11 269 sstri ⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
271 270 sseli ⊢ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
272 271 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
273 267 268 272 rspcdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 0s <s 𝑐 → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s ) )
274 262 273 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
275 274 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
276 245 256 257 261 275 sltmuldiv2wd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ↔ 𝑌 <s ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) )
277 244 276 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
278 257 254 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
279 166 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
280 246 278 279 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
281 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝐴 ∈ No )
282 257 281 254 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
283 282 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
284 280 283 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
285 277 284 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) )
286 56 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑌 ∈ No )
287 250 286 mulscld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑐 ·s 𝑌 ) ∈ No )
288 287 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
289 288 279 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
290 289 278 246 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ) )
291 246 278 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
292 288 279 291 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
293 290 292 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
294 285 293 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s )
295 294 exp32 ⊢ ( 𝜑 → ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) ) )
296 189 295 jaod ⊢ ( 𝜑 → ( ( 𝑐 = 0s ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) ) )
297 159 296 biimtrid ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) ) )
298 297 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s )
299 breq1 ⊢ ( 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → ( 𝑒 <s 1s ↔ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ) )
300 298 299 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
301 300 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
302 192 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } <<s ∪ ( 𝑅 “ ω ) )
303 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
304 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
305 oveq1 ⊢ ( 𝑥𝑅 = 𝑐 → ( 𝑥𝑅 -s 𝐴 ) = ( 𝑐 -s 𝐴 ) )
306 305 oveq1d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) )
307 306 oveq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) )
308 id ⊢ ( 𝑥𝑅 = 𝑐 → 𝑥𝑅 = 𝑐 )
309 307 308 oveq12d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) )
310 309 eqeq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) ) )
311 oveq2 ⊢ ( 𝑦𝑅 = 𝑑 → ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) )
312 311 oveq2d ⊢ ( 𝑦𝑅 = 𝑑 → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
313 312 oveq1d ⊢ ( 𝑦𝑅 = 𝑑 → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) )
314 313 eqeq2d ⊢ ( 𝑦𝑅 = 𝑑 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) )
315 310 314 rspc2ev ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
316 200 315 mp3an3 ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
317 316 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
318 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
319 318 2rexbidv ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
320 214 319 elab ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
321 317 320 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } )
322 elun2 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) )
323 321 322 220 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
324 222 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( 𝑅 ‘ suc 𝑖 ) = ( ( 𝑅 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
325 323 324 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ suc 𝑖 ) )
326 304 325 227 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) )
327 326 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝑅 ‘ 𝑗 ) ) )
328 eliun ⊢ ( 𝑑 ∈ ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) )
329 funiunfv ⊢ ( Fun 𝑅 → ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) = ∪ ( 𝑅 “ ω ) )
330 237 329 ax-mp ⊢ ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) = ∪ ( 𝑅 “ ω )
331 330 eleq2i ⊢ ( 𝑑 ∈ ∪ 𝑖 ∈ ω ( 𝑅 ‘ 𝑖 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
332 328 331 bitr3i ⊢ ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
333 327 332 241 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) ) )
334 333 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝑅 “ ω ) )
335 302 303 334 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 <s ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) )
336 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s ∈ No )
337 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝐴 ∈ No )
338 127 337 subscld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
339 338 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
340 339 135 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
341 336 340 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
342 20 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 0s ∈ No )
343 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝐴 )
344 rightgt ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑐 )
345 344 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑐 )
346 342 337 127 343 345 slttrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝑐 )
347 346 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 0s <s 𝑐 )
348 6 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
349 elun2 ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
350 349 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
351 267 348 350 rspcdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 0s <s 𝑐 → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s ) )
352 346 351 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
353 352 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
354 129 341 128 347 353 sltmuldiv2wd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ↔ 𝑌 <s ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) )
355 335 354 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
356 336 138 136 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
357 128 131 135 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
358 357 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
359 356 358 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
360 355 359 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) )
361 137 138 336 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ) )
362 336 138 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
363 130 136 362 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
364 361 363 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
365 360 364 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s )
366 365 299 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
367 366 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
368 301 367 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) → 𝑒 <s 1s ) )
369 155 368 biimtrid ⊢ ( 𝜑 → ( 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 1s ) )
370 369 imp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → 𝑒 <s 1s )
371 velsn ⊢ ( 𝑓 ∈ { 1s } ↔ 𝑓 = 1s )
372 breq2 ⊢ ( 𝑓 = 1s → ( 𝑒 <s 𝑓 ↔ 𝑒 <s 1s ) )
373 371 372 sylbi ⊢ ( 𝑓 ∈ { 1s } → ( 𝑒 <s 𝑓 ↔ 𝑒 <s 1s ) )
374 370 373 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → ( 𝑓 ∈ { 1s } → 𝑒 <s 𝑓 ) )
375 374 3impia ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ∧ 𝑓 ∈ { 1s } ) → 𝑒 <s 𝑓 )
376 103 105 143 146 375 ssltd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) <<s { 1s } )
377 eqid ⊢ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
378 377 rnmpo ⊢ ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
379 mpoexga ⊢ ( ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∈ V ∧ ∪ ( 𝑅 “ ω ) ∈ V ) → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
380 85 97 379 syl2anc ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
381 rnexg ⊢ ( ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
382 380 381 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
383 378 382 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
384 eqid ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
385 384 rnmpo ⊢ ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
386 mpoexga ⊢ ( ( ( R ‘ 𝐴 ) ∈ V ∧ ∪ ( 𝐿 “ ω ) ∈ V ) → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
387 95 87 386 sylancr ⊢ ( 𝜑 → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
388 rnexg ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
389 387 388 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
390 385 389 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
391 383 390 unexd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ∈ V )
392 108 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑐 ∈ No )
393 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ No )
394 392 393 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
395 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝐴 ∈ No )
396 134 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑑 ∈ No )
397 395 396 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
398 394 397 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
399 392 396 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
400 398 399 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
401 400 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
402 401 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
403 402 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
404 127 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑐 ∈ No )
405 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ No )
406 404 405 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
407 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝐴 ∈ No )
408 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑑 ∈ No )
409 407 408 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
410 406 409 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
411 404 408 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
412 410 411 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
413 412 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
414 413 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
415 414 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
416 403 415 unssd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ⊆ No )
417 elun ⊢ ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∨ 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
418 vex ⊢ 𝑓 ∈ V
419 eqeq1 ⊢ ( 𝑏 = 𝑓 → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
420 419 2rexbidv ⊢ ( 𝑏 = 𝑓 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
421 418 420 elab ⊢ ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
422 419 2rexbidv ⊢ ( 𝑏 = 𝑓 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
423 418 422 elab ⊢ ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
424 421 423 orbi12i ⊢ ( ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∨ 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
425 417 424 bitri ⊢ ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ↔ ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
426 eliun ⊢ ( 𝑑 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) )
427 239 eleq2i ⊢ ( 𝑑 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
428 426 427 bitr3i ⊢ ( ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
429 1 2 3 4 5 6 precsexlem9 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( ∀ 𝑐 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑐 ) <s 1s ∧ ∀ 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑑 ) ) )
430 rsp ⊢ ( ∀ 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑑 ) → ( 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
431 429 430 simpl2im ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
432 431 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
433 428 432 biimtrrid ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
434 433 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 1s <s ( 𝐴 ·s 𝑑 ) )
435 56 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 𝑌 ∈ No )
436 57 oveq1d ⊢ ( 𝑌 ∈ No → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 0s +s ( 𝐴 ·s 𝑑 ) ) )
437 435 436 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 0s +s ( 𝐴 ·s 𝑑 ) ) )
438 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 𝐴 ∈ No )
439 438 134 mulscld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
440 439 167 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 0s +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
441 437 440 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
442 134 162 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 0s ·s 𝑑 ) = 0s )
443 441 442 oveq12d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( ( 𝐴 ·s 𝑑 ) -s 0s ) )
444 439 170 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 𝐴 ·s 𝑑 ) -s 0s ) = ( 𝐴 ·s 𝑑 ) )
445 443 444 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
446 434 445 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) )
447 446 ex ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) )
448 67 breq2d ⊢ ( 𝑐 = 0s → ( 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) )
449 448 imbi2d ⊢ ( 𝑐 = 0s → ( ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ↔ ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) ) )
450 447 449 syl5ibrcom ⊢ ( 𝜑 → ( 𝑐 = 0s → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
451 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s ∈ No )
452 249 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑐 ∈ No )
453 134 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑑 ∈ No )
454 452 453 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
455 439 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
456 451 454 455 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
457 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝐴 ∈ No )
458 452 457 453 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
459 458 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
460 456 459 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
461 191 simp2d ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
462 461 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
463 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
464 201 oveq1d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) )
465 464 oveq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) )
466 465 204 oveq12d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) )
467 466 eqeq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) ) )
468 467 314 rspc2ev ⊢ ( ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
469 200 468 mp3an3 ⊢ ( ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
470 469 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
471 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
472 471 2rexbidv ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
473 214 472 elab ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
474 470 473 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } )
475 elun2 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) )
476 elun2 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
477 474 475 476 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
478 1 2 3 precsexlem4 ⊢ ( 𝑖 ∈ ω → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
479 478 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
480 477 479 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) )
481 fveq2 ⊢ ( 𝑗 = suc 𝑖 → ( 𝐿 ‘ 𝑗 ) = ( 𝐿 ‘ suc 𝑖 ) )
482 481 eleq2d ⊢ ( 𝑗 = suc 𝑖 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) ) )
483 482 rspcev ⊢ ( ( suc 𝑖 ∈ ω ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
484 463 480 483 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
485 484 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ) )
486 eliun ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
487 funiunfv ⊢ ( Fun 𝐿 → ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) = ∪ ( 𝐿 “ ω ) )
488 43 487 ax-mp ⊢ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) = ∪ ( 𝐿 “ ω )
489 488 eleq2i ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
490 486 489 bitr3i ⊢ ( ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
491 485 332 490 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) ) )
492 491 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
493 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
494 462 492 493 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 )
495 252 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
496 495 453 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
497 451 496 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
498 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ No )
499 260 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 0s <s 𝑐 )
500 274 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
501 497 498 452 499 500 sltdivmulwd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 ↔ ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ) )
502 494 501 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
503 460 502 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
504 451 454 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
505 287 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
506 504 455 505 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ) )
507 505 455 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
508 451 454 507 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
509 506 508 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
510 503 509 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
511 510 exp32 ⊢ ( 𝜑 → ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
512 450 511 jaod ⊢ ( 𝜑 → ( ( 𝑐 = 0s ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
513 159 512 biimtrid ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
514 513 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
515 breq2 ⊢ ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → ( 1s <s 𝑓 ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
516 514 515 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
517 516 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
518 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 1s ∈ No )
519 518 411 409 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
520 404 407 408 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
521 520 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
522 519 521 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
523 461 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
524 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
525 305 oveq1d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) )
526 525 oveq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) )
527 526 308 oveq12d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) )
528 527 eqeq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) ) )
529 528 210 rspc2ev ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
530 200 529 mp3an3 ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
531 530 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
532 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
533 532 2rexbidv ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
534 214 533 elab ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
535 531 534 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } )
536 elun1 ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) )
537 535 536 476 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
538 478 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
539 537 538 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) )
540 524 539 483 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
541 540 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ) )
542 541 177 490 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) ) )
543 542 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
544 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
545 523 543 544 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 )
546 338 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
547 546 408 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
548 518 547 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
549 346 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 0s <s 𝑐 )
550 352 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
551 548 405 404 549 550 sltdivmulwd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 ↔ ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ) )
552 545 551 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
553 522 552 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
554 518 411 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
555 554 409 406 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ) )
556 518 411 410 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
557 555 556 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
558 553 557 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
559 558 515 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
560 559 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
561 517 560 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) → 1s <s 𝑓 ) )
562 425 561 biimtrid ⊢ ( 𝜑 → ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 1s <s 𝑓 ) )
563 velsn ⊢ ( 𝑒 ∈ { 1s } ↔ 𝑒 = 1s )
564 breq1 ⊢ ( 𝑒 = 1s → ( 𝑒 <s 𝑓 ↔ 1s <s 𝑓 ) )
565 564 imbi2d ⊢ ( 𝑒 = 1s → ( ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 𝑓 ) ↔ ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 1s <s 𝑓 ) ) )
566 563 565 sylbi ⊢ ( 𝑒 ∈ { 1s } → ( ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 𝑓 ) ↔ ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 1s <s 𝑓 ) ) )
567 562 566 syl5ibrcom ⊢ ( 𝜑 → ( 𝑒 ∈ { 1s } → ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 𝑓 ) ) )
568 567 3imp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ { 1s } ∧ 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → 𝑒 <s 𝑓 )
569 105 391 146 416 568 ssltd ⊢ ( 𝜑 → { 1s } <<s ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
570 81 376 569 cuteq1 ⊢ ( 𝜑 → ( ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) |s ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) = 1s )
571 19 570 eqtrd ⊢ ( 𝜑 → ( 𝐴 ·s 𝑌 ) = 1s )