Theorem precsexlem8 28600

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 6885	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	sseq1d 3939	. . . . 5 ⊢ (𝑖 = ∅ → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘∅) ⊆ No))
3		fveq2 6885	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	sseq1d 3939	. . . . 5 ⊢ (𝑖 = ∅ → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘∅) ⊆ No))
5	2, 4	anbi12d 644	. . . 4 ⊢ (𝑖 = ∅ → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No) ↔ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No)))
6	5	imbi2d 343	. . 3 ⊢ (𝑖 = ∅ → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No)) ↔ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No))))
7		fveq2 6885	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	sseq1d 3939	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝑗) ⊆ No))
9		fveq2 6885	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	sseq1d 3939	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝑗) ⊆ No))
11	8, 10	anbi12d 644	. . . 4 ⊢ (𝑖 = 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No) ↔ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)))
12	11	imbi2d 343	. . 3 ⊢ (𝑖 = 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No)) ↔ (𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No))))
13		fveq2 6885	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	sseq1d 3939	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘suc 𝑗) ⊆ No))
15		fveq2 6885	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	sseq1d 3939	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘suc 𝑗) ⊆ No))
17	14, 16	anbi12d 644	. . . 4 ⊢ (𝑖 = suc 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No) ↔ ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No)))
18	17	imbi2d 343	. . 3 ⊢ (𝑖 = suc 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No)) ↔ (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No))))
19		fveq2 6885	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
20	19	sseq1d 3939	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝐼) ⊆ No))
21		fveq2 6885	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
22	21	sseq1d 3939	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝐼) ⊆ No))
23	20, 22	anbi12d 644	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No) ↔ ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No)))
24	23	imbi2d 343	. . 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 28593	. . . . . 6 ⊢ (𝐿‘∅) = { 0s }
29		0no 28195	. . . . . . 7 ⊢ 0s ∈ No
30		snssi 4745	. . . . . . 7 ⊢ ( 0s ∈ No → { 0s } ⊆ No)
31	29, 30	ax-mp 5	. . . . . 6 ⊢ { 0s } ⊆ No
32	28, 31	eqsstri 3954	. . . . 5 ⊢ (𝐿‘∅) ⊆ No
33	25, 26, 27	precsexlem2 28594	. . . . . 6 ⊢ (𝑅‘∅) = ∅
34		0ss 4349	. . . . . 6 ⊢ ∅ ⊆ No
35	33, 34	eqsstri 3954	. . . . 5 ⊢ (𝑅‘∅) ⊆ No
36	32, 35	pm3.2i 476	. . . 4 ⊢ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No)
37	36	a1i 11	. . 3 ⊢ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No))
38	25, 26, 27	precsexlem4 28596	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
39	38	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
40		simp3l 1220	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝐿‘𝑗) ⊆ No)
41		1no 28196	. . . . . . . . . . . . . . . 16 ⊢ 1s ∈ No
42	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No)
43		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ (R‘𝐴))
44	43	rightnod 28268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ No)
45		precsexlem.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ No)
46	45	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → 𝐴 ∈ No)
47	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No)
48	44, 47	subscld 28449	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝑅 −s 𝐴) ∈ No)
49		simpl3l 1247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No)
50		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ (𝐿‘𝑗))
51	49, 50	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No)
52	48, 51	mulscld 28521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿) ∈ No)
53	42, 52	addscld 28366	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) ∈ No)
54	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s ∈ No)
55		precsexlem.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0s <s 𝐴)
56	55	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → 0s <s 𝐴)
57	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝐴)
58		rightgt 28240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 ∈ (R‘𝐴) → 𝐴 <s 𝑥𝑅)
59	43, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 <s 𝑥𝑅)
60	54, 47, 44, 57, 59	ltstrd 28120	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅)
61	60	gt0ne0sd 28205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
62		breq2 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
63		oveq1 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
64	63	eqeq1d 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
65	64	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
66	62, 65	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )))
67		precsexlem.6	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
68	67	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
69	68	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
70		elun2 4181	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 ∈ (R‘𝐴) → 𝑥𝑅 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
71	43, 70	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
72	66, 69, 71	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
73	60, 72	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
74	53, 44, 61, 73	divsclwd 28582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∈ No)
75		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∈ No))
76	74, 75	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → 𝑎 ∈ No))
77	76	rexlimdvva 3219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → 𝑎 ∈ No))
78	77	abssdv 3992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ⊆ No)
79	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No)
80		ssrab2 4005	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ⊆ (L‘𝐴)
81		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})
82	80, 81	sselid 3906	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ (L‘𝐴))
83	82	leftnod 28266	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ No)
84	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No)
85	83, 84	subscld 28449	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 −s 𝐴) ∈ No)
86		simpl3r 1248	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No)
87		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ (𝑅‘𝑗))
88	86, 87	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No)
89	85, 88	mulscld 28521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅) ∈ No)
90	79, 89	addscld 28366	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) ∈ No)
91		breq2 5106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
92	91	elrab 3644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ (L‘𝐴) ∧ 0s <s 𝑥𝐿))
93	92	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
94	81, 93	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿)
95	94	gt0ne0sd 28205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ≠ 0s )
96		breq2 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
97		oveq1 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
98	97	eqeq1d 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
99	98	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
100	96, 99	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )))
101	68	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
102		elun1 4180	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 ∈ (L‘𝐴) → 𝑥𝐿 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
103	82, 102	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
104	100, 101, 103	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
105	94, 104	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
106	90, 83, 95, 105	divsclwd 28582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ∈ No)
107		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ∈ No))
108	106, 107	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → 𝑎 ∈ No))
109	108	rexlimdvva 3219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → 𝑎 ∈ No))
110	109	abssdv 3992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ⊆ No)
111	78, 110	unssd 4190	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) ⊆ No)
112	40, 111	unssd 4190	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})) ⊆ No)
113	39, 112	eqsstrd 3942	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝐿‘suc 𝑗) ⊆ No)
114	25, 26, 27	precsexlem5 28597	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
115	114	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
116		simp3r 1221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝑅‘𝑗) ⊆ No)
117	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No)
118		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})
119	80, 118	sselid 3906	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ (L‘𝐴))
120	119	leftnod 28266	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ No)
121	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No)
122	120, 121	subscld 28449	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 −s 𝐴) ∈ No)
123		simpl3l 1247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No)
124		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ (𝐿‘𝑗))
125	123, 124	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No)
126	122, 125	mulscld 28521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿) ∈ No)
127	117, 126	addscld 28366	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) ∈ No)
128	118, 93	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿)
129	128	gt0ne0sd 28205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s )
130	68	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
131	119, 102	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
132	100, 130, 131	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
133	128, 132	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
134	127, 120, 129, 133	divsclwd 28582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∈ No)
135		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∈ No))
136	134, 135	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 𝑎 ∈ No))
137	136	rexlimdvva 3219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 𝑎 ∈ No))
138	137	abssdv 3992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ⊆ No)
139	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No)
140		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ (R‘𝐴))
141	140	rightnod 28268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ No)
142	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No)
143	141, 142	subscld 28449	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 −s 𝐴) ∈ No)
144		simpl3r 1248	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No)
145		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ (𝑅‘𝑗))
146	144, 145	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No)
147	143, 146	mulscld 28521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅) ∈ No)
148	139, 147	addscld 28366	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) ∈ No)
149	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s ∈ No)
150	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝐴)
151	140, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 <s 𝑥𝑅)
152	149, 142, 141, 150, 151	ltstrd 28120	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅)
153	152	gt0ne0sd 28205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s )
154	68	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
155	140, 70	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
156	66, 154, 155	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
157	152, 156	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
158	148, 141, 153, 157	divsclwd 28582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ∈ No)
159		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝑎 ∈ No ↔ (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ∈ No))
160	158, 159	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) ∧ (𝑥𝑅 ∈ (R‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 𝑎 ∈ No))
161	160	rexlimdvva 3219	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 𝑎 ∈ No))
162	161	abssdv 3992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ⊆ No)
163	138, 162	unssd 4190	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) ⊆ No)
164	116, 163	unssd 4190	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})) ⊆ No)
165	115, 164	eqsstrd 3942	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝑅‘suc 𝑗) ⊆ No)
166	113, 165	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No))
167	166	3exp 1137	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ω → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No))))
168	167	com12 33	. . . 4 ⊢ (𝑗 ∈ ω → (𝜑 → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No))))
169	168	a2d 30	. . 3 ⊢ (𝑗 ∈ ω → ((𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No)) → (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No))))
170	6, 12, 18, 24, 37, 169	finds 7908	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No)))
171	170	impcom 413	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450  ⦋csb 3846   ⊆ wss 3895   ∪ cun 4149  ∅c0 4278  {csn 4583  ⟨cop 4589   class class class wbr 5102   ↦ cmpt 5185   ∘ ccom 5654  suc csuc 6364  ‘cfv 6538  (class class class)co 7420  ωcom 7877  1^st c1st 7999  2^nd c2nd 8000  reccrdg 8417  Nocsur 27997   <s clts 27998   0_s c0s 28191   1_s c1s 28192  Lcleft 28211  Rcright 28212   +_s cadds 28345   −_s csubs 28406   ·_s cmuls 28492   /_su cdivs 28573

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-ot 4592  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-nadd 8675  df-no 28000  df-lts 28001  df-bday 28002  df-les 28102  df-slts 28144  df-cuts 28146  df-0s 28193  df-1s 28194  df-made 28213  df-old 28214  df-left 28216  df-right 28217  df-norec 28324  df-norec2 28335  df-adds 28346  df-negs 28407  df-subs 28408  df-muls 28493  df-divs 28574

This theorem is used by:  precsexlem9  28601  precsexlem10  28602