Theorem omssubadd 34979

Description: A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) (Revised by AV, 4-Oct-2020.) Remove dependency on ax-reg 9590. (Revised by Timothy J. O'Malley, 15-Oct-2026.)

Hypotheses

Ref	Expression
oms.m	⊢ 𝑀 = (toOMeas‘𝑅)
oms.o	⊢ (𝜑 → 𝑄 ∈ 𝑉)
oms.r	⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))
omssubadd.a	⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄)
omssubadd.b	⊢ (𝜑 → 𝑋 ≼ ω)

Assertion

Ref	Expression
omssubadd	⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))

Distinct variable groups:   𝑦,𝑄   𝑦,𝑅   𝑦,𝑉   𝜑,𝑦   𝑦,𝑋

Allowed substitution hints:   𝐴(𝑦)   𝑀(𝑦)

Proof of Theorem omssubadd

Dummy variables 𝑥 𝑧 𝑒 𝑡 𝑢 𝑤 𝑓 𝑔 ℎ 𝑣 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omssubadd.b	. . . . . 6 ⊢ (𝜑 → 𝑋 ≼ ω)
2		nnenom 14127	. . . . . . 7 ⊢ ℕ ≈ ω
3		domen2 9143	. . . . . . 7 ⊢ (ℕ ≈ ω → (𝑋 ≼ ℕ ↔ 𝑋 ≼ ω))
4	2, 3	ax-mp 5	. . . . . 6 ⊢ (𝑋 ≼ ℕ ↔ 𝑋 ≼ ω)
5	1, 4	sylibr 237	. . . . 5 ⊢ (𝜑 → 𝑋 ≼ ℕ)
6		brdomi 8990	. . . . 5 ⊢ (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋–1-1→ℕ)
7	5, 6	syl 18	. . . 4 ⊢ (𝜑 → ∃𝑓 𝑓:𝑋–1-1→ℕ)
8	7	adantr 486	. . 3 ⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋–1-1→ℕ)
9		simplll 787	. . . . . . . 8 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10		ctex 8994	. . . . . . . . 9 ⊢ (𝑋 ≼ ω → 𝑋 ∈ V)
11	1, 10	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ V)
12	9, 11	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13		oms.r	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))
14		oms.o	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ 𝑉)
15	13, 14	fexd 7234	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ V)
16		dmexg 7914	. . . . . . . . . 10 ⊢ (𝑅 ∈ V → dom 𝑅 ∈ V)
17		pwexg 5339	. . . . . . . . . 10 ⊢ (dom 𝑅 ∈ V → 𝒫 dom 𝑅 ∈ V)
18	15, 16, 17	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 dom 𝑅 ∈ V)
19		rabexg 5298	. . . . . . . . 9 ⊢ (𝒫 dom 𝑅 ∈ V → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
20	18, 19	syl 18	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
21	20	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
22		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝜑
23		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑋
24	23	nfesum1 34719	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)
25	24	nfel1 2938	. . . . . . . . . . 11 ⊢ Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ
26	22, 25	nfan 1931	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
27		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑓:𝑋–1-1→ℕ
28	26, 27	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ)
29		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑒 ∈ ℝ+
30	28, 29	nfan 1931	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
31	9	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝜑)
32		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
33	11	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V)
34		omsf 34975	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞))
35		oms.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑀 = (toOMeas‘𝑅)
36	35	feq1i 6701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞))
37	34, 36	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞))
38	14, 13, 37	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞))
39	38	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞))
40	14	uniexd 7760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝑄 ∈ V)
41	40	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V)
42		omssubadd.a	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄)
43	41, 42	ssexd 5285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V)
44	13	fdmd 6721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝑅 = 𝑄)
45	44	unieqd 4879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄)
46	45	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom 𝑅 = ∪ 𝑄)
47	42, 46	sseqtrrd 3945	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom 𝑅)
48	43, 47	elpwd 4562	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅)
49	39, 48	ffvelcdmd 7086	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
50	49	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
51		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
52	26, 33, 50, 51	esumcvgre 34770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ)
53	52	ad4ant14 765	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ)
54		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+)
55		2rp 13129	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ+
56	55	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ+)
57		f1f 6779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑋–1-1→ℕ → 𝑓:𝑋⟶ℕ)
58	57	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑓:𝑋⟶ℕ)
59	58	ffvelcdmda 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ)
60	59	nnzd 12723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
61	56, 60	rpexpcld 14395	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ+)
62	61	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ+)
63	54, 62	rpdivcld 13185	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ+)
64	63	rpred 13168	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
65	64	adantl3r 763	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
66	53, 65	rexaddd 13368	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
67	49	ad5ant15 771	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
68		dfrp2 13529	. . . . . . . . . . . . . . . 16 ⊢ ℝ+ = (0(,)+∞)
69		ioossicc 13568	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) ⊆ (0[,]+∞)
70	68, 69	eqsstri 3954	. . . . . . . . . . . . . . 15 ⊢ ℝ+ ⊆ (0[,]+∞)
71	70, 63	sselid 3906	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
72	71	adantl3r 763	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
73	67, 72	xrge0addcld 33401	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
74	66, 73	eqeltrrd 2861	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
75	35	fveq1i 6887	. . . . . . . . . . . . . 14 ⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴)
76	14	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉)
77	13	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞))
78		omsfval 34973	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
79	76, 77, 42, 78	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
80	75, 79	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
81	80	ad5ant15 771	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
82	54	rpred 13168	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ)
83	82	adantl3r 763	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ)
84	61	rpred 13168	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ)
85	84	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ)
86	85	adantl3r 763	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ)
87		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+)
88	87	rpgt0d 13171	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒)
89		2re 12421	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90	60	adantllr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
91	90	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
92		2pos 12451	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
93	92	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 2)
94		expgt0 14242	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓‘𝑦)))
95	89, 91, 93, 94	mp3an2i 1495	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦)))
96	83, 86, 88, 95	divgt0d 12256	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦))))
97	65, 53	ltaddposd 11904	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
98	96, 97	mpbid 235	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
99	81, 98	eqbrtrrd 5128	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
100		iccssxr 13565	. . . . . . . . . . . . . . 15 ⊢ (0[,]+∞) ⊆ ℝ*
101		xrltso 13274	. . . . . . . . . . . . . . 15 ⊢ < Or ℝ*
102		soss 5578	. . . . . . . . . . . . . . 15 ⊢ ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
103	100, 101, 102	mp2 9	. . . . . . . . . . . . . 14 ⊢ < Or (0[,]+∞)
104	103	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or (0[,]+∞))
105		omscl 34974	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
106	76, 77, 48, 105	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
107		xrge0infss 33399	. . . . . . . . . . . . . 14 ⊢ (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ℎ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ℎ)))
108	106, 107	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ℎ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ℎ)))
109	104, 108	infglb 9487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
110	109	imp 412	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
111	31, 32, 74, 99, 110	syl22anc 852	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
112		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
113		esumex 34708	. . . . . . . . . . . . . . . 16 ⊢ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∈ V
114	112, 113	elrnmpti 5943	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
115	114	anbi1i 636	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
116		r19.41v 3192	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
117	115, 116	bitr4i 281	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
118	117	exbii 1880	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
119		df-rex 3087	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
120		rexcom4 3289	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
121	118, 119, 120	3bitr4i 306	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
122		breq1 5105	. . . . . . . . . . . . . 14 ⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
123	122	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
124	123	exlimiv 1962	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
125	124	reximi 3100	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
126	121, 125	sylbi 220	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
127	111, 126	syl 18	. . . . . . . . 9 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
128		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω)
129	128	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω))
130	129	ss2rabi 4001	. . . . . . . . . . 11 ⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}
131		rexss 3982	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
132	130, 131	ax-mp 5	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
133		unieq 4877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪ 𝑥)
134	133	sseq2d 3940	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥))
135		breq1 5105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
136	134, 135	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)))
137	136	elrab 3644	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)))
138	137	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))
139	138	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥)
140	139	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥))
141	140	anim1d 623	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
142	141	reximdv 3177	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
143	132, 142	biimtrid 245	. . . . . . . . 9 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
144	127, 143	mpd 16	. . . . . . . 8 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
145	30, 144	ralrimia 3261	. . . . . . 7 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
146		unieq 4877	. . . . . . . . . 10 ⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪ (𝑔‘𝑦))
147	146	sseq2d 3940	. . . . . . . . 9 ⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦)))
148		esumeq1 34713	. . . . . . . . . 10 ⊢ (𝑥 = (𝑔‘𝑦) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
149	148	breq1d 5112	. . . . . . . . 9 ⊢ (𝑥 = (𝑔‘𝑦) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
150	147, 149	anbi12d 644	. . . . . . . 8 ⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
151	150	ac6 10562	. . . . . . 7 ⊢ ((𝑋 ∈ V ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
152	12, 21, 145, 151	syl3anc 1398	. . . . . 6 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
153		simp-5l 797	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑)
154	43	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V)
155		iunexg 7976	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V)
156	11, 154, 155	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V)
157	47	iunssd 5008	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom 𝑅)
158	156, 157	elpwd 4562	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅)
159	38, 158	ffvelcdmd 7086	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞))
160	100, 159	sselid 3906	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ*)
161	153, 160	syl 18	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ*)
162		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
163	33	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V)
164	162, 163	fexd 7234	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V)
165		rnexg 7915	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ V → ran 𝑔 ∈ V)
166		uniexg 7758	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∈ V → ∪ ran 𝑔 ∈ V)
167	164, 165, 166	3syl 19	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ∈ V)
168	13	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
169		frn 6718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
170		ssrab2 4005	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
171	169, 170	sstrdi 3920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
172	171	unissd 4876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪ 𝒫 dom 𝑅)
173		unipw 5417	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅
174	172, 173	sseqtrdi 3948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅)
175	174	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅)
176	44	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
177	175, 176	sseqtrd 3944	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄)
178	177	sselda 3908	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran 𝑔) → 𝑐 ∈ 𝑄)
179	168, 178	ffvelcdmd 7086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran 𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞))
180	179	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
181	153, 162, 180	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
182		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∪ ran 𝑔
183	182	esumcl 34709	. . . . . . . . . . 11 ⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
184	167, 181, 183	syl2anc 596	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
185	100, 184	sselid 3906	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ*)
186		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
187	186	rexrd 11363	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ*)
188		simpllr 788	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ+)
189	188	rpxrd 13169	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ*)
190	187, 189	xaddcld 13435	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒) ∈ ℝ*)
191	169	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
192		sstr 3916	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
193	170, 192	mpan2 704	. . . . . . . . . . . . . . . . . 18 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
194		sspwuni 5059	. . . . . . . . . . . . . . . . . 18 ⊢ (ran 𝑔 ⊆ 𝒫 dom 𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅)
195	193, 194	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅)
196	191, 195	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ⊆ dom 𝑅)
197		ffn 6710	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑔 Fn 𝑋)
198	197	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 Fn 𝑋)
199	153, 1	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ≼ ω)
200		fnct 10624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω)
201		rnct 10608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ≼ ω → ran 𝑔 ≼ ω)
202	200, 201	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼ ω)
203		dfss3 3897	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
204		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
205	204	elrab 3644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω))
206	205	simprbi 503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω)
207	206	ralimi 3099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
208	203, 207	sylbi 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
209		unictb 10664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ∪ ran 𝑔 ≼ ω)
210	202, 208, 209	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ≼ ω)
211	198, 199, 191, 210	syl21anc 851	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ≼ ω)
212		ctex 8994	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V)
213		elpwg 4559	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran 𝑔 ∈ V → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅))
214	211, 212, 213	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅))
215	196, 214	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ∈ 𝒫 dom 𝑅)
216		simpl 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → 𝐴 ⊆ ∪ (𝑔‘𝑦))
217	216	ralimi 3099	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦))
218		fvssunirn 6917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑦) ⊆ ∪ ran 𝑔
219	218	unissi 4875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔
220		sstr 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔)
221	219, 220	mpan2 704	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔)
222	221	ralimi 3099	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
223		iunss 5002	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
224	222, 223	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
225	217, 224	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
226	225	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
227	215, 226, 211	jca32 525	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼ ω)))
228		unieq 4877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ ran 𝑔 → ∪ 𝑧 = ∪ ∪ ran 𝑔)
229	228	sseq2d 3940	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∪ ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔))
230		breq1 5105	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∪ ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω))
231	229, 230	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∪ ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼ ω)))
232	231	elrab 3644	. . . . . . . . . . . . . 14 ⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼ ω)))
233	227, 232	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)})
234		fveq2 6886	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤))
235	234	cbvesumv 34722	. . . . . . . . . . . . 13 ⊢ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤)
236		esumeq1 34713	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∪ ran 𝑔 → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤))
237	236	rspceeqv 3598	. . . . . . . . . . . . 13 ⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
238	233, 235, 237	sylancl 598	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
239		esumex 34708	. . . . . . . . . . . . 13 ⊢ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V
240		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
241	240	elrnmpt 5939	. . . . . . . . . . . . 13 ⊢ (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)))
242	239, 241	ax-mp 5	. . . . . . . . . . . 12 ⊢ (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))
243	238, 242	sylibr 237	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)))
244	103	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → < Or (0[,]+∞))
245		omscl 34974	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
246	14, 13, 158, 245	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
247		xrge0infss 33399	. . . . . . . . . . . . . 14 ⊢ (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < 𝑡)))
248	246, 247	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < 𝑡)))
249	244, 248	inflb 9486	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < )))
250	35	fveq1i 6887	. . . . . . . . . . . . . . 15 ⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴)
251	42	iunssd 5008	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄)
252		omsfval 34973	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
253	14, 13, 251, 252	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
254	250, 253	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
255	254	breq2d 5114	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < )))
256	255	notbid 321	. . . . . . . . . . . 12 ⊢ (𝜑 → (¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < )))
257	249, 256	sylibrd 262	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴)))
258	153, 243, 257	sylc 66	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴))
259	161, 185, 258	xrnltled 11382	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐))
260		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}
261	30, 260	nfan 1931	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
262		nfra1 3286	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
263	261, 262	nfan 1931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
264		simp-6l 799	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝜑)
265		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
266		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
267		fvex 6899	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑦) ∈ V
268	13	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
269		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
270		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋)
271	269, 270	ffvelcdmd 7086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
272	170, 271	sselid 3906	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅)
273	272	elpwid 4565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅)
274	268, 273	fssdmd 6729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄)
275		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦))
276	274, 275	sseldd 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄)
277	268, 276	ffvelcdmd 7086	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞))
278	277	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
279		nfcv 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑔‘𝑦)
280	279	esumcl 34709	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
281	267, 278, 280	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
282	264, 265, 266, 281	syl21anc 851	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
283	263, 282	ralrimia 3261	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
284	23	esumcl 34709	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
285	163, 283, 284	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
286	100, 285	sselid 3906	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ*)
287		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
288		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
289		fniunfv 7252	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn 𝑋 → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔)
290	288, 197, 289	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔)
291	287, 290	esumeq1d 34714	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ*𝑤 ∈ ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤))
292	11	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V)
293	267	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V)
294	292, 293, 277	esumiun 34773	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ*𝑤 ∈ ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
295	291, 294	eqbrtrrd 5128	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
296	295	ad5ant15 771	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
297	296	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
298	235, 297	eqbrtrid 5139	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
299	264, 266, 49	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
300	72	ad4ant14 765	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
301	299, 300	xrge0addcld 33401	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
302	263, 301	ralrimia 3261	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
303	23	esumcl 34709	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
304	163, 302, 303	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
305	100, 304	sselid 3906	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*)
306	199, 10	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V)
307	52	ad5ant15 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ)
308	307	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑀‘𝐴) ∈ ℝ)
309	65	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
310	309	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
311		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
312		rexadd 13366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
313	312	breq2d 5114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
314	313	biimpar 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))))
315	308, 310, 311, 314	syl21anc 851	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))))
316	315	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
317		simp-5l 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝜑)
318		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
319		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
320	317, 318, 319, 281	syl21anc 851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
321	100, 320	sselid 3906	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ*)
322	307	rexrd 11363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ*)
323	309	rexrd 11363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ*)
324	322, 323	xaddcld 13435	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*)
325		xrltle 13282	. . . . . . . . . . . . . . . . . 18 ⊢ ((Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ* ∧ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
326	321, 324, 325	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
327	316, 326	syld 48	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
328	327	adantld 496	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
329	261, 328	ralimdaa 3263	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦))))))
330	329	imp 412	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))))
331	330	r19.21bi 3254	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))))
332	263, 23, 306, 282, 301, 331	esumlef 34741	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))))
333	153, 49	sylan 592	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
334	263, 23, 306, 333, 300	esumaddf 34740	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))))
335	263, 300	ralrimia 3261	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
336	23	esumcl 34709	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
337	163, 335, 336	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
338	100, 337	sselid 3906	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ*)
339		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋–1-1→ℕ)
340		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑓 ∈ V
341	340	rnex 7923	. . . . . . . . . . . . . . . . . 18 ⊢ ran 𝑓 ∈ V
342	58	frnd 6719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 ⊆ ℕ)
343	342	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
344	343	sselda 3908	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
345	55	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
346		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
347	346	nnzd 12723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
348	345, 347	rpexpcld 14395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
349	348	rpreccld 13178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
350	70, 349	sselid 3906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
351	350	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
352	344, 351	syldan 603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
353	352	ralrimiva 3154	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
354		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑧ran 𝑓
355	354	esumcl 34709	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
356	341, 353, 355	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
357	100, 356	sselid 3906	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
358		1xr 11372	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
359	358	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
360	70	sseli 3904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ ℝ+ → 𝑒 ∈ (0[,]+∞))
361	360	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
362		elxrge0 13592	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
363	361, 362	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
364		nfv 1946	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋–1-1→ℕ)
365		nnex 12345	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ∈ V
366	365	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℕ ∈ V)
367	364, 366, 350, 342	esummono 34733	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
368		oveq2 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
369	368	oveq2d 7437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
370		ioossico 13573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0(,)+∞) ⊆ (0[,)+∞)
371	68, 370	eqsstri 3954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ+ ⊆ (0[,)+∞)
372	371, 349	sselid 3906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
373		eqidd 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
374		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
375	374	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
376	375	oveq2d 7437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
377		id 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
378		ovexd 7456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
379	373, 376, 377, 378	fvmptd 7002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
380	379	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
381		ax-1cn 11262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
382		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
383	382	geo2lim 16050	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℂ → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
384	381, 383	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
385		1red 11313	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 1 ∈ ℝ)
386	369, 372, 380, 384, 385	esumcvgsum 34767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
387		geoihalfsum 16057	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
388	386, 387	eqtrdi 2811	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
389	367, 388	breqtrd 5130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
390	389	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
391		xlemul2a 13423	. . . . . . . . . . . . . . . 16 ⊢ (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
392	357, 359, 363, 390, 391	syl31anc 1400	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
393	54	rpcnd 13170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ)
394	61	rpcnd 13170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ)
395	394	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ)
396		2cnd 12425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ)
397		2ne0 12453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
398	397	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0)
399	396, 398, 60	expne0d 14299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0)
400	399	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0)
401	393, 395, 400	divrecd 12100	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦)))))
402	61	rpreccld 13178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ+)
403	402	rpred 13168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ)
404	403	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ)
405		rexmul 13405	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦)))))
406	82, 404, 405	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦)))))
407	401, 406	eqtr4d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))))
408	407	esumeq2dv 34717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦)))))
409	11	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
410	70, 402	sselid 3906	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
411	410	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
412	371	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
413	412	sselda 3908	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
414	409, 411, 413	esummulc2 34761	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦)))))
415		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(1 / (2↑𝑧))
416		nfv 1946	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋–1-1→ℕ)
417		oveq2 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦)))
418	417	oveq2d 7437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦))))
419	11	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑋 ∈ V)
420		df-f1 6544	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋–1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ◡𝑓))
421	420	simprbi 503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡𝑓)
422	57	feqmptd 6954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:𝑋–1-1→ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
423	422	cnveqd 5852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋–1-1→ℕ → ◡𝑓 = ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
424	423	funeqd 6562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑋–1-1→ℕ → (Fun ◡𝑓 ↔ Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))))
425	421, 424	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
426	425	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
427	415, 416, 23, 418, 419, 426, 410, 59	esumc 34730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧)))
428		ffn 6710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
429		fnrnfv 6945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)})
430	58, 428, 429	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)})
431	364, 430	esumeq1d 34714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧)))
432	427, 431	eqtr4d 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
433	432	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
434	433	oveq2d 7437	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
435	408, 414, 434	3eqtr2rd 2802	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))))
436	363	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
437		xmulrid 13413	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
438	436, 437	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
439	392, 435, 438	3brtr3d 5135	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒)
440	153, 339, 188, 439	syl21anc 851	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒)
441		xleadd2a 13388	. . . . . . . . . . . . 13 ⊢ (((Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ* ∧ 𝑒 ∈ ℝ* ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ*) ∧ Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
442	338, 189, 187, 440, 441	syl31anc 1400	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
443	334, 442	eqbrtrd 5126	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +e (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
444	286, 305, 190, 332, 443	xrletrd 13295	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
445	185, 286, 190, 298, 444	xrletrd 13295	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
446	161, 185, 190, 259, 445	xrletrd 13295	. . . . . . . 8 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒))
447	188	rpred 13168	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ)
448	186, 447	rexaddd 13368	. . . . . . . 8 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +e 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
449	446, 448	breqtrd 5130	. . . . . . 7 ⊢ ((((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
450	449	anasss 472	. . . . . 6 ⊢ (((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
451	152, 450	exlimddv 1967	. . . . 5 ⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
452	451	ralrimiva 3154	. . . 4 ⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
453		xralrple 13339	. . . . . 6 ⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)))
454	160, 453	sylan 592	. . . . 5 ⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)))
455	454	adantr 486	. . . 4 ⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)))
456	452, 455	mpbird 260	. . 3 ⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))
457	8, 456	exlimddv 1967	. 2 ⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))
458	160	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ¬ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ*)
459	458	pnfged 13264	. . 3 ⊢ ((𝜑 ∧ ¬ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞)
460	49	ralrimiva 3154	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞))
461	23	esumcl 34709	. . . . 5 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞))
462	11, 460, 461	syl2anc 596	. . . 4 ⊢ (𝜑 → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞))
463		xrge0nre 13588	. . . 4 ⊢ ((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) = +∞)
464	462, 463	sylan 592	. . 3 ⊢ ((𝜑 ∧ ¬ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) = +∞)
465	459, 464	breqtrrd 5132	. 2 ⊢ ((𝜑 ∧ ¬ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))
466	457, 465	pm2.61dan 825	1 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895  𝒫 cpw 4556  ∪ cuni 4866  ∪ ciun 4950   class class class wbr 5102   ↦ cmpt 5185   Or wor 5557  ^◡ccnv 5649  dom cdm 5650  ran crn 5651  Fun wfun 6533   Fn wfn 6534  ⟶wf 6535  –1-1→wf1 6536  ‘cfv 6539  (class class class)co 7421  ωcom 7878   ≈ cen 8974   ≼ cdom 8975  infcinf 9437  ℂcc 11202  ℝcr 11203  0cc0 11204  1c1 11205   + caddc 11207   · cmul 11209  +∞cpnf 11344  ℝ^*cxr 11346   < clt 11347   ≤ cle 11348   / cdiv 11977  ℕcn 12339  2c2 12401  ℤcz 12697  ℝ⁺crp 13124   +_e cxad 13243   ·_e cxmu 13244  (,)cioo 13480  [,)cico 13482  [,]cicc 13483  seqcseq 14148  ↑cexp 14208   ⇝ cli 15657  Σcsu 15859  Σ^*cesum 34706  toOMeascoms 34970

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-inf2 9646  ax-cc 10517  ax-ac2 10545  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281  ax-pre-sup 11282  ax-addf 11283  ax-mulf 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-of 7694  df-om 7879  df-1st 8002  df-2nd 8003  df-supp 8181  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8721  df-map 8853  df-pm 8854  df-ixp 8930  df-en 8978  df-dom 8979  df-sdom 8980  df-fin 8981  df-fsupp 9358  df-fi 9407  df-sup 9438  df-inf 9439  df-oi 9508  df-card 10024  df-acn 10027  df-ac 10199  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-div 11978  df-nn 12340  df-2 12409  df-3 12410  df-4 12411  df-5 12412  df-6 12413  df-7 12414  df-8 12415  df-9 12416  df-n0 12611  df-xnn0 12684  df-z 12698  df-dec 12819  df-uz 12970  df-q 13080  df-rp 13125  df-xneg 13245  df-xadd 13246  df-xmul 13247  df-ioo 13484  df-ioc 13485  df-ico 13486  df-icc 13487  df-fz 13644  df-fzo 13793  df-fl 13936  df-mod 14014  df-seq 14149  df-exp 14209  df-fac 14422  df-bc 14451  df-hash 14479  df-shft 15226  df-cj 15272  df-re 15273  df-im 15274  df-sqrt 15408  df-abs 15409  df-limsup 15644  df-clim 15661  df-rlim 15662  df-sum 15860  df-ef 16239  df-sin 16241  df-cos 16242  df-pi 16244  df-struct 17331  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-ress 17415  df-plusg 17447  df-mulr 17448  df-starv 17449  df-sca 17450  df-vsca 17451  df-ip 17452  df-tset 17453  df-ple 17454  df-ds 17456  df-unif 17457  df-hom 17458  df-cco 17459  df-rest 17599  df-topn 17600  df-0g 17618  df-gsum 17619  df-topgen 17620  df-pt 17621  df-prds 17624  df-ordt 17679  df-xrs 17680  df-qtop 17685  df-imas 17686  df-xps 17688  df-mre 17762  df-mrc 17763  df-acs 17765  df-ps 18746  df-tsr 18747  df-plusf 18821  df-mgm 18822  df-sgrp 18914  df-mnd 18930  df-mhm 18984  df-submnd 18985  df-grp 19153  df-minusg 19154  df-sbg 19155  df-mulg 19284  df-subg 19339  df-cntz 19537  df-cmn 20002  df-abl 20003  df-mgp 20367  df-rng 20381  df-ur 20414  df-ring 20467  df-cring 20468  df-subrng 20804  df-subrg 20828  df-abv 21072  df-lmod 21143  df-scaf 21144  df-sra 21454  df-rgmod 21455  df-psmet 21676  df-xmet 21677  df-met 21678  df-bl 21679  df-mopn 21680  df-fbas 21681  df-fg 21682  df-cnfld 21685  df-top 23218  df-topon 23235  df-topsp 23257  df-bases 23270  df-cld 23343  df-ntr 23344  df-cls 23345  df-nei 23422  df-lp 23460  df-perf 23461  df-cn 23551  df-cnp 23552  df-haus 23639  df-tx 23887  df-hmeo 24080  df-fil 24171  df-fm 24263  df-flim 24264  df-flf 24265  df-tmd 24397  df-tgp 24398  df-tsms 24452  df-trg 24485  df-xms 24645  df-ms 24646  df-tms 24647  df-nm 24907  df-ngp 24908  df-nrg 24910  df-nlm 24911  df-ii 25204  df-cncf 25205  df-limc 26192  df-dv 26193  df-log 26890  df-esum 34707  df-oms 34971

This theorem is used by:  omsmeas  35002