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 breq2 ⊢ ( 𝑥𝑂 = 𝑐 → ( 𝐴 <s 𝑥𝑂 ↔ 𝐴 <s 𝑐 ) )
345 rightval ⊢ ( R ‘ 𝐴 ) = { 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥𝑂 }
346 344 345 elrab2 ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) ↔ ( 𝑐 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑐 ) )
347 346 simprbi ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑐 )
348 347 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑐 )
349 342 337 127 343 348 slttrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝑐 )
350 349 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 0s <s 𝑐 )
351 6 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
352 elun2 ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
353 352 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → 𝑐 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
354 267 351 353 rspcdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 0s <s 𝑐 → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s ) )
355 349 354 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
356 355 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
357 129 341 128 350 356 sltmuldiv2wd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ↔ 𝑌 <s ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) )
358 335 357 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
359 336 138 136 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
360 128 131 135 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
361 360 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
362 359 361 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
363 358 362 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) )
364 137 138 336 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ) )
365 336 138 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
366 130 136 365 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) <s ( 1s +s ( 𝑐 ·s 𝑑 ) ) ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
367 364 366 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s ↔ ( 𝑐 ·s 𝑌 ) <s ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) ) )
368 363 367 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) <s 1s )
369 368 299 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
370 369 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑒 <s 1s ) )
371 301 370 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑒 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) → 𝑒 <s 1s ) )
372 155 371 biimtrid ⊢ ( 𝜑 → ( 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 1s ) )
373 372 imp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → 𝑒 <s 1s )
374 velsn ⊢ ( 𝑓 ∈ { 1s } ↔ 𝑓 = 1s )
375 breq2 ⊢ ( 𝑓 = 1s → ( 𝑒 <s 𝑓 ↔ 𝑒 <s 1s ) )
376 374 375 sylbi ⊢ ( 𝑓 ∈ { 1s } → ( 𝑒 <s 𝑓 ↔ 𝑒 <s 1s ) )
377 373 376 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → ( 𝑓 ∈ { 1s } → 𝑒 <s 𝑓 ) )
378 377 3impia ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ∧ 𝑓 ∈ { 1s } ) → 𝑒 <s 𝑓 )
379 103 105 143 146 378 ssltd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) <<s { 1s } )
380 eqid ⊢ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
381 380 rnmpo ⊢ ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
382 mpoexga ⊢ ( ( ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∈ V ∧ ∪ ( 𝑅 “ ω ) ∈ V ) → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
383 85 97 382 syl2anc ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
384 rnexg ⊢ ( ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
385 383 384 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) , 𝑑 ∈ ∪ ( 𝑅 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
386 381 385 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
387 eqid ⊢ ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
388 387 rnmpo ⊢ ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) = { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) }
389 mpoexga ⊢ ( ( ( R ‘ 𝐴 ) ∈ V ∧ ∪ ( 𝐿 “ ω ) ∈ V ) → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
390 95 87 389 sylancr ⊢ ( 𝜑 → ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
391 rnexg ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
392 390 391 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( R ‘ 𝐴 ) , 𝑑 ∈ ∪ ( 𝐿 “ ω ) ↦ ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ∈ V )
393 388 392 eqeltrrid ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∈ V )
394 386 393 unexd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ∈ V )
395 108 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑐 ∈ No )
396 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ No )
397 395 396 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
398 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝐴 ∈ No )
399 134 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑑 ∈ No )
400 398 399 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
401 397 400 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
402 395 399 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
403 401 402 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
404 403 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
405 404 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
406 405 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
407 127 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑐 ∈ No )
408 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ No )
409 407 408 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
410 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝐴 ∈ No )
411 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑑 ∈ No )
412 410 411 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
413 409 412 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
414 407 411 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
415 413 414 subscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∈ No )
416 415 121 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
417 416 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 𝑏 ∈ No ) )
418 417 abssdv ⊢ ( 𝜑 → { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ⊆ No )
419 406 418 unssd ⊢ ( 𝜑 → ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ⊆ No )
420 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 𝑑 ) ) } ) )
421 vex ⊢ 𝑓 ∈ V
422 eqeq1 ⊢ ( 𝑏 = 𝑓 → ( 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
423 422 2rexbidv ⊢ ( 𝑏 = 𝑓 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
424 421 423 elab ⊢ ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
425 422 2rexbidv ⊢ ( 𝑏 = 𝑓 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
426 421 425 elab ⊢ ( 𝑓 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ↔ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
427 424 426 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 𝑑 ) ) ) )
428 420 427 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 𝑑 ) ) ) )
429 eliun ⊢ ( 𝑑 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) )
430 239 eleq2i ⊢ ( 𝑑 ∈ ∪ 𝑗 ∈ ω ( 𝑅 ‘ 𝑗 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
431 429 430 bitr3i ⊢ ( ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) ↔ 𝑑 ∈ ∪ ( 𝑅 “ ω ) )
432 1 2 3 4 5 6 precsexlem9 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( ∀ 𝑐 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑐 ) <s 1s ∧ ∀ 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑑 ) ) )
433 rsp ⊢ ( ∀ 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑑 ) → ( 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
434 432 433 simpl2im ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
435 434 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
436 431 435 biimtrrid ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( 𝐴 ·s 𝑑 ) ) )
437 436 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 1s <s ( 𝐴 ·s 𝑑 ) )
438 56 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 𝑌 ∈ No )
439 57 oveq1d ⊢ ( 𝑌 ∈ No → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 0s +s ( 𝐴 ·s 𝑑 ) ) )
440 438 439 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 0s +s ( 𝐴 ·s 𝑑 ) ) )
441 4 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 𝐴 ∈ No )
442 441 134 mulscld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
443 442 167 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 0s +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
444 440 443 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
445 134 162 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( 0s ·s 𝑑 ) = 0s )
446 444 445 oveq12d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( ( 𝐴 ·s 𝑑 ) -s 0s ) )
447 442 170 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( 𝐴 ·s 𝑑 ) -s 0s ) = ( 𝐴 ·s 𝑑 ) )
448 446 447 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) = ( 𝐴 ·s 𝑑 ) )
449 437 448 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) )
450 449 ex ⊢ ( 𝜑 → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) )
451 67 breq2d ⊢ ( 𝑐 = 0s → ( 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) )
452 451 imbi2d ⊢ ( 𝑐 = 0s → ( ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ↔ ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 0s ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 0s ·s 𝑑 ) ) ) ) )
453 450 452 syl5ibrcom ⊢ ( 𝜑 → ( 𝑐 = 0s → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
454 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s ∈ No )
455 249 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑐 ∈ No )
456 134 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑑 ∈ No )
457 455 456 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑑 ) ∈ No )
458 442 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝐴 ·s 𝑑 ) ∈ No )
459 454 457 458 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
460 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝐴 ∈ No )
461 455 460 456 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
462 461 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
463 459 462 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
464 191 simp2d ⊢ ( 𝜑 → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
465 464 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
466 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
467 201 oveq1d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) )
468 467 oveq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) )
469 468 204 oveq12d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) )
470 469 eqeq2d ⊢ ( 𝑥𝐿 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑐 ) ) )
471 470 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 𝑥𝐿 ) )
472 200 471 mp3an3 ⊢ ( ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
473 472 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
474 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
475 474 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 𝑥𝐿 ) ) )
476 214 475 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 𝑥𝐿 ) )
477 473 476 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } )
478 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 𝑥𝐿 ) } ) )
479 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 𝑥𝐿 ) } ) ) )
480 477 478 479 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
481 1 2 3 precsexlem4 ⊢ ( 𝑖 ∈ ω → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
482 481 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
483 480 482 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) )
484 fveq2 ⊢ ( 𝑗 = suc 𝑖 → ( 𝐿 ‘ 𝑗 ) = ( 𝐿 ‘ suc 𝑖 ) )
485 484 eleq2d ⊢ ( 𝑗 = suc 𝑖 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) ) )
486 485 rspcev ⊢ ( ( suc 𝑖 ∈ ω ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
487 466 483 486 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
488 487 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝑅 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ) )
489 eliun ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
490 funiunfv ⊢ ( Fun 𝐿 → ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) = ∪ ( 𝐿 “ ω ) )
491 43 490 ax-mp ⊢ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) = ∪ ( 𝐿 “ ω )
492 491 eleq2i ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ 𝑗 ∈ ω ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
493 489 492 bitr3i ⊢ ( ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
494 488 332 493 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) ) )
495 494 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
496 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
497 465 495 496 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 )
498 252 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
499 498 456 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
500 454 499 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
501 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 𝑌 ∈ No )
502 260 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 0s <s 𝑐 )
503 274 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
504 500 501 455 502 503 sltdivmulwd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 ↔ ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ) )
505 497 504 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
506 463 505 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
507 454 457 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
508 287 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑐 ·s 𝑌 ) ∈ No )
509 507 458 508 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ) )
510 508 458 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ∈ No )
511 454 457 510 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
512 509 511 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
513 506 512 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
514 513 exp32 ⊢ ( 𝜑 → ( 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
515 453 514 jaod ⊢ ( 𝜑 → ( ( 𝑐 = 0s ∨ 𝑐 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
516 159 515 biimtrid ⊢ ( 𝜑 → ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑑 ∈ ∪ ( 𝑅 “ ω ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) ) )
517 516 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
518 breq2 ⊢ ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → ( 1s <s 𝑓 ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
519 517 518 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∧ 𝑑 ∈ ∪ ( 𝑅 “ ω ) ) ) → ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
520 519 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
521 144 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 1s ∈ No )
522 521 414 412 addsubsassd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
523 407 410 411 subsdird ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) = ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) )
524 523 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 ·s 𝑑 ) -s ( 𝐴 ·s 𝑑 ) ) ) )
525 522 524 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) )
526 464 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ∪ ( 𝐿 “ ω ) <<s { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
527 198 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → suc 𝑖 ∈ ω )
528 305 oveq1d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) )
529 528 oveq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) )
530 529 308 oveq12d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) )
531 530 eqeq2d ⊢ ( 𝑥𝑅 = 𝑐 → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑐 ) ) )
532 531 210 rspc2ev ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ∧ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
533 200 532 mp3an3 ⊢ ( ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
534 533 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
535 eqeq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
536 535 2rexbidv ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
537 214 536 elab ⊢ ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
538 534 537 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } )
539 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 𝑥𝐿 ) } ) )
540 538 539 479 3syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
541 481 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( 𝐿 ‘ suc 𝑖 ) = ( ( 𝐿 ‘ 𝑖 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑖 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
542 540 541 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ suc 𝑖 ) )
543 527 542 486 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) ∧ ( 𝑖 ∈ ω ∧ 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) ) ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) )
544 543 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( ∃ 𝑖 ∈ ω 𝑑 ∈ ( 𝐿 ‘ 𝑖 ) → ∃ 𝑗 ∈ ω ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ( 𝐿 ‘ 𝑗 ) ) )
545 544 177 493 3imtr3g ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( R ‘ 𝐴 ) ) → ( 𝑑 ∈ ∪ ( 𝐿 “ ω ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) ) )
546 545 impr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) ∈ ∪ ( 𝐿 “ ω ) )
547 196 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 𝑌 ∈ { ( ∪ ( 𝐿 “ ω ) |s ∪ ( 𝑅 “ ω ) ) } )
548 526 546 547 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 )
549 338 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑐 -s 𝐴 ) ∈ No )
550 549 411 mulscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ∈ No )
551 521 550 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) ∈ No )
552 349 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 0s <s 𝑐 )
553 355 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ∃ 𝑦 ∈ No ( 𝑐 ·s 𝑦 ) = 1s )
554 551 408 407 552 553 sltdivmulwd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) /su 𝑐 ) <s 𝑌 ↔ ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ) )
555 548 554 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( ( 𝑐 -s 𝐴 ) ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
556 525 555 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) )
557 521 414 addscld ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 1s +s ( 𝑐 ·s 𝑑 ) ) ∈ No )
558 557 412 409 sltsubaddd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ) )
559 521 414 413 sltaddsubd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) <s ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
560 558 559 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( ( ( 1s +s ( 𝑐 ·s 𝑑 ) ) -s ( 𝐴 ·s 𝑑 ) ) <s ( 𝑐 ·s 𝑌 ) ↔ 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) )
561 556 560 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → 1s <s ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) )
562 561 518 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( R ‘ 𝐴 ) ∧ 𝑑 ∈ ∪ ( 𝐿 “ ω ) ) ) → ( 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
563 562 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) → 1s <s 𝑓 ) )
564 520 563 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ∨ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑓 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) ) → 1s <s 𝑓 ) )
565 428 564 biimtrid ⊢ ( 𝜑 → ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 1s <s 𝑓 ) )
566 velsn ⊢ ( 𝑒 ∈ { 1s } ↔ 𝑒 = 1s )
567 breq1 ⊢ ( 𝑒 = 1s → ( 𝑒 <s 𝑓 ↔ 1s <s 𝑓 ) )
568 567 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 𝑓 ) ) )
569 566 568 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 𝑓 ) ) )
570 565 569 syl5ibrcom ⊢ ( 𝜑 → ( 𝑒 ∈ { 1s } → ( 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) → 𝑒 <s 𝑓 ) ) )
571 570 3imp ⊢ ( ( 𝜑 ∧ 𝑒 ∈ { 1s } ∧ 𝑓 ∈ ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) ) → 𝑒 <s 𝑓 )
572 105 394 146 419 571 ssltd ⊢ ( 𝜑 → { 1s } <<s ( { 𝑏 ∣ ∃ 𝑐 ∈ ( { 0s } ∪ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) ∃ 𝑑 ∈ ∪ ( 𝑅 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ∪ { 𝑏 ∣ ∃ 𝑐 ∈ ( R ‘ 𝐴 ) ∃ 𝑑 ∈ ∪ ( 𝐿 “ ω ) 𝑏 = ( ( ( 𝑐 ·s 𝑌 ) +s ( 𝐴 ·s 𝑑 ) ) -s ( 𝑐 ·s 𝑑 ) ) } ) )
573 81 379 572 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 )
574 19 573 eqtrd ⊢ ( 𝜑 → ( 𝐴 ·s 𝑌 ) = 1s )