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 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝐴 <s 𝑥𝑂 ↔ 𝐴 <s 𝑥𝑅 ) )
61 rightval ⊢ ( R ‘ 𝐴 ) = { 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥𝑂 }
62 60 61 elrab2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ↔ ( 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑥𝑅 ) )
63 62 simprbi ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑥𝑅 )
64 47 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 <s 𝑥𝑅 )
65 57 50 48 59 64 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
66 65 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
67 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅 ) )
68 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝑅 ·s 𝑦 ) )
69 68 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
70 69 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
71 67 70 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) ) )
72 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
74 elun2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
75 47 74 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
76 71 73 75 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
77 65 76 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
78 56 48 66 77 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∈ No )
79 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∈ No ) )
80 78 79 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
81 80 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
82 81 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ⊆ No )
83 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
84 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
85 ssrab2 ⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ⊆ ( L ‘ 𝐴 )
86 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } )
87 85 86 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
88 84 87 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
89 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
90 88 89 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
91 simpl3r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
92 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) )
93 91 92 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
94 90 93 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
95 83 94 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
96 breq2 ⊢ ( 𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿 ) )
97 96 elrab ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ↔ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∧ 0s <s 𝑥𝐿 ) )
98 97 simprbi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 0s <s 𝑥𝐿 )
99 86 98 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
100 99 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
101 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿 ) )
102 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝐿 ·s 𝑦 ) )
103 102 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
104 103 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
105 101 104 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) ) )
106 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
107 elun1 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
108 87 107 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
109 105 106 108 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
110 99 109 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
111 95 88 100 110 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ∈ No )
112 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ∈ No ) )
113 111 112 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
114 113 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
115 114 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ⊆ No )
116 82 115 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ⊆ No )
117 43 116 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) ⊆ No )
118 42 117 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝐿 ‘ suc 𝑗 ) ⊆ No )
119 1 2 3 precsexlem5 ⊢ ( 𝑗 ∈ ω → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
120 119 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
121 simp3r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
122 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
123 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } )
124 85 123 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
125 84 124 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
126 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
127 125 126 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
128 simpl3l ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
129 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) )
130 128 129 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
131 127 130 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
132 122 131 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
133 123 98 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
134 133 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
135 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
136 124 107 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
137 105 135 136 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
138 133 137 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
139 132 125 134 138 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∈ No )
140 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∈ No ) )
141 139 140 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
142 141 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 𝑎 ∈ No ) )
143 142 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ⊆ No )
144 44 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
145 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( R ‘ 𝐴 ) )
146 46 145 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
147 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
148 146 147 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
149 simpl3r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
150 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) )
151 149 150 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
152 148 151 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
153 144 152 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
154 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s ∈ No )
155 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝐴 )
156 145 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 <s 𝑥𝑅 )
157 154 147 146 155 156 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
158 157 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
159 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
160 145 74 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
161 71 159 160 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
162 157 161 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
163 153 146 158 162 divsclwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ∈ No )
164 eleq1 ⊢ ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 𝑎 ∈ No ↔ ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ∈ No ) )
165 163 164 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
166 165 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 𝑎 ∈ No ) )
167 166 abssdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ⊆ No )
168 143 167 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ⊆ No )
169 121 168 unssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ⊆ No )
170 120 169 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝑅 ‘ suc 𝑗 ) ⊆ No )
171 118 170 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) )
172 171 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ ω → ( ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
173 172 com12 ⊢ ( 𝑗 ∈ ω → ( 𝜑 → ( ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
174 173 a2d ⊢ ( 𝑗 ∈ ω → ( ( 𝜑 → ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) ) → ( 𝜑 → ( ( 𝐿 ‘ suc 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ suc 𝑗 ) ⊆ No ) ) ) )
175 12 18 24 30 40 174 finds ⊢ ( 𝐼 ∈ ω → ( 𝜑 → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) ) )
176 175 impcom ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ( 𝐿 ‘ 𝐼 ) ⊆ No ∧ ( 𝑅 ‘ 𝐼 ) ⊆ No ) )