Theorem precsexlem11 28230

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (Contributed by Scott Fenton, 15-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 ))
precsexlem.7	⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))

Assertion

Ref	Expression
precsexlem11	⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )

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

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

Proof of Theorem precsexlem11

Dummy variables 𝑖 𝑗 𝑏 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lltr 27875	. . . 4 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
2		precsexlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ No )
3		precsexlem.5	. . . . . . 7 ⊢ (𝜑 → 0s <s 𝐴)
4	2, 3	0elleft 27924	. . . . . 6 ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
5	4	snssd 4767	. . . . 5 ⊢ (𝜑 → { 0s } ⊆ ( L ‘𝐴))
6		ssrab2 4034	. . . . . 6 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ ( L ‘𝐴)
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ ( L ‘𝐴))
8	5, 7	unssd 4146	. . . 4 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ ( L ‘𝐴))
9		ssslts1 27786	. . . 4 ⊢ ((( L ‘𝐴) <<s ( R ‘𝐴) ∧ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ ( L ‘𝐴)) → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴))
10	1, 8, 9	sylancr 588	. . 3 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴))
11		precsexlem.1	. . . 4 ⊢ 𝐹 = 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 }, ∅⟩)
12		precsexlem.2	. . . 4 ⊢ 𝐿 = (1st ∘ 𝐹)
13		precsexlem.3	. . . 4 ⊢ 𝑅 = (2nd ∘ 𝐹)
14		precsexlem.6	. . . 4 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
15	11, 12, 13, 2, 3, 14	precsexlem10 28229	. . 3 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
16	2, 3	cutpos 27946	. . 3 ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴)))
17		precsexlem.7	. . . 4 ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))
18	17	a1i 11	. . 3 ⊢ (𝜑 → 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)))
19	10, 15, 16, 18	mulsunif 28163	. 2 ⊢ (𝜑 → (𝐴 ·s 𝑌) = (({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) |s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})))
20		0no 27822	. . . . . . . . 9 ⊢ 0s ∈ No
21	20	elexi 3465	. . . . . . . 8 ⊢ 0s ∈ V
22	21	snid 4621	. . . . . . 7 ⊢ 0s ∈ { 0s }
23		elun1 4136	. . . . . . 7 ⊢ ( 0s ∈ { 0s } → 0s ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
24	22, 23	ax-mp 5	. . . . . 6 ⊢ 0s ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})
25		peano1 7843	. . . . . . . . 9 ⊢ ∅ ∈ ω
26	11, 12, 13	precsexlem1 28220	. . . . . . . . . 10 ⊢ (𝐿‘∅) = { 0s }
27	22, 26	eleqtrri 2836	. . . . . . . . 9 ⊢ 0s ∈ (𝐿‘∅)
28		fveq2 6844	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝐿‘𝑏) = (𝐿‘∅))
29	28	eleq2d 2823	. . . . . . . . . 10 ⊢ (𝑏 = ∅ → ( 0s ∈ (𝐿‘𝑏) ↔ 0s ∈ (𝐿‘∅)))
30	29	rspcev 3578	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 0s ∈ (𝐿‘∅)) → ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
31	25, 27, 30	mp2an 693	. . . . . . . 8 ⊢ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏)
32		eliun 4952	. . . . . . . 8 ⊢ ( 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏) ↔ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
33	31, 32	mpbir 231	. . . . . . 7 ⊢ 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏)
34		fo1st 7965	. . . . . . . . . . 11 ⊢ 1st :V–onto→V
35		fofun 6757	. . . . . . . . . . 11 ⊢ (1st :V–onto→V → Fun 1st )
36	34, 35	ax-mp 5	. . . . . . . . . 10 ⊢ Fun 1st
37		rdgfun 8359	. . . . . . . . . . 11 ⊢ Fun 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 }, ∅⟩)
38	11	funeqi 6523	. . . . . . . . . . 11 ⊢ (Fun 𝐹 ↔ Fun 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 }, ∅⟩))
39	37, 38	mpbir 231	. . . . . . . . . 10 ⊢ Fun 𝐹
40		funco 6542	. . . . . . . . . 10 ⊢ ((Fun 1st ∧ Fun 𝐹) → Fun (1st ∘ 𝐹))
41	36, 39, 40	mp2an 693	. . . . . . . . 9 ⊢ Fun (1st ∘ 𝐹)
42	12	funeqi 6523	. . . . . . . . 9 ⊢ (Fun 𝐿 ↔ Fun (1st ∘ 𝐹))
43	41, 42	mpbir 231	. . . . . . . 8 ⊢ Fun 𝐿
44		funiunfv 7206	. . . . . . . 8 ⊢ (Fun 𝐿 → ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω))
45	43, 44	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω)
46	33, 45	eleqtri 2835	. . . . . 6 ⊢ 0s ∈ ∪ (𝐿 “ ω)
47		addsrid 27977	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
48	20, 47	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s +s 0s ) = 0s
49		muls01 28125	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s ·s 0s ) = 0s )
50	20, 49	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s ·s 0s ) = 0s
51	48, 50	oveq12i 7382	. . . . . . . 8 ⊢ (( 0s +s 0s ) -s ( 0s ·s 0s )) = ( 0s -s 0s )
52		subsid 28082	. . . . . . . . 9 ⊢ ( 0s ∈ No → ( 0s -s 0s ) = 0s )
53	20, 52	ax-mp 5	. . . . . . . 8 ⊢ ( 0s -s 0s ) = 0s
54	51, 53	eqtr2i 2761	. . . . . . 7 ⊢ 0s = (( 0s +s 0s ) -s ( 0s ·s 0s ))
55	15	cutscld 27796	. . . . . . . . . . 11 ⊢ (𝜑 → (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No )
56	17, 55	eqeltrid 2841	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ No )
57		muls02 28154	. . . . . . . . . 10 ⊢ (𝑌 ∈ No → ( 0s ·s 𝑌) = 0s )
58	56, 57	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ( 0s ·s 𝑌) = 0s )
59		muls01 28125	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
60	2, 59	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
61	58, 60	oveq12d 7388	. . . . . . . 8 ⊢ (𝜑 → (( 0s ·s 𝑌) +s (𝐴 ·s 0s )) = ( 0s +s 0s ))
62	61	oveq1d 7385	. . . . . . 7 ⊢ (𝜑 → ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )) = (( 0s +s 0s ) -s ( 0s ·s 0s )))
63	54, 62	eqtr4id 2791	. . . . . 6 ⊢ (𝜑 → 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )))
64		oveq1 7377	. . . . . . . . . 10 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑌) = ( 0s ·s 𝑌))
65	64	oveq1d 7385	. . . . . . . . 9 ⊢ (𝑐 = 0s → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)))
66		oveq1 7377	. . . . . . . . 9 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑑) = ( 0s ·s 𝑑))
67	65, 66	oveq12d 7388	. . . . . . . 8 ⊢ (𝑐 = 0s → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))
68	67	eqeq2d 2748	. . . . . . 7 ⊢ (𝑐 = 0s → ( 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
69		oveq2 7378	. . . . . . . . . 10 ⊢ (𝑑 = 0s → (𝐴 ·s 𝑑) = (𝐴 ·s 0s ))
70	69	oveq2d 7386	. . . . . . . . 9 ⊢ (𝑑 = 0s → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 0s )))
71		oveq2 7378	. . . . . . . . 9 ⊢ (𝑑 = 0s → ( 0s ·s 𝑑) = ( 0s ·s 0s ))
72	70, 71	oveq12d 7388	. . . . . . . 8 ⊢ (𝑑 = 0s → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )))
73	72	eqeq2d 2748	. . . . . . 7 ⊢ (𝑑 = 0s → ( 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s ))))
74	68, 73	rspc2ev 3591	. . . . . 6 ⊢ (( 0s ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 0s ∈ ∪ (𝐿 “ ω) ∧ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s ))) → ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
75	24, 46, 63, 74	mp3an12i 1468	. . . . 5 ⊢ (𝜑 → ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
76		eqeq1 2741	. . . . . . 7 ⊢ (𝑏 = 0s → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
77	76	2rexbidv 3203	. . . . . 6 ⊢ (𝑏 = 0s → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
78	21, 77	elab 3636	. . . . 5 ⊢ ( 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
79	75, 78	sylibr 234	. . . 4 ⊢ (𝜑 → 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})
80		elun1 4136	. . . 4 ⊢ ( 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} → 0s ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
81	79, 80	syl 17	. . 3 ⊢ (𝜑 → 0s ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
82		eqid 2737	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
83	82	rnmpo 7503	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
84		sltsex1 27776	. . . . . . . . 9 ⊢ (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴) → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
85	10, 84	syl 17	. . . . . . . 8 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
86		sltsex1 27776	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ∈ V)
87	15, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝐿 “ ω) ∈ V)
88		mpoexga 8033	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
89	85, 87, 88	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
90		rnexg 7856	. . . . . . 7 ⊢ ((𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
91	89, 90	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
92	83, 91	eqeltrrid 2842	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
93		eqid 2737	. . . . . . 7 ⊢ (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
94	93	rnmpo 7503	. . . . . 6 ⊢ ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
95		fvex 6857	. . . . . . . 8 ⊢ ( R ‘𝐴) ∈ V
96		sltsex2 27777	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ∈ V)
97	15, 96	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝑅 “ ω) ∈ V)
98		mpoexga 8033	. . . . . . . 8 ⊢ ((( R ‘𝐴) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
99	95, 97, 98	sylancr 588	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
100		rnexg 7856	. . . . . . 7 ⊢ ((𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
101	99, 100	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
102	94, 101	eqeltrrid 2842	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
103	92, 102	unexd 7711	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∈ V)
104		snex 5387	. . . . 5 ⊢ { 1s } ∈ V
105	104	a1i 11	. . . 4 ⊢ (𝜑 → { 1s } ∈ V)
106		sltsss1 27778	. . . . . . . . . . . . . 14 ⊢ (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴) → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ No )
107	10, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ No )
108	107	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})) → 𝑐 ∈ No )
109	108	adantrr 718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
110	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No )
111	109, 110	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
112	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No )
113		sltsss1 27778	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ⊆ No )
114	15, 113	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝐿 “ ω) ⊆ No )
115	114	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝑑 ∈ No )
116	115	adantrl 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
117	112, 116	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
118	111, 117	addscld 27993	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
119	109, 116	mulscld 28148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
120	118, 119	subscld 28076	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
121		eleq1 2825	. . . . . . . 8 ⊢ (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → (𝑏 ∈ No ↔ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No ))
122	120, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
123	122	rexlimdvva 3195	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
124	123	abssdv 4021	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
125		rightssno 27887	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝐴) ⊆ No
126	125	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( R ‘𝐴) ⊆ No )
127	126	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑐 ∈ No )
128	127	adantrr 718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
129	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
130	128, 129	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
131	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
132		sltsss2 27779	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ⊆ No )
133	15, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝑅 “ ω) ⊆ No )
134	133	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑑 ∈ No )
135	134	adantrl 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
136	131, 135	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
137	130, 136	addscld 27993	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
138	128, 135	mulscld 28148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
139	137, 138	subscld 28076	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
140	139, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
141	140	rexlimdvva 3195	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
142	141	abssdv 4021	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
143	124, 142	unssd 4146	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ⊆ No )
144		1no 27823	. . . . 5 ⊢ 1s ∈ No
145		snssi 4766	. . . . 5 ⊢ ( 1s ∈ No → { 1s } ⊆ No )
146	144, 145	mp1i 13	. . . 4 ⊢ (𝜑 → { 1s } ⊆ No )
147		elun 4107	. . . . . . . . 9 ⊢ (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∨ 𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
148		vex 3446	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
149		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
150	149	2rexbidv 3203	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
151	148, 150	elab 3636	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
152	149	2rexbidv 3203	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
153	148, 152	elab 3636	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
154	151, 153	orbi12i 915	. . . . . . . . 9 ⊢ ((𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∨ 𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
155	147, 154	bitri 275	. . . . . . . 8 ⊢ (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
156		elun 4107	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 ∈ { 0s } ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
157		velsn 4598	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ { 0s } ↔ 𝑐 = 0s )
158	157	orbi1i 914	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ { 0s } ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
159	156, 158	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
160	58	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s ·s 𝑌) = 0s )
161	160	oveq1d 7385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
162		muls02 28154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ No → ( 0s ·s 𝑑) = 0s )
163	115, 162	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s ·s 𝑑) = 0s )
164	161, 163	oveq12d 7388	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (( 0s +s (𝐴 ·s 𝑑)) -s 0s ))
165	2	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝐴 ∈ No )
166	165, 115	mulscld 28148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (𝐴 ·s 𝑑) ∈ No )
167		addslid 27981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ·s 𝑑) ∈ No → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
168	166, 167	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
169	168	oveq1d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s +s (𝐴 ·s 𝑑)) -s 0s ) = ((𝐴 ·s 𝑑) -s 0s ))
170		subsid1 28081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ·s 𝑑) ∈ No → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
171	166, 170	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
172	164, 169, 171	3eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
173		eliun 4952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖))
174		funiunfv 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐿 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω))
175	43, 174	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω)
176	175	eleq2i 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
177	173, 176	bitr3i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
178	11, 12, 13, 2, 3, 14	precsexlem9 28228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)))
179	178	simpld 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s )
180		rsp 3226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
181	179, 180	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
182	181	rexlimdva 3139	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
183	177, 182	biimtrrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝐿 “ ω) → (𝐴 ·s 𝑑) <s 1s ))
184	183	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (𝐴 ·s 𝑑) <s 1s )
185	172, 184	eqbrtrd 5122	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) <s 1s )
186	185	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝐿 “ ω) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) <s 1s ))
187	67	breq1d 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 0s → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) <s 1s ))
188	187	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 0s → ((𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ) ↔ (𝑑 ∈ ∪ (𝐿 “ ω) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) <s 1s )))
189	186, 188	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 = 0s → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )))
190		cutcuts 27794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
191	15, 190	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
192	191	simp3d 1145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
193	192	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
194		ovex 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ V
195	194	snid 4621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
196	17, 195	eqeltri 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
197	196	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
198		peano2 7844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
199	198	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
200		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)
201		oveq1 7377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥𝐿 = 𝑐 → (𝑥𝐿 -s 𝐴) = (𝑐 -s 𝐴))
202	201	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑦𝐿))
203	202	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)))
204		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → 𝑥𝐿 = 𝑐)
205	203, 204	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
206	205	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
207		oveq2 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦𝐿 = 𝑑 → ((𝑐 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑑))
208	207	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦𝐿 = 𝑑 → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
209	208	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦𝐿 = 𝑑 → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
210	209	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦𝐿 = 𝑑 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)))
211	206, 210	rspc2ev 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝐿‘𝑖) ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
212	200, 211	mp3an3 1453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
213	212	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
214		ovex 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ V
215		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
216	215	2rexbidv 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
217	214, 216	elab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
218	213, 217	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)})
219		elun1 4136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))
220		elun2 4137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
221	218, 219, 220	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
222	11, 12, 13	precsexlem5 28224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
223	222	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
224	221, 223	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
225		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = suc 𝑖 → (𝑅‘𝑗) = (𝑅‘suc 𝑖))
226	225	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)))
227	226	rspcev 3578	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
228	199, 224, 227	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
229	228	rexlimdvaa 3140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
230		eliun 4952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
231		fo2nd 7966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2nd :V–onto→V
232		fofun 6757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd :V–onto→V → Fun 2nd )
233	231, 232	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Fun 2nd
234		funco 6542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd ∘ 𝐹))
235	233, 39, 234	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Fun (2nd ∘ 𝐹)
236	13	funeqi 6523	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun 𝑅 ↔ Fun (2nd ∘ 𝐹))
237	235, 236	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Fun 𝑅
238		funiunfv 7206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑅 → ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω))
239	237, 238	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω)
240	239	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
241	230, 240	bitr3i 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
242	229, 177, 241	3imtr3g 295	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω)))
243	242	impr 454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
244	193, 197, 243	sltssepcd 27785	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 <s (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
245	56	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No )
246	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s ∈ No )
247		leftssno 27886	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( L ‘𝐴) ⊆ No
248	6, 247	sstri 3945	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ No
249	248	sseli 3931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑐 ∈ No )
250	249	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑐 ∈ No )
251	2	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 ∈ No )
252	250, 251	subscld 28076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 -s 𝐴) ∈ No )
253	252	adantrr 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 -s 𝐴) ∈ No )
254	115	adantrl 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
255	253, 254	mulscld 28148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
256	246, 255	addscld 27993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
257	249	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
258		breq2 5104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑐 → ( 0s <s 𝑥 ↔ 0s <s 𝑐))
259	258	elrab 3648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑐 ∈ ( L ‘𝐴) ∧ 0s <s 𝑐))
260	259	simprbi 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑐)
261	260	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
262	260	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑐)
263		breq2 5104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥𝑂 = 𝑐 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑐))
264		oveq1 7377	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑂 = 𝑐 → (𝑥𝑂 ·s 𝑦) = (𝑐 ·s 𝑦))
265	264	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑂 = 𝑐 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑐 ·s 𝑦) = 1s ))
266	265	rexbidv 3162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥𝑂 = 𝑐 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
267	263, 266	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥𝑂 = 𝑐 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )))
268	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
269		ssun1 4132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ( L ‘𝐴) ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
270	6, 269	sstri 3945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
271	270	sseli 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
272	271	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
273	267, 268, 272	rspcdva 3579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
274	262, 273	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
275	274	adantrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
276	245, 256, 257, 261, 275	ltmuldivs2wd 28215	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ↔ 𝑌 <s (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)))
277	244, 276	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
278	257, 254	mulscld 28148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
279	166	adantrl 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
280	246, 278, 279	addsubsassd 28094	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
281	2	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No )
282	257, 281, 254	subsdird 28172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
283	282	oveq2d 7386	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
284	280, 283	eqtr4d 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
285	277, 284	breqtrrd 5128	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)))
286	56	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑌 ∈ No )
287	250, 286	mulscld 28148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 ·s 𝑌) ∈ No )
288	287	adantrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
289	288, 279	addscld 27993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
290	289, 278, 246	ltsubaddsd 28102	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
291	246, 278	addscld 27993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
292	288, 279, 291	ltaddsubsd 28104	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑)) ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
293	290, 292	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
294	285, 293	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )
295	294	exp32 420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )))
296	189, 295	jaod 860	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )))
297	159, 296	biimtrid 242	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )))
298	297	imp32 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )
299		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → (𝑒 <s 1s ↔ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ))
300	298, 299	syl5ibrcom 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
301	300	rexlimdvva 3195	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
302	192	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
303	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
304	198	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
305		oveq1 7377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝑅 = 𝑐 → (𝑥𝑅 -s 𝐴) = (𝑐 -s 𝐴))
306	305	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑦𝑅))
307	306	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)))
308		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → 𝑥𝑅 = 𝑐)
309	307, 308	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
310	309	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
311		oveq2 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦𝑅 = 𝑑 → ((𝑐 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑑))
312	311	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦𝑅 = 𝑑 → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
313	312	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦𝑅 = 𝑑 → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
314	313	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦𝑅 = 𝑑 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)))
315	310, 314	rspc2ev 3591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝑅‘𝑖) ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
316	200, 315	mp3an3 1453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
317	316	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
318		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
319	318	2rexbidv 3203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
320	214, 319	elab 3636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
321	317, 320	sylibr 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})
322		elun2 4137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))
323	321, 322, 220	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
324	222	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
325	323, 324	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
326	304, 325, 227	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
327	326	rexlimdvaa 3140	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
328		eliun 4952	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝑅‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖))
329		funiunfv 7206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑅 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω))
330	237, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω)
331	330	eleq2i 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝑅‘𝑖) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
332	328, 331	bitr3i 277	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
333	327, 332, 241	3imtr3g 295	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (𝑑 ∈ ∪ (𝑅 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω)))
334	333	impr 454	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
335	302, 303, 334	sltssepcd 27785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 <s (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
336	144	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s ∈ No )
337	2	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝐴 ∈ No )
338	127, 337	subscld 28076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (𝑐 -s 𝐴) ∈ No )
339	338	adantrr 718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 -s 𝐴) ∈ No )
340	339, 135	mulscld 28148	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
341	336, 340	addscld 27993	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
342	20	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s ∈ No )
343	3	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
344		rightgt 27867	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ( R ‘𝐴) → 𝐴 <s 𝑐)
345	344	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑐)
346	342, 337, 127, 343, 345	ltstrd 27748	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s <s 𝑐)
347	346	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
348	14	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
349		elun2 4137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ( R ‘𝐴) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
350	349	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
351	267, 348, 350	rspcdva 3579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
352	346, 351	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
353	352	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
354	129, 341, 128, 347, 353	ltmuldivs2wd 28215	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ↔ 𝑌 <s (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)))
355	335, 354	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
356	336, 138, 136	addsubsassd 28094	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
357	128, 131, 135	subsdird 28172	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
358	357	oveq2d 7386	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
359	356, 358	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
360	355, 359	breqtrrd 5128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)))
361	137, 138, 336	ltsubaddsd 28102	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
362	336, 138	addscld 27993	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
363	130, 136, 362	ltaddsubsd 28104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑)) ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
364	361, 363	bitrd 279	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
365	360, 364	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )
366	365, 299	syl5ibrcom 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
367	366	rexlimdvva 3195	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
368	301, 367	jaod 860	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) → 𝑒 <s 1s ))
369	155, 368	biimtrid 242	. . . . . . 7 ⊢ (𝜑 → (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 1s ))
370	369	imp 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → 𝑒 <s 1s )
371		velsn 4598	. . . . . . 7 ⊢ (𝑓 ∈ { 1s } ↔ 𝑓 = 1s )
372		breq2 5104	. . . . . . 7 ⊢ (𝑓 = 1s → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
373	371, 372	sylbi 217	. . . . . 6 ⊢ (𝑓 ∈ { 1s } → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
374	370, 373	syl5ibrcom 247	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → (𝑓 ∈ { 1s } → 𝑒 <s 𝑓))
375	374	3impia 1118	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∧ 𝑓 ∈ { 1s }) → 𝑒 <s 𝑓)
376	103, 105, 143, 146, 375	sltsd 27781	. . 3 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) <<s { 1s })
377		eqid 2737	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
378	377	rnmpo 7503	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
379		mpoexga 8033	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
380	85, 97, 379	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
381		rnexg 7856	. . . . . . 7 ⊢ ((𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
382	380, 381	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
383	378, 382	eqeltrrid 2842	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
384		eqid 2737	. . . . . . 7 ⊢ (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
385	384	rnmpo 7503	. . . . . 6 ⊢ ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
386		mpoexga 8033	. . . . . . . 8 ⊢ ((( R ‘𝐴) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
387	95, 87, 386	sylancr 588	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
388		rnexg 7856	. . . . . . 7 ⊢ ((𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
389	387, 388	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
390	385, 389	eqeltrrid 2842	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
391	383, 390	unexd 7711	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∈ V)
392	108	adantrr 718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
393	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
394	392, 393	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
395	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
396	134	adantrl 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
397	395, 396	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
398	394, 397	addscld 27993	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
399	392, 396	mulscld 28148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
400	398, 399	subscld 28076	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
401	400, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
402	401	rexlimdvva 3195	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
403	402	abssdv 4021	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
404	127	adantrr 718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
405	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No )
406	404, 405	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
407	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No )
408	115	adantrl 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
409	407, 408	mulscld 28148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
410	406, 409	addscld 27993	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
411	404, 408	mulscld 28148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
412	410, 411	subscld 28076	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
413	412, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
414	413	rexlimdvva 3195	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
415	414	abssdv 4021	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
416	403, 415	unssd 4146	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ⊆ No )
417		elun 4107	. . . . . . . 8 ⊢ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∨ 𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
418		vex 3446	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
419		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑓 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
420	419	2rexbidv 3203	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
421	418, 420	elab 3636	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
422	419	2rexbidv 3203	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
423	418, 422	elab 3636	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
424	421, 423	orbi12i 915	. . . . . . . 8 ⊢ ((𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∨ 𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
425	417, 424	bitri 275	. . . . . . 7 ⊢ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
426		eliun 4952	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗))
427	239	eleq2i 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
428	426, 427	bitr3i 277	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
429	11, 12, 13, 2, 3, 14	precsexlem9 28228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (∀𝑐 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑐) <s 1s ∧ ∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑)))
430		rsp 3226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
431	429, 430	simpl2im 503	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
432	431	rexlimdva 3139	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
433	428, 432	biimtrrid 243	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (𝐴 ·s 𝑑)))
434	433	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s (𝐴 ·s 𝑑))
435	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑌 ∈ No )
436	57	oveq1d 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 ∈ No → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
437	435, 436	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
438	2	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝐴 ∈ No )
439	438, 134	mulscld 28148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (𝐴 ·s 𝑑) ∈ No )
440	439, 167	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
441	437, 440	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
442	134, 162	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s ·s 𝑑) = 0s )
443	441, 442	oveq12d 7388	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = ((𝐴 ·s 𝑑) -s 0s ))
444	439, 170	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
445	443, 444	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
446	434, 445	breqtrrd 5128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))
447	446	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
448	67	breq2d 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 0s → ( 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
449	448	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 0s → ((𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ↔ (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))))
450	447, 449	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 = 0s → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
451	144	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s ∈ No )
452	249	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
453	134	adantrl 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
454	452, 453	mulscld 28148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
455	439	adantrl 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
456	451, 454, 455	addsubsassd 28094	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
457	2	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
458	452, 457, 453	subsdird 28172	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
459	458	oveq2d 7386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
460	456, 459	eqtr4d 2775	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
461	191	simp2d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
462	461	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
463	198	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
464	201	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑦𝑅))
465	464	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)))
466	465, 204	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
467	466	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
468	467, 314	rspc2ev 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝑅‘𝑖) ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
469	200, 468	mp3an3 1453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
470	469	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
471		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
472	471	2rexbidv 3203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
473	214, 472	elab 3636	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
474	470, 473	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})
475		elun2 4137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))
476		elun2 4137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
477	474, 475, 476	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
478	11, 12, 13	precsexlem4 28223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
479	478	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
480	477, 479	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
481		fveq2 6844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → (𝐿‘𝑗) = (𝐿‘suc 𝑖))
482	481	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)))
483	482	rspcev 3578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
484	463, 480, 483	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
485	484	rexlimdvaa 3140	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
486		eliun 4952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
487		funiunfv 7206	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐿 → ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω))
488	43, 487	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω)
489	488	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
490	486, 489	bitr3i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
491	485, 332, 490	3imtr3g 295	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
492	491	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
493	196	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
494	462, 492, 493	sltssepcd 27785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
495	252	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 -s 𝐴) ∈ No )
496	495, 453	mulscld 28148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
497	451, 496	addscld 27993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
498	56	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
499	260	ad2antrl 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
500	274	adantrr 718	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
501	497, 498, 452, 499, 500	ltdivmulswd 28212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
502	494, 501	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
503	460, 502	eqbrtrd 5122	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
504	451, 454	addscld 27993	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
505	287	adantrr 718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
506	504, 455, 505	ltsubaddsd 28102	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
507	505, 455	addscld 27993	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
508	451, 454, 507	ltaddsubsd 28104	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
509	506, 508	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
510	503, 509	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
511	510	exp32 420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
512	450, 511	jaod 860	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
513	159, 512	biimtrid 242	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
514	513	imp32 418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
515		breq2 5104	. . . . . . . . . 10 ⊢ (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → ( 1s <s 𝑓 ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
516	514, 515	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
517	516	rexlimdvva 3195	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
518	144	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s ∈ No )
519	518, 411, 409	addsubsassd 28094	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
520	404, 407, 408	subsdird 28172	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
521	520	oveq2d 7386	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
522	519, 521	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
523	461	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
524	198	ad2antrl 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
525	305	oveq1d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑦𝐿))
526	525	oveq2d 7386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)))
527	526, 308	oveq12d 7388	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
528	527	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
529	528, 210	rspc2ev 3591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖) ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
530	200, 529	mp3an3 1453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
531	530	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
532		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
533	532	2rexbidv 3203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
534	214, 533	elab 3636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
535	531, 534	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)})
536		elun1 4136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))
537	535, 536, 476	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
538	478	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
539	537, 538	eleqtrrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
540	524, 539, 483	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
541	540	rexlimdvaa 3140	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
542	541, 177, 490	3imtr3g 295	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (𝑑 ∈ ∪ (𝐿 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
543	542	impr 454	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
544	196	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
545	523, 543, 544	sltssepcd 27785	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
546	338	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 -s 𝐴) ∈ No )
547	546, 408	mulscld 28148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
548	518, 547	addscld 27993	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
549	346	adantrr 718	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
550	352	adantrr 718	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
551	548, 405, 404, 549, 550	ltdivmulswd 28212	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
552	545, 551	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
553	522, 552	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
554	518, 411	addscld 27993	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
555	554, 409, 406	ltsubaddsd 28102	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
556	518, 411, 410	ltaddsubsd 28104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
557	555, 556	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
558	553, 557	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
559	558, 515	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
560	559	rexlimdvva 3195	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
561	517, 560	jaod 860	. . . . . . 7 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) → 1s <s 𝑓))
562	425, 561	biimtrid 242	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 1s <s 𝑓))
563		velsn 4598	. . . . . . 7 ⊢ (𝑒 ∈ { 1s } ↔ 𝑒 = 1s )
564		breq1 5103	. . . . . . . 8 ⊢ (𝑒 = 1s → (𝑒 <s 𝑓 ↔ 1s <s 𝑓))
565	564	imbi2d 340	. . . . . . 7 ⊢ (𝑒 = 1s → ((𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓) ↔ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 1s <s 𝑓)))
566	563, 565	sylbi 217	. . . . . 6 ⊢ (𝑒 ∈ { 1s } → ((𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓) ↔ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 1s <s 𝑓)))
567	562, 566	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → (𝑒 ∈ { 1s } → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓)))
568	567	3imp 1111	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ { 1s } ∧ 𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → 𝑒 <s 𝑓)
569	105, 391, 146, 416, 568	sltsd 27781	. . 3 ⊢ (𝜑 → { 1s } <<s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
570	81, 376, 569	cuteq1 27830	. 2 ⊢ (𝜑 → (({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) |s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) = 1s )
571	19, 570	eqtrd 2772	1 ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442  ⦋csb 3851   ∪ cun 3901   ⊆ wss 3903  ∅c0 4287  {csn 4582  ⟨cop 4588  ∪ cuni 4865  ∪ ciun 4948   class class class wbr 5100   ↦ cmpt 5181  ran crn 5635   “ cima 5637   ∘ ccom 5638  suc csuc 6329  Fun wfun 6496  –onto→wfo 6500  ‘cfv 6502  (class class class)co 7370   ∈ cmpo 7372  ωcom 7820  1^st c1st 7943  2^nd c2nd 7944  reccrdg 8352   No csur 27624   <s clts 27625   <<s cslts 27770   |s ccuts 27772   0_s c0s 27818   1_s c1s 27819   L cleft 27838   R cright 27839   +_s cadds 27972   -_s csubs 28033   ·_s cmuls 28119   /_su cdivs 28200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-dc 10370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-ot 4591  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-se 5588  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-2o 8410  df-oadd 8413  df-nadd 8606  df-no 27627  df-lts 27628  df-bday 27629  df-les 27730  df-slts 27771  df-cuts 27773  df-0s 27820  df-1s 27821  df-made 27840  df-old 27841  df-left 27843  df-right 27844  df-norec 27951  df-norec2 27962  df-adds 27973  df-negs 28034  df-subs 28035  df-muls 28120  df-divs 28201

This theorem is referenced by:  precsex  28231