Theorem precsexlem8 28155

Description: Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025.)

Hypotheses

Ref	Expression
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

Ref	Expression
precsexlem8	⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))

Distinct variable groups:   𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦,𝑦_𝐿,𝑦_𝑅   𝐹,𝑙,𝑝   𝐿,𝑎,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝑅,𝑎,𝑙,𝑟,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝜑,𝑎,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑟,𝑝,𝑙,𝑥_𝑂)   𝑅(𝑥,𝑦,𝑝,𝑥_𝑂)   𝐹(𝑥,𝑦,𝑟,𝑎,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅)   𝐼(𝑥,𝑦,𝑟,𝑝,𝑎,𝑙,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅)   𝐿(𝑥,𝑦,𝑟,𝑝,𝑥_𝑂)

Proof of Theorem precsexlem8

Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6875	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	sseq1d 3990	. . . . 5 ⊢ (𝑖 = ∅ → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘∅) ⊆ No ))
3		fveq2 6875	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	sseq1d 3990	. . . . 5 ⊢ (𝑖 = ∅ → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘∅) ⊆ No ))
5	2, 4	anbi12d 632	. . . 4 ⊢ (𝑖 = ∅ → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No )))
6	5	imbi2d 340	. . 3 ⊢ (𝑖 = ∅ → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No ))))
7		fveq2 6875	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	sseq1d 3990	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝑗) ⊆ No ))
9		fveq2 6875	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	sseq1d 3990	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝑗) ⊆ No ))
11	8, 10	anbi12d 632	. . . 4 ⊢ (𝑖 = 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )))
12	11	imbi2d 340	. . 3 ⊢ (𝑖 = 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))))
13		fveq2 6875	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	sseq1d 3990	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘suc 𝑗) ⊆ No ))
15		fveq2 6875	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	sseq1d 3990	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘suc 𝑗) ⊆ No ))
17	14, 16	anbi12d 632	. . . 4 ⊢ (𝑖 = suc 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No )))
18	17	imbi2d 340	. . 3 ⊢ (𝑖 = suc 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
19		fveq2 6875	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
20	19	sseq1d 3990	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝐼) ⊆ No ))
21		fveq2 6875	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
22	21	sseq1d 3990	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝐼) ⊆ No ))
23	20, 22	anbi12d 632	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No )))
24	23	imbi2d 340	. . 3 ⊢ (𝑖 = 𝐼 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))))
25		precsexlem.1	. . . . . . 7 ⊢ 𝐹 = 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 }, ∅⟩)
26		precsexlem.2	. . . . . . 7 ⊢ 𝐿 = (1st ∘ 𝐹)
27		precsexlem.3	. . . . . . 7 ⊢ 𝑅 = (2nd ∘ 𝐹)
28	25, 26, 27	precsexlem1 28148	. . . . . 6 ⊢ (𝐿‘∅) = { 0s }
29		0sno 27788	. . . . . . 7 ⊢ 0s ∈ No
30		snssi 4784	. . . . . . 7 ⊢ ( 0s ∈ No → { 0s } ⊆ No )
31	29, 30	ax-mp 5	. . . . . 6 ⊢ { 0s } ⊆ No
32	28, 31	eqsstri 4005	. . . . 5 ⊢ (𝐿‘∅) ⊆ No
33	25, 26, 27	precsexlem2 28149	. . . . . 6 ⊢ (𝑅‘∅) = ∅
34		0ss 4375	. . . . . 6 ⊢ ∅ ⊆ No
35	33, 34	eqsstri 4005	. . . . 5 ⊢ (𝑅‘∅) ⊆ No
36	32, 35	pm3.2i 470	. . . 4 ⊢ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No )
37	36	a1i 11	. . 3 ⊢ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No ))
38	25, 26, 27	precsexlem4 28151	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
39	38	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
40		simp3l 1202	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘𝑗) ⊆ No )
41		1sno 27789	. . . . . . . . . . . . . . . 16 ⊢ 1s ∈ No
42	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
43		rightssno 27837	. . . . . . . . . . . . . . . . . 18 ⊢ ( R ‘𝐴) ⊆ No
44		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ ( R ‘𝐴))
45	43, 44	sselid 3956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ No )
46		precsexlem.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ No )
47	46	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → 𝐴 ∈ No )
48	47	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
49	45, 48	subscld 28010	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
50		simpl3l 1229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No )
51		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ (𝐿‘𝑗))
52	50, 51	sseldd 3959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
53	49, 52	mulscld 28078	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
54	42, 53	addscld 27930	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
55	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s ∈ No )
56		precsexlem.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0s <s 𝐴)
57	56	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → 0s <s 𝐴)
58	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝐴)
59		breq2 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝐴 <s 𝑥𝑂 ↔ 𝐴 <s 𝑥𝑅))
60		rightval 27820	. . . . . . . . . . . . . . . . . . 19 ⊢ ( R ‘𝐴) = {𝑥𝑂 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥𝑂}
61	59, 60	elrab2 3674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) ↔ (𝑥𝑅 ∈ ( O ‘( bday ‘𝐴)) ∧ 𝐴 <s 𝑥𝑅))
62	61	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
63	44, 62	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 <s 𝑥𝑅)
64	55, 48, 45, 58, 63	slttrd 27721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅)
65	64	sgt0ne0d 27797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
66		breq2 5123	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
67		oveq1 7410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
68	67	eqeq1d 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
69	68	rexbidv 3164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
70	66, 69	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )))
71		precsexlem.6	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
72	71	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
73	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
74		elun2 4158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
75	44, 74	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
76	70, 73, 75	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
77	64, 76	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
78	54, 45, 65, 77	divsclwd 28138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∈ No )
79		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∈ No ))
80	78, 79	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → 𝑎 ∈ No ))
81	80	rexlimdvva 3198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → 𝑎 ∈ No ))
82	81	abssdv 4043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ⊆ No )
83	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
84		leftssno 27836	. . . . . . . . . . . . . . . . . 18 ⊢ ( L ‘𝐴) ⊆ No
85		ssrab2 4055	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ ( L ‘𝐴)
86		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})
87	85, 86	sselid 3956	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ ( L ‘𝐴))
88	84, 87	sselid 3956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ No )
89	47	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
90	88, 89	subscld 28010	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
91		simpl3r 1230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No )
92		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ (𝑅‘𝑗))
93	91, 92	sseldd 3959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
94	90, 93	mulscld 28078	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
95	83, 94	addscld 27930	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
96		breq2 5123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
97	96	elrab 3671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ ( L ‘𝐴) ∧ 0s <s 𝑥𝐿))
98	97	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
99	86, 98	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿)
100	99	sgt0ne0d 27797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ≠ 0s )
101		breq2 5123	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
102		oveq1 7410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
103	102	eqeq1d 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
104	103	rexbidv 3164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
105	101, 104	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )))
106	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
107		elun1 4157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
108	87, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
109	105, 106, 108	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
110	99, 109	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
111	95, 88, 100, 110	divsclwd 28138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ∈ No )
112		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ∈ No ))
113	111, 112	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → 𝑎 ∈ No ))
114	113	rexlimdvva 3198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → 𝑎 ∈ No ))
115	114	abssdv 4043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ⊆ No )
116	82, 115	unssd 4167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) ⊆ No )
117	40, 116	unssd 4167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})) ⊆ No )
118	39, 117	eqsstrd 3993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘suc 𝑗) ⊆ No )
119	25, 26, 27	precsexlem5 28152	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
120	119	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
121		simp3r 1203	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘𝑗) ⊆ No )
122	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
123		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})
124	85, 123	sselid 3956	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ ( L ‘𝐴))
125	84, 124	sselid 3956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ No )
126	47	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
127	125, 126	subscld 28010	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
128		simpl3l 1229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No )
129		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ (𝐿‘𝑗))
130	128, 129	sseldd 3959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
131	127, 130	mulscld 28078	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
132	122, 131	addscld 27930	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
133	123, 98	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿)
134	133	sgt0ne0d 27797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s )
135	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
136	124, 107	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
137	105, 135, 136	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
138	133, 137	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
139	132, 125, 134, 138	divsclwd 28138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∈ No )
140		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∈ No ))
141	139, 140	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 𝑎 ∈ No ))
142	141	rexlimdvva 3198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 𝑎 ∈ No ))
143	142	abssdv 4043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ⊆ No )
144	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
145		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ ( R ‘𝐴))
146	43, 145	sselid 3956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ No )
147	47	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
148	146, 147	subscld 28010	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
149		simpl3r 1230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No )
150		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ (𝑅‘𝑗))
151	149, 150	sseldd 3959	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
152	148, 151	mulscld 28078	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
153	144, 152	addscld 27930	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
154	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s ∈ No )
155	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝐴)
156	145, 62	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 <s 𝑥𝑅)
157	154, 147, 146, 155, 156	slttrd 27721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅)
158	157	sgt0ne0d 27797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s )
159	72	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
160	145, 74	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
161	70, 159, 160	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
162	157, 161	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
163	153, 146, 158, 162	divsclwd 28138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ∈ No )
164		eleq1 2822	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ∈ No ))
165	163, 164	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 𝑎 ∈ No ))
166	165	rexlimdvva 3198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 𝑎 ∈ No ))
167	166	abssdv 4043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ⊆ No )
168	143, 167	unssd 4167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) ⊆ No )
169	121, 168	unssd 4167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})) ⊆ No )
170	120, 169	eqsstrd 3993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘suc 𝑗) ⊆ No )
171	118, 170	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))
172	171	3exp 1119	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ω → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
173	172	com12 32	. . . 4 ⊢ (𝑗 ∈ ω → (𝜑 → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
174	173	a2d 29	. . 3 ⊢ (𝑗 ∈ ω → ((𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
175	6, 12, 18, 24, 37, 174	finds 7890	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No )))
176	175	impcom 407	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  {cab 2713  ∀wral 3051  ∃wrex 3060  {crab 3415  Vcvv 3459  ⦋csb 3874   ∪ cun 3924   ⊆ wss 3926  ∅c0 4308  {csn 4601  ⟨cop 4607   class class class wbr 5119   ↦ cmpt 5201   ∘ ccom 5658  suc csuc 6354  ‘cfv 6530  (class class class)co 7403  ωcom 7859  1^st c1st 7984  2^nd c2nd 7985  reccrdg 8421   No csur 27601   <s cslt 27602   bday cbday 27603   0_s c0s 27784   1_s c1s 27785   O cold 27799   L cleft 27801   R cright 27802   +_s cadds 27909   -_s csubs 27969   ·_s cmuls 28049   /_su cdivs 28130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-ot 4610  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-nadd 8676  df-no 27604  df-slt 27605  df-bday 27606  df-sle 27707  df-sslt 27743  df-scut 27745  df-0s 27786  df-1s 27787  df-made 27803  df-old 27804  df-left 27806  df-right 27807  df-norec 27888  df-norec2 27899  df-adds 27910  df-negs 27970  df-subs 27971  df-muls 28050  df-divs 28131

This theorem is referenced by:  precsexlem9  28156  precsexlem10  28157