Theorem precsexlem11 28259

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		lltropt 27929	. . . 4 ⊢ ( L ‘𝐴) <<s ( R ‘𝐴)
2		precsexlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ No )
3		precsexlem.5	. . . . . . 7 ⊢ (𝜑 → 0s <s 𝐴)
4	2, 3	0elleft 27966	. . . . . 6 ⊢ (𝜑 → 0s ∈ ( L ‘𝐴))
5	4	snssd 4834	. . . . 5 ⊢ (𝜑 → { 0s } ⊆ ( L ‘𝐴))
6		ssrab2 4103	. . . . . 6 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ ( L ‘𝐴)
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ ( L ‘𝐴))
8	5, 7	unssd 4215	. . . 4 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ ( L ‘𝐴))
9		sssslt1 27858	. . . 4 ⊢ ((( L ‘𝐴) <<s ( R ‘𝐴) ∧ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ⊆ ( L ‘𝐴)) → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴))
10	1, 8, 9	sylancr 586	. . 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 28258	. . 3 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
16	2, 3	cutpos 27985	. . 3 ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴)))
17		precsexlem.7	. . . 4 ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))
18	17	a1i 11	. . 3 ⊢ (𝜑 → 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)))
19	10, 15, 16, 18	mulsunif 28194	. 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		0sno 27889	. . . . . . . . 9 ⊢ 0s ∈ No
21	20	elexi 3511	. . . . . . . 8 ⊢ 0s ∈ V
22	21	snid 4684	. . . . . . 7 ⊢ 0s ∈ { 0s }
23		elun1 4205	. . . . . . 7 ⊢ ( 0s ∈ { 0s } → 0s ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
24	22, 23	ax-mp 5	. . . . . 6 ⊢ 0s ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})
25		peano1 7927	. . . . . . . . 9 ⊢ ∅ ∈ ω
26	11, 12, 13	precsexlem1 28249	. . . . . . . . . 10 ⊢ (𝐿‘∅) = { 0s }
27	22, 26	eleqtrri 2843	. . . . . . . . 9 ⊢ 0s ∈ (𝐿‘∅)
28		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝐿‘𝑏) = (𝐿‘∅))
29	28	eleq2d 2830	. . . . . . . . . 10 ⊢ (𝑏 = ∅ → ( 0s ∈ (𝐿‘𝑏) ↔ 0s ∈ (𝐿‘∅)))
30	29	rspcev 3635	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 0s ∈ (𝐿‘∅)) → ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
31	25, 27, 30	mp2an 691	. . . . . . . 8 ⊢ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏)
32		eliun 5019	. . . . . . . 8 ⊢ ( 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏) ↔ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
33	31, 32	mpbir 231	. . . . . . 7 ⊢ 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏)
34		fo1st 8050	. . . . . . . . . . 11 ⊢ 1st :V–onto→V
35		fofun 6835	. . . . . . . . . . 11 ⊢ (1st :V–onto→V → Fun 1st )
36	34, 35	ax-mp 5	. . . . . . . . . 10 ⊢ Fun 1st
37		rdgfun 8472	. . . . . . . . . . 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 6599	. . . . . . . . . . 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 6618	. . . . . . . . . 10 ⊢ ((Fun 1st ∧ Fun 𝐹) → Fun (1st ∘ 𝐹))
41	36, 39, 40	mp2an 691	. . . . . . . . 9 ⊢ Fun (1st ∘ 𝐹)
42	12	funeqi 6599	. . . . . . . . 9 ⊢ (Fun 𝐿 ↔ Fun (1st ∘ 𝐹))
43	41, 42	mpbir 231	. . . . . . . 8 ⊢ Fun 𝐿
44		funiunfv 7285	. . . . . . . 8 ⊢ (Fun 𝐿 → ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω))
45	43, 44	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω)
46	33, 45	eleqtri 2842	. . . . . 6 ⊢ 0s ∈ ∪ (𝐿 “ ω)
47		addsrid 28015	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
48	20, 47	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s +s 0s ) = 0s
49		muls01 28156	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s ·s 0s ) = 0s )
50	20, 49	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s ·s 0s ) = 0s
51	48, 50	oveq12i 7460	. . . . . . . 8 ⊢ (( 0s +s 0s ) -s ( 0s ·s 0s )) = ( 0s -s 0s )
52		subsid 28117	. . . . . . . . 9 ⊢ ( 0s ∈ No → ( 0s -s 0s ) = 0s )
53	20, 52	ax-mp 5	. . . . . . . 8 ⊢ ( 0s -s 0s ) = 0s
54	51, 53	eqtr2i 2769	. . . . . . 7 ⊢ 0s = (( 0s +s 0s ) -s ( 0s ·s 0s ))
55	15	scutcld 27866	. . . . . . . . . . 11 ⊢ (𝜑 → (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No )
56	17, 55	eqeltrid 2848	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ No )
57		muls02 28185	. . . . . . . . . 10 ⊢ (𝑌 ∈ No → ( 0s ·s 𝑌) = 0s )
58	56, 57	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ( 0s ·s 𝑌) = 0s )
59		muls01 28156	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
60	2, 59	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
61	58, 60	oveq12d 7466	. . . . . . . 8 ⊢ (𝜑 → (( 0s ·s 𝑌) +s (𝐴 ·s 0s )) = ( 0s +s 0s ))
62	61	oveq1d 7463	. . . . . . 7 ⊢ (𝜑 → ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )) = (( 0s +s 0s ) -s ( 0s ·s 0s )))
63	54, 62	eqtr4id 2799	. . . . . 6 ⊢ (𝜑 → 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )))
64		oveq1 7455	. . . . . . . . . 10 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑌) = ( 0s ·s 𝑌))
65	64	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑐 = 0s → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)))
66		oveq1 7455	. . . . . . . . 9 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑑) = ( 0s ·s 𝑑))
67	65, 66	oveq12d 7466	. . . . . . . 8 ⊢ (𝑐 = 0s → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))
68	67	eqeq2d 2751	. . . . . . 7 ⊢ (𝑐 = 0s → ( 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
69		oveq2 7456	. . . . . . . . . 10 ⊢ (𝑑 = 0s → (𝐴 ·s 𝑑) = (𝐴 ·s 0s ))
70	69	oveq2d 7464	. . . . . . . . 9 ⊢ (𝑑 = 0s → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 0s )))
71		oveq2 7456	. . . . . . . . 9 ⊢ (𝑑 = 0s → ( 0s ·s 𝑑) = ( 0s ·s 0s ))
72	70, 71	oveq12d 7466	. . . . . . . 8 ⊢ (𝑑 = 0s → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s )))
73	72	eqeq2d 2751	. . . . . . 7 ⊢ (𝑑 = 0s → ( 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) -s ( 0s ·s 0s ))))
74	68, 73	rspc2ev 3648	. . . . . 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 1465	. . . . 5 ⊢ (𝜑 → ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
76		eqeq1 2744	. . . . . . 7 ⊢ (𝑏 = 0s → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
77	76	2rexbidv 3228	. . . . . 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 3694	. . . . 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 4205	. . . 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 2740	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
83	82	rnmpo 7583	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
84		ssltex1 27849	. . . . . . . . 9 ⊢ (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) <<s ( R ‘𝐴) → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
85	10, 84	syl 17	. . . . . . . 8 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
86		ssltex1 27849	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ∈ V)
87	15, 86	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝐿 “ ω) ∈ V)
88		mpoexga 8118	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
89	85, 87, 88	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
90		rnexg 7942	. . . . . . 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 2849	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
93		eqid 2740	. . . . . . 7 ⊢ (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
94	93	rnmpo 7583	. . . . . 6 ⊢ ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
95		fvex 6933	. . . . . . . 8 ⊢ ( R ‘𝐴) ∈ V
96		ssltex2 27850	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ∈ V)
97	15, 96	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝑅 “ ω) ∈ V)
98		mpoexga 8118	. . . . . . . 8 ⊢ ((( R ‘𝐴) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
99	95, 97, 98	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
100		rnexg 7942	. . . . . . 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 2849	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
103	92, 102	unexd 7789	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∈ V)
104		snex 5451	. . . . 5 ⊢ { 1s } ∈ V
105	104	a1i 11	. . . 4 ⊢ (𝜑 → { 1s } ∈ V)
106		ssltss1 27851	. . . . . . . . . . . . . 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 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})) → 𝑐 ∈ No )
109	108	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
110	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No )
111	109, 110	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
112	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No )
113		ssltss1 27851	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ⊆ No )
114	15, 113	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝐿 “ ω) ⊆ No )
115	114	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝑑 ∈ No )
116	115	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
117	112, 116	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
118	111, 117	addscld 28031	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
119	109, 116	mulscld 28179	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
120	118, 119	subscld 28111	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
121		eleq1 2832	. . . . . . . 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 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
124	123	abssdv 4091	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
125		rightssno 27938	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝐴) ⊆ No
126	125	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( R ‘𝐴) ⊆ No )
127	126	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑐 ∈ No )
128	127	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
129	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
130	128, 129	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
131	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
132		ssltss2 27852	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ⊆ No )
133	15, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝑅 “ ω) ⊆ No )
134	133	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑑 ∈ No )
135	134	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
136	131, 135	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
137	130, 136	addscld 28031	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
138	128, 135	mulscld 28179	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
139	137, 138	subscld 28111	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
140	139, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
141	140	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
142	141	abssdv 4091	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
143	124, 142	unssd 4215	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ⊆ No )
144		1sno 27890	. . . . 5 ⊢ 1s ∈ No
145		snssi 4833	. . . . 5 ⊢ ( 1s ∈ No → { 1s } ⊆ No )
146	144, 145	mp1i 13	. . . 4 ⊢ (𝜑 → { 1s } ⊆ No )
147		elun 4176	. . . . . . . . 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 3492	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
149		eqeq1 2744	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
150	149	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
151	148, 150	elab 3694	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
152	149	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
153	148, 152	elab 3694	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
154	151, 153	orbi12i 913	. . . . . . . . 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 4176	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 ∈ { 0s } ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}))
157		velsn 4664	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ { 0s } ↔ 𝑐 = 0s )
158	157	orbi1i 912	. . . . . . . . . . . . . 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 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
162		muls02 28185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ No → ( 0s ·s 𝑑) = 0s )
163	115, 162	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s ·s 𝑑) = 0s )
164	161, 163	oveq12d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (( 0s +s (𝐴 ·s 𝑑)) -s 0s ))
165	2	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝐴 ∈ No )
166	165, 115	mulscld 28179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (𝐴 ·s 𝑑) ∈ No )
167		addslid 28019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ·s 𝑑) ∈ No → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
168	166, 167	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
169	168	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s +s (𝐴 ·s 𝑑)) -s 0s ) = ((𝐴 ·s 𝑑) -s 0s ))
170		subsid1 28116	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ·s 𝑑) ∈ No → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
171	166, 170	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
172	164, 169, 171	3eqtrd 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
173		eliun 5019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖))
174		funiunfv 7285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐿 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω))
175	43, 174	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω)
176	175	eleq2i 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
177	173, 176	bitr3i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
178	11, 12, 13, 2, 3, 14	precsexlem9 28257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)))
179	178	simpld 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s )
180		rsp 3253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
181	179, 180	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
182	181	rexlimdva 3161	. . . . . . . . . . . . . . . . . . 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 5188	. . . . . . . . . . . . . . . 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 5176	. . . . . . . . . . . . . . . 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		scutcut 27864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
191	15, 190	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
192	191	simp3d 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
193	192	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
194		ovex 7481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ V
195	194	snid 4684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
196	17, 195	eqeltri 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
197	196	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
198		peano2 7929	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
199	198	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
200		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)
201		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥𝐿 = 𝑐 → (𝑥𝐿 -s 𝐴) = (𝑐 -s 𝐴))
202	201	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑦𝐿))
203	202	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)))
204		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → 𝑥𝐿 = 𝑐)
205	203, 204	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
206	205	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
207		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦𝐿 = 𝑑 → ((𝑐 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑑))
208	207	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦𝐿 = 𝑑 → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
209	208	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦𝐿 = 𝑑 → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
210	209	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3648	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
213	212	ad2ant2l 745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
214		ovex 7481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ V
215		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
216	215	2rexbidv 3228	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3694	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4205	. . . . . . . . . . . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . . . . . . . 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 28253	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
223	222	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
224	221, 223	eleqtrrd 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
225		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = suc 𝑖 → (𝑅‘𝑗) = (𝑅‘suc 𝑖))
226	225	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)))
227	226	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
228	199, 224, 227	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
229	228	rexlimdvaa 3162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
230		eliun 5019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
231		fo2nd 8051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2nd :V–onto→V
232		fofun 6835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd :V–onto→V → Fun 2nd )
233	231, 232	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Fun 2nd
234		funco 6618	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd ∘ 𝐹))
235	233, 39, 234	mp2an 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Fun (2nd ∘ 𝐹)
236	13	funeqi 6599	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun 𝑅 ↔ Fun (2nd ∘ 𝐹))
237	235, 236	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Fun 𝑅
238		funiunfv 7285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑅 → ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω))
239	237, 238	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω)
240	239	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . . 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	ssltsepcd 27857	. . . . . . . . . . . . . . . . . 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 27937	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( L ‘𝐴) ⊆ No
248	6, 247	sstri 4018	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ No
249	248	sseli 4004	. . . . . . . . . . . . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 -s 𝐴) ∈ No )
253	252	adantrr 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 -s 𝐴) ∈ No )
254	115	adantrl 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
255	253, 254	mulscld 28179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
256	246, 255	addscld 28031	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
257	249	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
258		breq2 5170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑐 → ( 0s <s 𝑥 ↔ 0s <s 𝑐))
259	258	elrab 3708	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑐 ∈ ( L ‘𝐴) ∧ 0s <s 𝑐))
260	259	simprbi 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑐)
261	260	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
262	260	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑐)
263		breq2 5170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥𝑂 = 𝑐 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑐))
264		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑂 = 𝑐 → (𝑥𝑂 ·s 𝑦) = (𝑐 ·s 𝑦))
265	264	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑂 = 𝑐 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑐 ·s 𝑦) = 1s ))
266	265	rexbidv 3185	. . . . . . . . . . . . . . . . . . . . . . 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 4201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ( L ‘𝐴) ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
270	6, 269	sstri 4018	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ⊆ (( L ‘𝐴) ∪ ( R ‘𝐴))
271	270	sseli 4004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
272	271	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
273	267, 268, 272	rspcdva 3636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
274	262, 273	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
275	274	adantrr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
276	245, 256, 257, 261, 275	sltmuldiv2wd 28245	. . . . . . . . . . . . . . . . . 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 28179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
279	166	adantrl 715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
280	246, 278, 279	addsubsassd 28129	. . . . . . . . . . . . . . . . . 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 28203	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
283	282	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
284	280, 283	eqtr4d 2783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
285	277, 284	breqtrrd 5194	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)))
286	56	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑌 ∈ No )
287	250, 286	mulscld 28179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 ·s 𝑌) ∈ No )
288	287	adantrr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
289	288, 279	addscld 28031	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
290	289, 278, 246	sltsubaddd 28137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
291	246, 278	addscld 28031	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
292	288, 279, 291	sltaddsubd 28139	. . . . . . . . . . . . . . . . 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 858	. . . . . . . . . . . . 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 5169	. . . . . . . . . . 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 3219	. . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
305		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝑅 = 𝑐 → (𝑥𝑅 -s 𝐴) = (𝑐 -s 𝐴))
306	305	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑦𝑅))
307	306	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)))
308		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → 𝑥𝑅 = 𝑐)
309	307, 308	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
310	309	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
311		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦𝑅 = 𝑑 → ((𝑐 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑑))
312	311	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦𝑅 = 𝑑 → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
313	312	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦𝑅 = 𝑑 → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐))
314	313	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . 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 3648	. . . . . . . . . . . . . . . . . . . . . . . 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 1450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
317	316	ad2ant2l 745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
318		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
319	318	2rexbidv 3228	. . . . . . . . . . . . . . . . . . . . . . 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 3694	. . . . . . . . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
325	323, 324	eleqtrrd 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
326	304, 325, 227	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
327	326	rexlimdvaa 3162	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
328		eliun 5019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝑅‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖))
329		funiunfv 7285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑅 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω))
330	237, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω)
331	330	eleq2i 2836	. . . . . . . . . . . . . . . . . 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	ssltsepcd 27857	. . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (𝑐 -s 𝐴) ∈ No )
339	338	adantrr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 -s 𝐴) ∈ No )
340	339, 135	mulscld 28179	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
341	336, 340	addscld 28031	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
342	20	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s ∈ No )
343	3	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
344		breq2 5170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑐 → (𝐴 <s 𝑥𝑂 ↔ 𝐴 <s 𝑐))
345		rightval 27921	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( R ‘𝐴) = {𝑥𝑂 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥𝑂}
346	344, 345	elrab2 3711	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ( R ‘𝐴) ↔ (𝑐 ∈ ( O ‘( bday ‘𝐴)) ∧ 𝐴 <s 𝑐))
347	346	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ ( R ‘𝐴) → 𝐴 <s 𝑐)
348	347	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑐)
349	342, 337, 127, 343, 348	slttrd 27822	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 0s <s 𝑐)
350	349	adantrr 716	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
351	14	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
352		elun2 4206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ ( R ‘𝐴) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
353	352	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑐 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
354	267, 351, 353	rspcdva 3636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
355	349, 354	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
356	355	adantrr 716	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
357	129, 341, 128, 350, 356	sltmuldiv2wd 28245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ↔ 𝑌 <s (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)))
358	335, 357	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
359	336, 138, 136	addsubsassd 28129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
360	128, 131, 135	subsdird 28203	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
361	360	oveq2d 7464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
362	359, 361	eqtr4d 2783	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
363	358, 362	breqtrrd 5194	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)))
364	137, 138, 336	sltsubaddd 28137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
365	336, 138	addscld 28031	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
366	130, 136, 365	sltaddsubd 28139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑)) ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
367	364, 366	bitrd 279	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑))))
368	363, 367	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) <s 1s )
369	368, 299	syl5ibrcom 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
370	369	rexlimdvva 3219	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
371	301, 370	jaod 858	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) → 𝑒 <s 1s ))
372	155, 371	biimtrid 242	. . . . . . 7 ⊢ (𝜑 → (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 1s ))
373	372	imp 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → 𝑒 <s 1s )
374		velsn 4664	. . . . . . 7 ⊢ (𝑓 ∈ { 1s } ↔ 𝑓 = 1s )
375		breq2 5170	. . . . . . 7 ⊢ (𝑓 = 1s → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
376	374, 375	sylbi 217	. . . . . 6 ⊢ (𝑓 ∈ { 1s } → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
377	373, 376	syl5ibrcom 247	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → (𝑓 ∈ { 1s } → 𝑒 <s 𝑓))
378	377	3impia 1117	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∧ 𝑓 ∈ { 1s }) → 𝑒 <s 𝑓)
379	103, 105, 143, 146, 378	ssltd 27854	. . 3 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) <<s { 1s })
380		eqid 2740	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
381	380	rnmpo 7583	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
382		mpoexga 8118	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
383	85, 97, 382	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
384		rnexg 7942	. . . . . . 7 ⊢ ((𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
385	383, 384	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
386	381, 385	eqeltrrid 2849	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
387		eqid 2740	. . . . . . 7 ⊢ (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
388	387	rnmpo 7583	. . . . . 6 ⊢ ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}
389		mpoexga 8118	. . . . . . . 8 ⊢ ((( R ‘𝐴) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
390	95, 87, 389	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
391		rnexg 7942	. . . . . . 7 ⊢ ((𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
392	390, 391	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ( R ‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ∈ V)
393	388, 392	eqeltrrid 2849	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∈ V)
394	386, 393	unexd 7789	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ∈ V)
395	108	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
396	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
397	395, 396	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
398	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
399	134	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
400	398, 399	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
401	397, 400	addscld 28031	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
402	395, 399	mulscld 28179	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
403	401, 402	subscld 28111	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
404	403, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
405	404	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
406	405	abssdv 4091	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
407	127	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No )
408	56	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No )
409	407, 408	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
410	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No )
411	115	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No )
412	410, 411	mulscld 28179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
413	409, 412	addscld 28031	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
414	407, 411	mulscld 28179	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
415	413, 414	subscld 28111	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∈ No )
416	415, 121	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
417	416	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 𝑏 ∈ No ))
418	417	abssdv 4091	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ⊆ No )
419	406, 418	unssd 4215	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) ⊆ No )
420		elun 4176	. . . . . . . 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 𝑑))}))
421		vex 3492	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
422		eqeq1 2744	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑓 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
423	422	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
424	421, 423	elab 3694	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
425	422	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
426	421, 425	elab 3694	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
427	424, 426	orbi12i 913	. . . . . . . 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 𝑑))))
428	420, 427	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 𝑑))))
429		eliun 5019	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗))
430	239	eleq2i 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
431	429, 430	bitr3i 277	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
432	11, 12, 13, 2, 3, 14	precsexlem9 28257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (∀𝑐 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑐) <s 1s ∧ ∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑)))
433		rsp 3253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
434	432, 433	simpl2im 503	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
435	434	rexlimdva 3161	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
436	431, 435	biimtrrid 243	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (𝐴 ·s 𝑑)))
437	436	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s (𝐴 ·s 𝑑))
438	56	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑌 ∈ No )
439	57	oveq1d 7463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 ∈ No → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
440	438, 439	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
441	2	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝐴 ∈ No )
442	441, 134	mulscld 28179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (𝐴 ·s 𝑑) ∈ No )
443	442, 167	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
444	440, 443	eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
445	134, 162	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s ·s 𝑑) = 0s )
446	444, 445	oveq12d 7466	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = ((𝐴 ·s 𝑑) -s 0s ))
447	442, 170	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((𝐴 ·s 𝑑) -s 0s ) = (𝐴 ·s 𝑑))
448	446, 447	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
449	437, 448	breqtrrd 5194	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))
450	449	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
451	67	breq2d 5178	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 0s → ( 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ↔ 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑))))
452	451	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 0s → ((𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) ↔ (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) -s ( 0s ·s 𝑑)))))
453	450, 452	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 = 0s → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
454	144	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s ∈ No )
455	249	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No )
456	134	adantrl 715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No )
457	455, 456	mulscld 28179	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No )
458	442	adantrl 715	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No )
459	454, 457, 458	addsubsassd 28129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
460	2	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No )
461	455, 460, 456	subsdird 28203	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
462	461	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
463	459, 462	eqtr4d 2783	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
464	191	simp2d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
465	464	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
466	198	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
467	201	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) = ((𝑐 -s 𝐴) ·s 𝑦𝑅))
468	467	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)))
469	468, 204	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
470	469	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
471	470, 314	rspc2ev 3648	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 𝑥𝐿))
472	200, 471	mp3an3 1450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
473	472	ad2ant2l 745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
474		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
475	474	2rexbidv 3228	. . . . . . . . . . . . . . . . . . . . . . . . . 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 𝑥𝐿)))
476	214, 475	elab 3694	. . . . . . . . . . . . . . . . . . . . . . . . 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 𝑥𝐿))
477	473, 476	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})
478		elun2 4206	. . . . . . . . . . . . . . . . . . . . . . . 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 𝑥𝐿)}))
479		elun2 4206	. . . . . . . . . . . . . . . . . . . . . . . 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 𝑥𝐿)})))
480	477, 478, 479	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 𝑥𝐿)})))
481	11, 12, 13	precsexlem4 28252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
482	481	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
483	480, 482	eleqtrrd 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
484		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → (𝐿‘𝑗) = (𝐿‘suc 𝑖))
485	484	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)))
486	485	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
487	466, 483, 486	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
488	487	rexlimdvaa 3162	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
489		eliun 5019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
490		funiunfv 7285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐿 → ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω))
491	43, 490	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω)
492	491	eleq2i 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
493	489, 492	bitr3i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
494	488, 332, 493	3imtr3g 295	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
495	494	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
496	196	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
497	465, 495, 496	ssltsepcd 27857	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
498	252	adantrr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 -s 𝐴) ∈ No )
499	498, 456	mulscld 28179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
500	454, 499	addscld 28031	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
501	56	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No )
502	260	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
503	274	adantrr 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
504	500, 501, 455, 502, 503	sltdivmulwd 28242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
505	497, 504	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
506	463, 505	eqbrtrd 5188	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
507	454, 457	addscld 28031	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
508	287	adantrr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No )
509	507, 458, 508	sltsubaddd 28137	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
510	508, 458	addscld 28031	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No )
511	454, 457, 510	sltaddsubd 28139	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
512	509, 511	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
513	506, 512	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
514	513	exp32 420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
515	453, 514	jaod 858	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
516	159, 515	biimtrid 242	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))))
517	516	imp32 418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
518		breq2 5170	. . . . . . . . . 10 ⊢ (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → ( 1s <s 𝑓 ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
519	517, 518	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
520	519	rexlimdvva 3219	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
521	144	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s ∈ No )
522	521, 414, 412	addsubsassd 28129	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
523	407, 410, 411	subsdird 28203	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑)))
524	523	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) -s (𝐴 ·s 𝑑))))
525	522, 524	eqtr4d 2783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)))
526	464	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
527	198	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
528	305	oveq1d 7463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) = ((𝑐 -s 𝐴) ·s 𝑦𝐿))
529	528	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)))
530	529, 308	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
531	530	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
532	531, 210	rspc2ev 3648	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖) ∧ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
533	200, 532	mp3an3 1450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
534	533	ad2ant2l 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
535		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
536	535	2rexbidv 3228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
537	214, 536	elab 3694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
538	534, 537	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)})
539		elun1 4205	. . . . . . . . . . . . . . . . . . . 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 𝑥𝐿)}))
540	538, 539, 479	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
541	481	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
542	540, 541	eleqtrrd 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
543	527, 542, 486	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
544	543	rexlimdvaa 3162	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
545	544, 177, 493	3imtr3g 295	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (𝑑 ∈ ∪ (𝐿 “ ω) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
546	545	impr 454	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
547	196	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
548	526, 546, 547	ssltsepcd 27857	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
549	338	adantrr 716	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 -s 𝐴) ∈ No )
550	549, 411	mulscld 28179	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 -s 𝐴) ·s 𝑑) ∈ No )
551	521, 550	addscld 28031	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) ∈ No )
552	349	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
553	355	adantrr 716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
554	551, 408, 407, 552, 553	sltdivmulwd 28242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
555	548, 554	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 -s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
556	525, 555	eqbrtrd 5188	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
557	521, 414	addscld 28031	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No )
558	557, 412, 409	sltsubaddd 28137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
559	521, 414, 413	sltaddsubd 28139	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
560	558, 559	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) -s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))))
561	556, 560	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)))
562	561, 518	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ( R ‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
563	562	rexlimdvva 3219	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
564	520, 563	jaod 858	. . . . . . 7 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))) → 1s <s 𝑓))
565	428, 564	biimtrid 242	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 1s <s 𝑓))
566		velsn 4664	. . . . . . 7 ⊢ (𝑒 ∈ { 1s } ↔ 𝑒 = 1s )
567		breq1 5169	. . . . . . . 8 ⊢ (𝑒 = 1s → (𝑒 <s 𝑓 ↔ 1s <s 𝑓))
568	567	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 𝑓)))
569	566, 568	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 𝑓)))
570	565, 569	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → (𝑒 ∈ { 1s } → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓)))
571	570	3imp 1111	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ { 1s } ∧ 𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))})) → 𝑒 <s 𝑓)
572	105, 394, 146, 419, 571	ssltd 27854	. . 3 ⊢ (𝜑 → { 1s } <<s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) -s (𝑐 ·s 𝑑))}))
573	81, 379, 572	cuteq1 27896	. 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 )
574	19, 573	eqtrd 2780	1 ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {cab 2717  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488  ⦋csb 3921   ∪ cun 3974   ⊆ wss 3976  ∅c0 4352  {csn 4648  ⟨cop 4654  ∪ cuni 4931  ∪ ciun 5015   class class class wbr 5166   ↦ cmpt 5249  ran crn 5701   “ cima 5703   ∘ ccom 5704  suc csuc 6397  Fun wfun 6567  –onto→wfo 6571  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  ωcom 7903  1^st c1st 8028  2^nd c2nd 8029  reccrdg 8465   No csur 27702   <s cslt 27703   bday cbday 27704   <<s csslt 27843   |s cscut 27845   0_s c0s 27885   1_s c1s 27886   O cold 27900   L cleft 27902   R cright 27903   +_s cadds 28010   -_s csubs 28070   ·_s cmuls 28150   /_su cdivs 28231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-dc 10515

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-ot 4657  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sle 27808  df-sslt 27844  df-scut 27846  df-0s 27887  df-1s 27888  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec 27989  df-norec2 28000  df-adds 28011  df-negs 28071  df-subs 28072  df-muls 28151  df-divs 28232

This theorem is referenced by:  precsex  28260