Theorem precsexlem8 28123

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  {crab 3394  Vcvv 3436  ⦋csb 3851   ∪ cun 3901   ⊆ wss 3903  ∅c0 4284  {csn 4577  ⟨cop 4583   class class class wbr 5092   ↦ cmpt 5173   ∘ ccom 5623  suc csuc 6309  ‘cfv 6482  (class class class)co 7349  ωcom 7799  1^st c1st 7922  2^nd c2nd 7923  reccrdg 8331   No csur 27549   <s cslt 27550   0_s c0s 27737   1_s c1s 27738   L cleft 27757   R cright 27758   +_s cadds 27873   -_s csubs 27933   ·_s cmuls 28016   /_su cdivs 28097

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-ot 4586  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-nadd 8584  df-no 27552  df-slt 27553  df-bday 27554  df-sle 27655  df-sslt 27692  df-scut 27694  df-0s 27739  df-1s 27740  df-made 27759  df-old 27760  df-left 27762  df-right 27763  df-norec 27852  df-norec2 27863  df-adds 27874  df-negs 27934  df-subs 27935  df-muls 28017  df-divs 28098

This theorem is referenced by:  precsexlem9  28124  precsexlem10  28125