omssubadd - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > omssubadd		Structured version Visualization version GIF version

Theorem omssubadd 35015

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 9616. (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 14153	. . . . . . 7 ⊢ ℕ ≈ ω
3		domen2 9170	. . . . . . 7 ⊢ (ℕ ≈ ω → (𝑋 ≼ ℕ ↔ 𝑋 ≼ ω))
4	2, 3	ax-mp 5	. . . . . 6 ⊢ (𝑋 ≼ ℕ ↔ 𝑋 ≼ ω)
5	1, 4	sylibr 237	. . . . 5 ⊢ (𝜑 → 𝑋 ≼ ℕ)
6		brdomi 9017	. . . . 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 9021	. . . . . . . . 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 7259	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ V)
16		dmexg 7940	. . . . . . . . . 10 ⊢ (𝑅 ∈ V → dom 𝑅 ∈ V)
17		pwexg 5345	. . . . . . . . . 10 ⊢ (dom 𝑅 ∈ V → 𝒫 dom 𝑅 ∈ V)
18	15, 16, 17	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 dom 𝑅 ∈ V)
19		rabexg 5304	. . . . . . . . 9 ⊢ (𝒫 dom 𝑅 ∈ V → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
20	18, 19	syl 18	. . . . . . . 8 ⊢ (𝜑 → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
21	20	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V)
22		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝜑
23		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑋
24	23	nfesum1 34755	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴)
25	24	nfel1 2942	. . . . . . . . . . 11 ⊢ Ⅎ𝑦Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ
26	22, 25	nfan 1934	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
27		nfv 1949	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑓:𝑋⟶1-1ℕ
28	26, 27	nfan 1934	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ)
29		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑒 ∈ ℝ⁺
30	28, 29	nfan 1934	. . . . . . . 8 ⊢ Ⅎ𝑦(((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺)
31	9	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝜑)
32		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
33	11	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V)
34		omsf 35011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞))
35		oms.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑀 = (toOMeas‘𝑅)
36	35	feq1i 6725	. . . . . . . . . . . . . . . . . . . 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 7786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ 𝑄 ∈ V)
41	40	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V)
42		omssubadd.a	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄)
43	41, 42	ssexd 5291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V)
44	13	fdmd 6745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → dom 𝑅 = 𝑄)
45	44	unieqd 4883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄)
46	45	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom 𝑅 = ∪ 𝑄)
47	42, 46	sseqtrrd 3950	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom 𝑅)
48	43, 47	elpwd 4566	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅)
49	39, 48	ffvelcdmd 7112	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
50	49	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
51		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
52	26, 33, 50, 51	esumcvgre 34806	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ)
53	52	ad4ant14 765	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ)
54		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ⁺)
55		2rp 13155	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ⁺
56	55	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ⁺)
57		f1f 6803	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑋⟶1-1ℕ → 𝑓:𝑋⟶ℕ)
58	57	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → 𝑓:𝑋⟶ℕ)
59	58	ffvelcdmda 7111	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ)
60	59	nnzd 12749	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
61	56, 60	rpexpcld 14421	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ⁺)
62	61	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ⁺)
63	54, 62	rpdivcld 13211	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ⁺)
64	63	rpred 13194	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
65	64	adantl3r 763	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ)
66	53, 65	rexaddd 13394	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
67	49	ad5ant15 771	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞))
68		dfrp2 13555	. . . . . . . . . . . . . . . 16 ⊢ ℝ⁺ = (0(,)+∞)
69		ioossicc 13594	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) ⊆ (0[,]+∞)
70	68, 69	eqsstri 3959	. . . . . . . . . . . . . . 15 ⊢ ℝ⁺ ⊆ (0[,]+∞)
71	70, 63	sselid 3911	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
72	71	adantl3r 763	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
73	67, 72	xrge0addcld 33427	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
74	66, 73	eqeltrrd 2865	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
75	35	fveq1i 6912	. . . . . . . . . . . . . 14 ⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴)
76	14	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉)
77	13	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞))
78		omsfval 35009	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
79	76, 77, 42, 78	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
80	75, 79	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
81	80	ad5ant15 771	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
82	54	rpred 13194	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ)
83	82	adantl3r 763	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ)
84	61	rpred 13194	. . . . . . . . . . . . . . . 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 13197	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒)
89		2re 12447	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90	60	adantllr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
91	90	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ)
92		2pos 12477	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
93	92	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 0 < 2)
94		expgt0 14268	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓‘𝑦)))
95	89, 91, 93, 94	mp3an2i 1496	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦)))
96	83, 86, 88, 95	divgt0d 12282	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦))))
97	65, 53	ltaddposd 11930	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
98	96, 97	mpbid 235	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
99	81, 98	eqbrtrrd 5133	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
100		iccssxr 13591	. . . . . . . . . . . . . . 15 ⊢ (0[,]+∞) ⊆ ℝ^*
101		xrltso 13300	. . . . . . . . . . . . . . 15 ⊢ < Or ℝ^*
102		soss 5584	. . . . . . . . . . . . . . 15 ⊢ ((0[,]+∞) ⊆ ℝ^* → ( < Or ℝ^* → < Or (0[,]+∞)))
103	100, 101, 102	mp2 9	. . . . . . . . . . . . . 14 ⊢ < Or (0[,]+∞)
104	103	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or (0[,]+∞))
105		omscl 35010	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
106	76, 77, 48, 105	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
107		xrge0infss 33425	. . . . . . . . . . . . . 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 9513	. . . . . . . . . . . 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 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))
113		esumex 34744	. . . . . . . . . . . . . . . 16 ⊢ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤) ∈ V
114	112, 113	elrnmpti 5952	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))
115	114	anbi1i 636	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
116		r19.41v 3196	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
117	115, 116	bitr4i 281	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
118	117	exbii 1881	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
119		df-rex 3091	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
120		rexcom4 3293	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
121	118, 119, 120	3bitr4i 306	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
122		breq1 5109	. . . . . . . . . . . . . 14 ⊢ (𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
123	122	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
124	123	exlimiv 1965	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑢 = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
125	124	reximi 3104	. . . . . . . . . . 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 4004	. . . . . . . . . . 11 ⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}
131		rexss 3987	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
132	130, 131	ax-mp 5	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
133		unieq 4881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪ 𝑥)
134	133	sseq2d 3945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥))
135		breq1 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
136	134, 135	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)))
137	136	elrab 3648	. . . . . . . . . . . . . . 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 3181	. . . . . . . . . 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 3265	. . . . . . 7 ⊢ ((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
146		unieq 4881	. . . . . . . . . 10 ⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪ (𝑔‘𝑦))
147	146	sseq2d 3945	. . . . . . . . 9 ⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦)))
148		esumeq1 34749	. . . . . . . . . 10 ⊢ (𝑥 = (𝑔‘𝑦) → Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
149	148	breq1d 5116	. . . . . . . . 9 ⊢ (𝑥 = (𝑔‘𝑦) → (Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))
150	147, 149	anbi12d 644	. . . . . . . 8 ⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
151	150	ac6 10588	. . . . . . 7 ⊢ ((𝑋 ∈ V ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
152	12, 21, 145, 151	syl3anc 1399	. . . . . 6 ⊢ ((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))
153		simp-5l 797	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑)
154	43	ralrimiva 3158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V)
155		iunexg 8002	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V)
156	11, 154, 155	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V)
157	47	iunssd 5012	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom 𝑅)
158	156, 157	elpwd 4566	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅)
159	38, 158	ffvelcdmd 7112	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞))
160	100, 159	sselid 3911	. . . . . . . . . 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 7259	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V)
165		rnexg 7941	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ V → ran 𝑔 ∈ V)
166		uniexg 7784	. . . . . . . . . . . 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 6742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
170		ssrab2 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
171	169, 170	sstrdi 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
172	171	unissd 4880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪ 𝒫 dom 𝑅)
173		unipw 5423	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅
174	172, 173	sseqtrdi 3953	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅)
175	174	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅)
176	44	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
177	175, 176	sseqtrd 3949	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄)
178	177	sselda 3913	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran 𝑔) → 𝑐 ∈ 𝑄)
179	168, 178	ffvelcdmd 7112	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran 𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞))
180	179	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
181	153, 162, 180	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
182		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∪ ran 𝑔
183	182	esumcl 34745	. . . . . . . . . . 11 ⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) → Σ^*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
184	167, 181, 183	syl2anc 596	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞))
185	100, 184	sselid 3911	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ^)
186		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)
187	186	rexrd 11389	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ^)
188		simpllr 788	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ⁺)
189	188	rpxrd 13195	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ^*)
190	187, 189	xaddcld 13461	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒) ∈ ℝ^)
191	169	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
192		sstr 3921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
193	170, 192	mpan2 704	. . . . . . . . . . . . . . . . . 18 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
194		sspwuni 5063	. . . . . . . . . . . . . . . . . 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 6734	. . . . . . . . . . . . . . . . . . 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 10650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω)
201		rnct 10634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ≼ ω → ran 𝑔 ≼ ω)
202	200, 201	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼ ω)
203		dfss3 3902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
204		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
205	204	elrab 3648	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω))
206	205	simprbi 503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω)
207	206	ralimi 3103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
208	203, 207	sylbi 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
209		unictb 10690	. . . . . . . . . . . . . . . . . . 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 9021	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V)
213		elpwg 4563	. . . . . . . . . . . . . . . . 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 3103	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦))
218		fvssunirn 6942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔‘𝑦) ⊆ ∪ ran 𝑔
219	218	unissi 4879	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔
220		sstr 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔)
221	219, 220	mpan2 704	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔)
222	221	ralimi 3103	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)
223		iunss 5006	. . . . . . . . . . . . . . . . . 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 4881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∪ ran 𝑔 → ∪ 𝑧 = ∪ ∪ ran 𝑔)
229	228	sseq2d 3945	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∪ ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔))
230		breq1 5109	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∪ ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω))
231	229, 230	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∪ ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼ ω)))
232	231	elrab 3648	. . . . . . . . . . . . . 14 ⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼ ω)))
233	227, 232	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)})
234		fveq2 6911	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤))
235	234	cbvesumv 34758	. . . . . . . . . . . . 13 ⊢ Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ^𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤)
236		esumeq1 34749	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∪ ran 𝑔 → Σ^𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ^𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤))
237	236	rspceeqv 3602	. . . . . . . . . . . . 13 ⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧ Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ^𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))
238	233, 235, 237	sylancl 598	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))
239		esumex 34744	. . . . . . . . . . . . 13 ⊢ Σ^*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V
240		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤))
241	240	elrnmpt 5948	. . . . . . . . . . . . 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 35010	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
246	14, 13, 158, 245	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞))
247		xrge0infss 33425	. . . . . . . . . . . . . 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 9512	. . . . . . . . . . . 12 ⊢ (𝜑 → (Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)) → ¬ Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < )))
250	35	fveq1i 6912	. . . . . . . . . . . . . . 15 ⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴)
251	42	iunssd 5012	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄)
252		omsfval 35009	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
253	14, 13, 251, 252	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
254	250, 253	eqtrid 2810	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ^*𝑤 ∈ 𝑥(𝑅‘𝑤)), (0[,]+∞), < ))
255	254	breq2d 5118	. . . . . . . . . . . . 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 11408	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ^*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐))
260		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}
261	30, 260	nfan 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((((𝜑 ∧ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
262		nfra1 3290	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
263	261, 262	nfan 1934	. . . . . . . . . . . . 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 6924	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑦) ∈ V
268	13	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
269		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
270		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋)
271	269, 270	ffvelcdmd 7112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
272	170, 271	sselid 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅)
273	272	elpwid 4569	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅)
274	268, 273	fssdmd 6753	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄)
275		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦))
276	274, 275	sseldd 3914	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄)
277	268, 276	ffvelcdmd 7112	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞))
278	277	ralrimiva 3158	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
279		nfcv 2926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤(𝑔‘𝑦)
280	279	esumcl 34745	. . . . . . . . . . . . . . 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 3265	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
284	23	esumcl 34745	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) → Σ^𝑦 ∈ 𝑋Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
285	163, 283, 284	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))
286	100, 285	sselid 3911	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ^*)
287		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
288		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω})
289		fniunfv 7277	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 Fn 𝑋 → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔)
290	288, 197, 289	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔)
291	287, 290	esumeq1d 34750	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ^𝑤 ∈ ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ^𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤))
292	11	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V)
293	267	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V)
294	292, 293, 277	esumiun 34809	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → Σ^𝑤 ∈ ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ^𝑦 ∈ 𝑋Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤))
295	291, 294	eqbrtrrd 5133	. . . . . . . . . . . . 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 5144	. . . . . . . . . 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 33427	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
302	263, 301	ralrimia 3265	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))
303	23	esumcl 34745	. . . . . . . . . . . . 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 3911	. . . . . . . . . . 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 13392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))
313	312	breq2d 5118	. . . . . . . . . . . . . . . . . . . 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 3911	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ^*)
322	307	rexrd 11389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ^)
323	309	rexrd 11389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ^)
324	322, 323	xaddcld 13461	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ^)
325		xrltle 13308	. . . . . . . . . . . . . . . . . 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 3267	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦))))))
330	329	imp 412	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))))
331	330	r19.21bi 3258	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ^*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))))
332	263, 23, 306, 282, 301, 331	esumlef 34777	. . . . . . . . . . 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 34776	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e Σ^*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))))
335	263, 300	ralrimia 3265	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
336	23	esumcl 34745	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) → Σ^*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
337	163, 335, 336	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))
338	100, 337	sselid 3911	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ^)
339		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋⟶1-1ℕ)
340		vex 3458	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑓 ∈ V
341	340	rnex 7949	. . . . . . . . . . . . . . . . . 18 ⊢ ran 𝑓 ∈ V
342	58	frnd 6743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → ran 𝑓 ⊆ ℕ)
343	342	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → ran 𝑓 ⊆ ℕ)
344	343	sselda 3913	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
345	55	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ⁺)
346		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
347	346	nnzd 12749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
348	345, 347	rpexpcld 14421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ⁺)
349	348	rpreccld 13204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ⁺)
350	70, 349	sselid 3911	. . . . . . . . . . . . . . . . . . . . 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 3158	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
354		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑧ran 𝑓
355	354	esumcl 34745	. . . . . . . . . . . . . . . . . 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 3911	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ^)
358		1xr 11398	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ^*
359	358	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → 1 ∈ ℝ^*)
360	70	sseli 3909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ ℝ⁺ → 𝑒 ∈ (0[,]+∞))
361	360	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ (0[,]+∞))
362		elxrge0 13618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ^* ∧ 0 ≤ 𝑒))
363	361, 362	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ∈ ℝ^* ∧ 0 ≤ 𝑒))
364		nfv 1949	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋⟶1-1ℕ)
365		nnex 12371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ∈ V
366	365	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → ℕ ∈ V)
367	364, 366, 350, 342	esummono 34769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ^𝑧 ∈ ℕ(1 / (2↑𝑧)))
368		oveq2 7454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
369	368	oveq2d 7462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
370		ioossico 13599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (0(,)+∞) ⊆ (0[,)+∞)
371	68, 370	eqsstri 3959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ⁺ ⊆ (0[,)+∞)
372	371, 349	sselid 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
373		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
374		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
375	374	oveq2d 7462	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
376	375	oveq2d 7462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
377		id 23	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
378		ovexd 7481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
379	373, 376, 377, 378	fvmptd 7027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
380	379	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
381		ax-1cn 11288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
382		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
383	382	geo2lim 16076	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℂ → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
384	381, 383	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
385		1red 11339	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → 1 ∈ ℝ)
386	369, 372, 380, 384, 385	esumcvgsum 34803	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
387		geoihalfsum 16083	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
388	386, 387	eqtrdi 2814	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
389	367, 388	breqtrd 5135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
390	389	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → Σ^*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
391		xlemul2a 13449	. . . . . . . . . . . . . . . 16 ⊢ (((Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ^ ∧ 1 ∈ ℝ^* ∧ (𝑒 ∈ ℝ^* ∧ 0 ≤ 𝑒)) ∧ Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·_e Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·_e 1))
392	357, 359, 363, 390, 391	syl31anc 1401	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ·_e Σ^*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·_e 1))
393	54	rpcnd 13196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ)
394	61	rpcnd 13196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ)
395	394	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ)
396		2cnd 12451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ)
397		2ne0 12479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
398	397	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0)
399	396, 398, 60	expne0d 14325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0)
400	399	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0)
401	393, 395, 400	divrecd 12126	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦)))))
402	61	rpreccld 13204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ⁺)
403	402	rpred 13194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ)
404	403	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ)
405		rexmul 13431	. . . . . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·_e (1 / (2↑(𝑓‘𝑦)))))
408	407	esumeq2dv 34753	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ^𝑦 ∈ 𝑋(𝑒 ·_e (1 / (2↑(𝑓‘𝑦)))))
409	11	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → 𝑋 ∈ V)
410	70, 402	sselid 3911	. . . . . . . . . . . . . . . . . 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 3913	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ (0[,)+∞))
414	409, 411, 413	esummulc2 34797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ·_e Σ^𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ^𝑦 ∈ 𝑋(𝑒 ·_e (1 / (2↑(𝑓‘𝑦)))))
415		nfcv 2926	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(1 / (2↑𝑧))
416		nfv 1949	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋⟶1-1ℕ)
417		oveq2 7454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦)))
418	417	oveq2d 7462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦))))
419	11	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → 𝑋 ∈ V)
420		df-f1 6566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶1-1ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ^◡𝑓))
421	420	simprbi 503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑋⟶1-1ℕ → Fun ^◡𝑓)
422	57	feqmptd 6979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓:𝑋⟶1-1ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
423	422	cnveqd 5861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓:𝑋⟶1-1ℕ → ^◡𝑓 = ^◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))
424	423	funeqd 6584	. . . . . . . . . . . . . . . . . . . . . 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 34766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ^𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧)))
428		ffn 6734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
429		fnrnfv 6970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)})
430	58, 428, 429	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)})
431	364, 430	esumeq1d 34750	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ^𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧)))
432	427, 431	eqtr4d 2801	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) → Σ^𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
433	432	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → Σ^𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
434	433	oveq2d 7462	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ·_e Σ^𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·_e Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
435	408, 414, 434	3eqtr2rd 2805	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ·_e Σ^𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))))
436	363	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ ℝ^*)
437		xmulrid 13439	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ ℝ^* → (𝑒 ·_e 1) = 𝑒)
438	436, 437	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑒 ·_e 1) = 𝑒)
439	392, 435, 438	3brtr3d 5140	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → Σ^*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒)
440	153, 339, 188, 439	syl21anc 851	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒)
441		xleadd2a 13414	. . . . . . . . . . . . 13 ⊢ (((Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ^ ∧ 𝑒 ∈ ℝ^* ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ^) ∧ Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
442	338, 189, 187, 440, 441	syl31anc 1401	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e Σ^𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
443	334, 442	eqbrtrd 5131	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋((𝑀‘𝐴) +_e (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
444	286, 305, 190, 332, 443	xrletrd 13321	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑦 ∈ 𝑋Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
445	185, 286, 190, 298, 444	xrletrd 13321	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ^𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
446	161, 185, 190, 259, 445	xrletrd 13321	. . . . . . . 8 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒))
447	188	rpred 13194	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ)
448	186, 447	rexaddd 13394	. . . . . . . 8 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) +_e 𝑒) = (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
449	446, 448	breqtrd 5135	. . . . . . 7 ⊢ ((((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
450	449	anasss 472	. . . . . 6 ⊢ (((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ^𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
451	152, 450	exlimddv 1970	. . . . 5 ⊢ ((((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) ∧ 𝑒 ∈ ℝ⁺) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
452	451	ralrimiva 3158	. . . 4 ⊢ (((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋⟶1-1ℕ) → ∀𝑒 ∈ ℝ⁺ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))
453		xralrple 13365	. . . . . 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 1970	. 2 ⊢ ((𝜑 ∧ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴))
458	160	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ¬ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ^)
459	458	pnfged 13290	. . 3 ⊢ ((𝜑 ∧ ¬ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞)
460	49	ralrimiva 3158	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞))
461	23	esumcl 34745	. . . . 5 ⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) → Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞))
462	11, 460, 461	syl2anc 596	. . . 4 ⊢ (𝜑 → Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞))
463		xrge0nre 13614	. . . 4 ⊢ ((Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴) = +∞)
464	462, 463	sylan 592	. . 3 ⊢ ((𝜑 ∧ ¬ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) = +∞)
465	459, 464	breqtrrd 5137	. 2 ⊢ ((𝜑 ∧ ¬ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ^𝑦 ∈ 𝑋(𝑀‘𝐴))
466	457, 465	pm2.61dan 825	1 ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ^*𝑦 ∈ 𝑋(𝑀‘𝐴))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2147 {cab 2741 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⊆ wss 3900 𝒫 cpw 4560 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5106 ↦ cmpt 5190 Or wor 5563 ^◡ccnv 5655 dom cdm 5656 ran crn 5657 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 ⟶1-1wf1 6558 ‘cfv 6561 (class class class)co 7446 ωcom 7904 ≈ cen 9001 ≼ cdom 9002 infcinf 9463 ℂcc 11228 ℝcr 11229 0cc0 11230 1c1 11231 + caddc 11233 · cmul 11235 +∞cpnf 11370 ℝ^*cxr 11372 < clt 11373 ≤ cle 11374 / cdiv 12003 ℕcn 12365 2c2 12427 ℤcz 12723 ℝ⁺crp 13150 +_e cxad 13269 ·_e cxmu 13270 (,)cioo 13506 [,)cico 13508 [,]cicc 13509 seqcseq 14174 ↑cexp 14234 ⇝ cli 15683 Σcsu 15885 Σ^*cesum 34742 toOMeascoms 35006

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cc 10543 ax-ac2 10571 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308 ax-addf 11309 ax-mulf 11310

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-supp 8208 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-oadd 8511 df-er 8748 df-map 8880 df-pm 8881 df-ixp 8957 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fsupp 9385 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9534 df-card 10050 df-acn 10053 df-ac 10225 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-9 12442 df-n0 12637 df-xnn0 12710 df-z 12724 df-dec 12845 df-uz 12996 df-q 13106 df-rp 13151 df-xneg 13271 df-xadd 13272 df-xmul 13273 df-ioo 13510 df-ioc 13511 df-ico 13512 df-icc 13513 df-fz 13670 df-fzo 13819 df-fl 13962 df-mod 14040 df-seq 14175 df-exp 14235 df-fac 14448 df-bc 14477 df-hash 14505 df-shft 15252 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-limsup 15670 df-clim 15687 df-rlim 15688 df-sum 15886 df-ef 16265 df-sin 16267 df-cos 16268 df-pi 16270 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-starv 17475 df-sca 17476 df-vsca 17477 df-ip 17478 df-tset 17479 df-ple 17480 df-ds 17482 df-unif 17483 df-hom 17484 df-cco 17485 df-rest 17625 df-topn 17626 df-0g 17644 df-gsum 17645 df-topgen 17646 df-pt 17647 df-prds 17650 df-ordt 17705 df-xrs 17706 df-qtop 17711 df-imas 17712 df-xps 17714 df-mre 17788 df-mrc 17789 df-acs 17791 df-ps 18772 df-tsr 18773 df-plusf 18847 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-mhm 19010 df-submnd 19011 df-grp 19179 df-minusg 19180 df-sbg 19181 df-mulg 19310 df-subg 19365 df-cntz 19564 df-cmn 20029 df-abl 20030 df-mgp 20394 df-rng 20408 df-ur 20441 df-ring 20494 df-cring 20495 df-subrng 20831 df-subrg 20855 df-abv 21099 df-lmod 21170 df-scaf 21171 df-sra 21481 df-rgmod 21482 df-psmet 21703 df-xmet 21704 df-met 21705 df-bl 21706 df-mopn 21707 df-fbas 21708 df-fg 21709 df-cnfld 21712 df-top 23245 df-topon 23262 df-topsp 23284 df-bases 23297 df-cld 23370 df-ntr 23371 df-cls 23372 df-nei 23449 df-lp 23487 df-perf 23488 df-cn 23578 df-cnp 23579 df-haus 23666 df-tx 23914 df-hmeo 24107 df-fil 24198 df-fm 24290 df-flim 24291 df-flf 24292 df-tmd 24424 df-tgp 24425 df-tsms 24479 df-trg 24512 df-xms 24672 df-ms 24673 df-tms 24674 df-nm 24934 df-ngp 24935 df-nrg 24937 df-nlm 24938 df-ii 25231 df-cncf 25232 df-limc 26219 df-dv 26220 df-log 26917 df-esum 34743 df-oms 35007

This theorem is used by: omsmeas 35038

W3C validator