Metamath Proof Explorer

Theorem precsexlem8

Description: Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-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 ) )
Assertion precsexlem8 ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) )

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 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ ∅ ) )
8 7 sseq1d ⊢ ( 𝑖 = ∅ → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ↔ ( 𝐿 ‘ ∅ ) ⊆ No ) )
9 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ ∅ ) )
10 9 sseq1d ⊢ ( 𝑖 = ∅ → ( ( 𝑅 ‘ 𝑖 ) ⊆ No ↔ ( 𝑅 ‘ ∅ ) ⊆ No ) )
11 8 10 anbi12d ⊢ ( 𝑖 = ∅ → ( ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ↔ ( ( 𝐿 ‘ ∅ ) ⊆ No ∧ ( 𝑅 ‘ ∅ ) ⊆ No ) ) )
12 11 imbi2d ⊢ ( 𝑖 = ∅ → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ) ↔ ( 𝜑 → ( ( 𝐿 ‘ ∅ ) ⊆ No ∧ ( 𝑅 ‘ ∅ ) ⊆ No ) ) ) )
13 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) )
14 13 sseq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ↔ ( 𝐿 ‘ 𝑗 ) ⊆ No ) )
15 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑗 ) )
16 15 sseq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑅 ‘ 𝑖 ) ⊆ No ↔ ( 𝑅 ‘ 𝑗 ) ⊆ No ) )
17 14 16 anbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ↔ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) )
18 17 imbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ) ↔ ( 𝜑 → ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ) )
19 fveq2 ⊢ ( 𝑖 = suc 𝑗 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ suc 𝑗 ) )
20 19 sseq1d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ↔ ( 𝐿 ‘ suc 𝑗 ) ⊆ No ) )
21 fveq2 ⊢ ( 𝑖 = suc 𝑗 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ suc 𝑗 ) )
22 21 sseq1d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝑅 ‘ 𝑖 ) ⊆ No ↔ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) )
23 20 22 anbi12d ⊢ ( 𝑖 = suc 𝑗 → ( ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ↔ ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) )
24 23 imbi2d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ) ↔ ( 𝜑 → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
25 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝐼 ) )
26 25 sseq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ↔ ( 𝐿 ‘ 𝐼 ) ⊆ No ) )
27 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐼 ) )
28 27 sseq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑅 ‘ 𝑖 ) ⊆ No ↔ ( 𝑅 ‘ 𝐼 ) ⊆ No ) )
29 26 28 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ↔ ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) ) )
30 29 imbi2d ⊢ ( 𝑖 = 𝐼 → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑖 ) ⊆ No ∧ ( 𝑅 ‘ 𝑖 ) ⊆ No ) ) ↔ ( 𝜑 → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) ) ) )
31 1 2 3 precsexlem1 ⊢ ( 𝐿 ‘ ∅ ) = { 0s }
32 0sno ⊢ 0s ∈ No
33 snssi ⊢ ( 0s ∈ No → { 0s } ⊆ No )
34 32 33 ax-mp ⊢ { 0s } ⊆ No
35 31 34 eqsstri ⊢ ( 𝐿 ‘ ∅ ) ⊆ No
36 1 2 3 precsexlem2 ⊢ ( 𝑅 ‘ ∅ ) = ∅
37 0ss ⊢ ∅ ⊆ No
38 36 37 eqsstri ⊢ ( 𝑅 ‘ ∅ ) ⊆ No
39 35 38 pm3.2i ⊢ ( ( 𝐿 ‘ ∅ ) ⊆ No ∧ ( 𝑅 ‘ ∅ ) ⊆ No )
40 39 a1i ⊢ ( 𝜑 → ( ( 𝐿 ‘ ∅ ) ⊆ No ∧ ( 𝑅 ‘ ∅ ) ⊆ No ) )
41 1 2 3 precsexlem4 ⊢ ( 𝑗 ∈ ω → ( 𝐿 ‘ suc 𝑗 ) = ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
42 41 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝐿 ‘ suc 𝑗 ) = ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
43 simp3l ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
44 1sno ⊢ 1s ∈ No
45 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
46 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
47 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( R ‘ 𝐴 ) )
48 46 47 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
49 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → 𝐴 ∈ No )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
51 48 50 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
52 simpl3l ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
53 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) )
54 52 53 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
55 51 54 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
56 45 55 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
57 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s ∈ No )
58 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → 0s <s 𝐴 )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝐴 )
60 rightgt ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑥𝑅 )
61 47 60 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 <s 𝑥𝑅 )
62 57 50 48 59 61 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
63 62 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
64 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅 ) )
65 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝑅 ·s 𝑦 ) )
66 65 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
67 66 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
68 64 67 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) ) )
69 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
71 elun2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
72 47 71 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
73 68 70 72 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
74 62 73 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
75 56 48 63 74 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∈ No )
76 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∈ No ) )
77 75 76 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
78 77 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
79 78 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ⊆ No )
80 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
81 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
82 ssrab2 ⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ ( L ‘ 𝐴 )
83 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } )
84 82 83 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
85 81 84 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
86 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
87 85 86 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
88 simpl3r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
89 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) )
90 88 89 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
91 87 90 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
92 80 91 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
93 breq2 ⊢ ( 𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿 ) )
94 93 elrab ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ↔ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∧ 0s <s 𝑥𝐿 ) )
95 94 simprbi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 0s <s 𝑥𝐿 )
96 83 95 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
97 96 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
98 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿 ) )
99 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝐿 ·s 𝑦 ) )
100 99 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
101 100 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
102 98 101 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) ) )
103 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
104 elun1 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
105 84 104 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
106 102 103 105 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
107 96 106 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
108 92 85 97 107 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ∈ No )
109 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ∈ No ) )
110 108 109 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
111 110 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
112 111 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ⊆ No )
113 79 112 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ⊆ No )
114 43 113 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) ⊆ No )
115 42 114 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝐿 ‘ suc 𝑗 ) ⊆ No )
116 1 2 3 precsexlem5 ⊢ ( 𝑗 ∈ ω → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
117 116 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
118 simp3r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
119 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
120 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } )
121 82 120 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
122 81 121 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
123 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
124 122 123 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
125 simpl3l ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
126 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) )
127 125 126 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
128 124 127 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
129 119 128 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
130 120 95 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
131 130 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
132 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
133 121 104 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
134 102 132 133 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
135 130 134 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
136 129 122 131 135 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∈ No )
137 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∈ No ) )
138 136 137 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
139 138 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
140 139 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ⊆ No )
141 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
142 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( R ‘ 𝐴 ) )
143 46 142 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
144 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
145 143 144 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
146 simpl3r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
147 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) )
148 146 147 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
149 145 148 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
150 141 149 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
151 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s ∈ No )
152 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝐴 )
153 142 60 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 <s 𝑥𝑅 )
154 151 144 143 152 153 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
155 154 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
156 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
157 142 71 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
158 68 156 157 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
159 154 158 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
160 150 143 155 159 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ∈ No )
161 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ∈ No ) )
162 160 161 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
163 162 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
164 163 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ⊆ No )
165 140 164 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ⊆ No )
166 118 165 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⊆ No )
167 117 166 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ suc 𝑗 ) ⊆ No )
168 115 167 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) )
169 168 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ ω → ( ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
170 169 com12 ⊢ ( 𝑗 ∈ ω → ( 𝜑 → ( ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
171 170 a2d ⊢ ( 𝑗 ∈ ω → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝜑 → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
172 12 18 24 30 40 171 finds ⊢ ( 𝐼 ∈ ω → ( 𝜑 → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) ) )
173 172 impcom ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) )