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

Theorem omssubadd 31668
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.)
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.
StepHypRef Expression
1 omssubadd.b . . . . . 6 (𝜑𝑋 ≼ ω)
2 nnenom 13343 . . . . . . 7 ℕ ≈ ω
32ensymi 8542 . . . . . 6 ω ≈ ℕ
4 domentr 8551 . . . . . 6 ((𝑋 ≼ ω ∧ ω ≈ ℕ) → 𝑋 ≼ ℕ)
51, 3, 4sylancl 589 . . . . 5 (𝜑𝑋 ≼ ℕ)
6 brdomi 8503 . . . . 5 (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋1-1→ℕ)
75, 6syl 17 . . . 4 (𝜑 → ∃𝑓 𝑓:𝑋1-1→ℕ)
87adantr 484 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋1-1→ℕ)
9 simplll 774 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10 ctex 8507 . . . . . . . . . . 11 (𝑋 ≼ ω → 𝑋 ∈ V)
111, 10syl 17 . . . . . . . . . 10 (𝜑𝑋 ∈ V)
129, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13 nfv 1915 . . . . . . . . . . . . 13 𝑦𝜑
14 nfcv 2955 . . . . . . . . . . . . . . 15 𝑦𝑋
1514nfesum1 31409 . . . . . . . . . . . . . 14 𝑦Σ*𝑦𝑋(𝑀𝐴)
16 nfcv 2955 . . . . . . . . . . . . . 14 𝑦
1715, 16nfel 2969 . . . . . . . . . . . . 13 𝑦Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ
1813, 17nfan 1900 . . . . . . . . . . . 12 𝑦(𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
19 nfv 1915 . . . . . . . . . . . 12 𝑦 𝑓:𝑋1-1→ℕ
2018, 19nfan 1900 . . . . . . . . . . 11 𝑦((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ)
21 nfv 1915 . . . . . . . . . . 11 𝑦 𝑒 ∈ ℝ+
2220, 21nfan 1900 . . . . . . . . . 10 𝑦(((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
239adantr 484 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝜑)
24 simpr 488 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑦𝑋)
2511adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → 𝑋 ∈ V)
26 oms.o . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄𝑉)
27 oms.r . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅:𝑄⟶(0[,]+∞))
28 omsf 31664 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 = (toOMeas‘𝑅)
3029feq1i 6478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀:𝒫 dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
3128, 30sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3226, 27, 31syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3332adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 𝑄)
3527fdmd 6497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom 𝑅 = 𝑄)
3635unieqd 4814 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 dom 𝑅 = 𝑄)
3736adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → dom 𝑅 = 𝑄)
3834, 37sseqtrrd 3956 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → 𝐴 dom 𝑅)
3926uniexd 7448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 𝑄 ∈ V)
4039adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑋) → 𝑄 ∈ V)
41 ssexg 5191 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 𝑄 𝑄 ∈ V) → 𝐴 ∈ V)
4234, 40, 41syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 ∈ V)
43 elpwg 4500 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ V → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4538, 44mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝐴 ∈ 𝒫 dom 𝑅)
4633, 45ffvelrnd 6829 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
4746adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
48 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
4918, 25, 47, 48esumcvgre 31460 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5049adantlr 714 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5150adantlr 714 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
52 rpssre 12384 . . . . . . . . . . . . . . . . . . 19 + ⊆ ℝ
53 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
54 2rp 12382 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ+
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℝ+)
56 df-f1 6329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun 𝑓))
5756simplbi 501 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → 𝑓:𝑋⟶ℕ)
5857adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑓:𝑋⟶ℕ)
5958ffvelrnda 6828 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℕ)
6059nnzd 12074 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
6155, 60rpexpcld 13604 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6261adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6353, 62rpdivcld 12436 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ+)
6452, 63sseldi 3913 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
6564adantl3r 749 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
66 rexadd 12613 . . . . . . . . . . . . . . . . 17 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
6751, 65, 66syl2anc 587 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
689, 46sylan 583 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
69 dfrp2 30517 . . . . . . . . . . . . . . . . . . . 20 + = (0(,)+∞)
70 ioossicc 12811 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
7169, 70eqsstri 3949 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
7271, 63sseldi 3913 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7372adantl3r 749 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7468, 73xrge0addcld 30512 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7567, 74eqeltrrd 2891 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7652, 53sseldi 3913 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7776adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7852, 61sseldi 3913 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
7978adantlr 714 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8079adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
81 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
8281rpgt0d 12422 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 𝑒)
83 2re 11699 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 2 ∈ ℝ)
8560adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
8685adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
87 2pos 11728 . . . . . . . . . . . . . . . . . . . 20 0 < 2
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 2)
89 expgt0 13458 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ (𝑓𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓𝑦)))
9084, 86, 88, 89syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (2↑(𝑓𝑦)))
9177, 80, 82, 90divgt0d 11564 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (𝑒 / (2↑(𝑓𝑦))))
9265, 51ltaddposd 11213 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (0 < (𝑒 / (2↑(𝑓𝑦))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
9391, 92mpbid 235 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
9429fveq1i 6646 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝐴) = ((toOMeas‘𝑅)‘𝐴)
9526adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑄𝑉)
9627adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑅:𝑄⟶(0[,]+∞))
97 omsfval 31662 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9895, 96, 34, 97syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9994, 98syl5eq 2845 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
1009, 99sylan 583 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
101100eqcomd 2804 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) = (𝑀𝐴))
102101breq1d 5040 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
10393, 102mpbird 260 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
10475, 103jca 515 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
105 iccssxr 12808 . . . . . . . . . . . . . . . . . . 19 (0[,]+∞) ⊆ ℝ*
106 xrltso 12522 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
107 soss 5457 . . . . . . . . . . . . . . . . . . 19 ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
108105, 106, 107mp2 9 . . . . . . . . . . . . . . . . . 18 < Or (0[,]+∞)
109 biid 264 . . . . . . . . . . . . . . . . . 18 ( < Or (0[,]+∞) ↔ < Or (0[,]+∞))
110108, 109mpbi 233 . . . . . . . . . . . . . . . . 17 < Or (0[,]+∞)
111110a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → < Or (0[,]+∞))
112 omscl 31663 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
11395, 96, 45, 112syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
114 xrge0infss 30510 . . . . . . . . . . . . . . . . 17 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
115113, 114syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
116111, 115infglb 8938 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → ((((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
117116imp 410 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑋) ∧ (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
11823, 24, 104, 117syl21anc 836 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
119 eqid 2798 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
120 esumex 31398 . . . . . . . . . . . . . . . . . . 19 Σ*𝑤𝑥(𝑅𝑤) ∈ V
121119, 120elrnmpti 5796 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤))
122121anbi1i 626 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
123 r19.41v 3300 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
124122, 123bitr4i 281 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
125124exbii 1849 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
126 df-rex 3112 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
127 rexcom4 3212 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
128125, 126, 1273bitr4i 306 . . . . . . . . . . . . . 14 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
129 breq1 5033 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
130 idd 24 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
131129, 130sylbid 243 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
132131imp 410 . . . . . . . . . . . . . . . 16 ((𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
133132exlimiv 1931 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
134133reximi 3206 . . . . . . . . . . . . . 14 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
135128, 134sylbi 220 . . . . . . . . . . . . 13 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
136118, 135syl 17 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
137 simpr 488 . . . . . . . . . . . . . . . 16 ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω)
138137a1i 11 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω))
139138ss2rabi 4004 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
140 rexss 3986 . . . . . . . . . . . . . 14 ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
141139, 140ax-mp 5 . . . . . . . . . . . . 13 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
142 unieq 4811 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 𝑧 = 𝑥)
143142sseq2d 3947 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐴 𝑧𝐴 𝑥))
144 breq1 5033 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
145143, 144anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝐴 𝑧𝑧 ≼ ω) ↔ (𝐴 𝑥𝑥 ≼ ω)))
146145elrab 3628 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 𝑥𝑥 ≼ ω)))
147146simprbi 500 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → (𝐴 𝑥𝑥 ≼ ω))
148147simpld 498 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥)
149148a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥))
150149anim1d 613 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
151150reximdv 3232 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
152141, 151syl5bi 245 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
153136, 152mpd 15 . . . . . . . . . . 11 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
154153ex 416 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
15522, 154ralrimi 3180 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
156 unieq 4811 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → 𝑥 = (𝑔𝑦))
157156sseq2d 3947 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (𝐴 𝑥𝐴 (𝑔𝑦)))
158 esumeq1 31403 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
159158breq1d 5040 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
160157, 159anbi12d 633 . . . . . . . . . . 11 (𝑥 = (𝑔𝑦) → ((𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
161160ac6sg 9899 . . . . . . . . . 10 (𝑋 ∈ V → (∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))))
162161imp 410 . . . . . . . . 9 ((𝑋 ∈ V ∧ ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
16312, 155, 162syl2anc 587 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
1649ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
16538ralrimiva 3149 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦𝑋 𝐴 dom 𝑅)
166 iunss 4932 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀𝑦𝑋 𝐴 dom 𝑅)
167165, 166sylibr 237 . . . . . . . . . . . . . . . . 17 (𝜑 𝑦𝑋 𝐴 dom 𝑅)
16842ralrimiva 3149 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦𝑋 𝐴 ∈ V)
169 iunexg 7646 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 𝐴 ∈ V) → 𝑦𝑋 𝐴 ∈ V)
17011, 168, 169syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑦𝑋 𝐴 ∈ V)
171 elpwg 4500 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
172170, 171syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
173167, 172mpbird 260 . . . . . . . . . . . . . . . 16 (𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅)
17432, 173ffvelrnd 6829 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ (0[,]+∞))
175105, 174sseldi 3913 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
176164, 175syl 17 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
177 simplr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
17825ad4antr 731 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
179 fex 6966 . . . . . . . . . . . . . . . . 17 ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ 𝑋 ∈ V) → 𝑔 ∈ V)
180177, 178, 179syl2anc 587 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 ∈ V)
181 rnexg 7595 . . . . . . . . . . . . . . . 16 (𝑔 ∈ V → ran 𝑔 ∈ V)
182 uniexg 7446 . . . . . . . . . . . . . . . 16 (ran 𝑔 ∈ V → ran 𝑔 ∈ V)
183180, 181, 1823syl 18 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ V)
184 simp-5l 784 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
18527ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
186 frn 6493 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
187 ssrab2 4007 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
188186, 187sstrdi 3927 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
189188unissd 4810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 𝒫 dom 𝑅)
190 unipw 5308 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 dom 𝑅 = dom 𝑅
191189, 190sseqtrdi 3965 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
192191adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ⊆ dom 𝑅)
19335adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
194192, 193sseqtrd 3955 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔𝑄)
195194sselda 3915 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑐𝑄)
196185, 195ffvelrnd 6829 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → (𝑅𝑐) ∈ (0[,]+∞))
197196ralrimiva 3149 . . . . . . . . . . . . . . . 16 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
198184, 177, 197syl2anc 587 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
199 nfcv 2955 . . . . . . . . . . . . . . . 16 𝑐 ran 𝑔
200199esumcl 31399 . . . . . . . . . . . . . . 15 (( ran 𝑔 ∈ V ∧ ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
201183, 198, 200syl2anc 587 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
202105, 201sseldi 3913 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*)
203 simp-5r 785 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
204203rexrd 10680 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*)
205 simpllr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ+)
206205rpxrd 12420 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ*)
207204, 206xaddcld 12682 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) ∈ ℝ*)
208186ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
209 sstr 3923 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
210187, 209mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
211 sspwuni 4985 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅)
212210, 211sylib 221 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
213208, 212syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ dom 𝑅)
214 ffn 6487 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑔 Fn 𝑋)
215214ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 Fn 𝑋)
216164, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ≼ ω)
217 fnct 9948 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 Fn 𝑋𝑋 ≼ ω) → 𝑔 ≼ ω)
218 rnct 9936 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 ≼ ω → ran 𝑔 ≼ ω)
219217, 218syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 Fn 𝑋𝑋 ≼ ω) → ran 𝑔 ≼ ω)
220 dfss3 3903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
221220biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
222 breq1 5033 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
223222elrab 3628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω))
224223simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑤 ≼ ω)
225224ralimi 3128 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
226221, 225syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
227 unictb 9986 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ran 𝑔 ≼ ω)
228219, 226, 227syl2an 598 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn 𝑋𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ≼ ω)
229215, 216, 208, 228syl21anc 836 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ≼ ω)
230 ctex 8507 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V)
231 elpwg 4500 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ∈ V → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
232229, 230, 2313syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
233213, 232mpbird 260 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ 𝒫 dom 𝑅)
234 simpl 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝐴 (𝑔𝑦))
235234ralimi 3128 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 𝐴 (𝑔𝑦))
236 fvssunirn 6674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔𝑦) ⊆ ran 𝑔
237236unissi 4809 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔𝑦) ⊆ ran 𝑔
238 sstr 3923 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 (𝑔𝑦) ∧ (𝑔𝑦) ⊆ ran 𝑔) → 𝐴 ran 𝑔)
239237, 238mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 (𝑔𝑦) → 𝐴 ran 𝑔)
240239ralimi 3128 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑋 𝐴 (𝑔𝑦) → ∀𝑦𝑋 𝐴 ran 𝑔)
241 iunss 4932 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑦𝑋 𝐴 ran 𝑔 ↔ ∀𝑦𝑋 𝐴 ran 𝑔)
242240, 241sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 𝐴 (𝑔𝑦) → 𝑦𝑋 𝐴 ran 𝑔)
243235, 242syl 17 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝑦𝑋 𝐴 ran 𝑔)
244243adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑦𝑋 𝐴 ran 𝑔)
245233, 244, 229jca32 519 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
246 unieq 4811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ran 𝑔 𝑧 = ran 𝑔)
247246sseq2d 3947 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔))
248 breq1 5033 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → (𝑧 ≼ ω ↔ ran 𝑔 ≼ ω))
249247, 248anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ran 𝑔 → (( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
250249elrab 3628 . . . . . . . . . . . . . . . . . . 19 ( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
251245, 250sylibr 237 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)})
252 fveq2 6645 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑤 → (𝑅𝑐) = (𝑅𝑤))
253252cbvesumv 31412 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)
254 esumeq1 31403 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝑔 → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
255254rspceeqv 3586 . . . . . . . . . . . . . . . . . 18 (( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
256251, 253, 255sylancl 589 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
257 esumex 31398 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ V
258 eqid 2798 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
259258elrnmpt 5792 . . . . . . . . . . . . . . . . . 18 *𝑐 ran 𝑔(𝑅𝑐) ∈ V → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤)))
260257, 259ax-mp 5 . . . . . . . . . . . . . . . . 17 *𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
261256, 260sylibr 237 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)))
262110a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → < Or (0[,]+∞))
263 omscl 31663 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
26426, 27, 173, 263syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
265 xrge0infss 30510 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
266264, 265syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
267262, 266inflb 8937 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
26829fveq1i 6646 . . . . . . . . . . . . . . . . . . . 20 (𝑀 𝑦𝑋 𝐴) = ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴)
269167, 36sseqtrd 3955 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝑦𝑋 𝐴 𝑄)
270 omsfval 31662 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 𝑄) → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
27126, 27, 269, 270syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
272268, 271syl5eq 2845 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
273272breq2d 5042 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
274273notbid 321 . . . . . . . . . . . . . . . . 17 (𝜑 → (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
275267, 274sylibrd 262 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
276164, 261, 275sylc 65 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
277 biid 264 . . . . . . . . . . . . . . 15 (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
278276, 277sylib 221 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
279 xrlenlt 10695 . . . . . . . . . . . . . . 15 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
280176, 202, 279syl2anc 587 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
281278, 280mpbird 260 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐))
282 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
28322, 282nfan 1900 . . . . . . . . . . . . . . . . . 18 𝑦((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
284 nfra1 3183 . . . . . . . . . . . . . . . . . 18 𝑦𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
285283, 284nfan 1900 . . . . . . . . . . . . . . . . 17 𝑦(((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
286 simp-6l 786 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝜑)
287 simpllr 775 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
288 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑦𝑋)
28927ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
290 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
291 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑦𝑋)
292290, 291ffvelrnd 6829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
293187, 292sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ 𝒫 dom 𝑅)
294293elpwid 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ dom 𝑅)
295289, 294fssdmd 6503 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ 𝑄)
296 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤 ∈ (𝑔𝑦))
297295, 296sseldd 3916 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤𝑄)
298289, 297ffvelrnd 6829 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑅𝑤) ∈ (0[,]+∞))
299298ralrimiva 3149 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
300 fvex 6658 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑦) ∈ V
301 nfcv 2955 . . . . . . . . . . . . . . . . . . . . . 22 𝑤(𝑔𝑦)
302301esumcl 31399 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
303300, 302mpan 689 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
304299, 303syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
305286, 287, 288, 304syl21anc 836 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
306305ex 416 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)))
307285, 306ralrimi 3180 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
30814esumcl 31399 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
309178, 307, 308syl2anc 587 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
310105, 309sseldi 3913 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
311 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑤(𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
312 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
313 fniunfv 6984 . . . . . . . . . . . . . . . . . . . 20 (𝑔 Fn 𝑋 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
314312, 214, 3133syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
315311, 314esumeq1d 31404 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
31611adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑋 ∈ V)
317300a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑔𝑦) ∈ V)
318316, 317, 298esumiun 31463 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
319315, 318eqbrtrrd 5054 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
3209, 319sylan 583 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
321320adantr 484 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
322253, 321eqbrtrid 5065 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
323286, 288, 46syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
324 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+))
325324, 288, 73syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
326323, 325xrge0addcld 30512 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
327326ex 416 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)))
328285, 327ralrimi 3180 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
32914esumcl 31399 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
330178, 328, 329syl2anc 587 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
331105, 330sseldi 3913 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
332216, 10syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
333 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ))
334 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑦𝑋)
335333, 334, 49syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
336335adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑀𝐴) ∈ ℝ)
33765adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
338337adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
339 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 *𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
340339adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
34166breq2d 5042 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
342341biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
343336, 338, 340, 342syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
344343ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
345333simpld 498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝜑)
346 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
347345, 346, 334, 304syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
348105, 347sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
349335rexrd 10680 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ*)
350337rexrd 10680 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
351349, 350xaddcld 12682 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
352 xrltle 12530 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ* ∧ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
353348, 351, 352syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
354344, 353syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
355354adantld 494 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
356355ex 416 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (𝑦𝑋 → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))))
357283, 356ralrimi 3180 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
358 ralim 3130 . . . . . . . . . . . . . . . . . . 19 (∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
359357, 358syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
360359imp 410 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
361360r19.21bi 3173 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
362285, 14, 332, 305, 326, 361esumlef 31431 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
363164, 46sylan 583 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
364285, 14, 332, 363, 325esumaddf 31430 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))))
365325ex 416 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)))
366285, 365ralrimi 3180 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
36714esumcl 31399 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
368178, 366, 367syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
369105, 368sseldi 3913 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
370 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑓:𝑋1-1→ℕ)
371 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
372371rnex 7599 . . . . . . . . . . . . . . . . . . . . . . 23 ran 𝑓 ∈ V
373372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V)
37458frnd 6494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 ⊆ ℕ)
375374adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
376375sselda 3915 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
37754a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
378 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
379378nnzd 12074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
380377, 379rpexpcld 13604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
381380rpreccld 12429 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
38271, 381sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
383382adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
384376, 383syldan 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
385384ralrimiva 3149 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
386 nfcv 2955 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧ran 𝑓
387386esumcl 31399 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
388373, 385, 387syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
389105, 388sseldi 3913 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
390 1xr 10689 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
391390a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
39271sseli 3911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+𝑒 ∈ (0[,]+∞))
393392adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
394 elxrge0 12835 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
395393, 394sylib 221 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
396 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧(𝜑𝑓:𝑋1-1→ℕ)
397 nnex 11631 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ ∈ V
398397a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → ℕ ∈ V)
399396, 398, 382, 374esummono 31423 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
400 oveq2 7143 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
401400oveq2d 7151 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
402 ioossico 12816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0(,)+∞) ⊆ (0[,)+∞)
40369, 402eqsstri 3949 . . . . . . . . . . . . . . . . . . . . . . . . 25 + ⊆ (0[,)+∞)
404403, 381sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
405 eqidd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
406 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
407406oveq2d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
408407oveq2d 7151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
409 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
410 ovexd 7170 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
411405, 408, 409, 410fvmptd 6752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
412411adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
413 ax-1cn 10584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
414 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
415414geo2lim 15223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℂ → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
416413, 415ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1
417416a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
418 1re 10630 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
419418a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 1 ∈ ℝ)
420401, 404, 412, 417, 419esumcvgsum 31457 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
421 geoihalfsum 15230 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
422420, 421eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
423399, 422breqtrd 5056 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
424423adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
425 xlemul2a 12670 . . . . . . . . . . . . . . . . . . . 20 (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
426389, 391, 395, 424, 425syl31anc 1370 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
42713, 19nfan 1900 . . . . . . . . . . . . . . . . . . . . . 22 𝑦(𝜑𝑓:𝑋1-1→ℕ)
428427, 21nfan 1900 . . . . . . . . . . . . . . . . . . . . 21 𝑦((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
42976recnd 10658 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℂ)
43078recnd 10658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
431430adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
432 2cn 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
433432a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℂ)
434 2ne0 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≠ 0
435434a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ≠ 0)
436433, 435, 60expne0d 13512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
437436adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
438429, 431, 437divrecd 11408 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
439 1rp 12381 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℝ+
440439a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 1 ∈ ℝ+)
441440, 61rpdivcld 12436 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ+)
44252, 441sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
443442adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
444 rexmul 12652 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
44576, 443, 444syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
446438, 445eqtr4d 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
447446ralrimiva 3149 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
448428, 447esumeq2d 31406 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
44911ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
45071, 441sseldi 3913 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
451450adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
452403a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
453452sselda 3915 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
454449, 451, 453esummulc2 31451 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
455 nfcv 2955 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦(1 / (2↑𝑧))
456 oveq2 7143 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑓𝑦) → (2↑𝑧) = (2↑(𝑓𝑦)))
457456oveq2d 7151 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑓𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓𝑦))))
45811adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑋 ∈ V)
45956simprbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → Fun 𝑓)
46057feqmptd 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
461460cnveqd 5710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
462461funeqd 6346 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → (Fun 𝑓 ↔ Fun (𝑦𝑋 ↦ (𝑓𝑦))))
463459, 462mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
464463adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
465455, 427, 14, 457, 458, 464, 450, 59esumc 31420 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
466 ffn 6487 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
467 fnrnfv 6700 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
46858, 466, 4673syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
469396, 468esumeq1d 31404 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
470465, 469eqtr4d 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
471470adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
472471oveq2d 7151 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
473448, 454, 4723eqtr2rd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))))
474395simpld 498 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
475 xmulid1 12660 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
476474, 475syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
477426, 473, 4763brtr3d 5061 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
478164, 370, 205, 477syl21anc 836 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
479 xleadd2a 12635 . . . . . . . . . . . . . . . . 17 (((Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*) ∧ Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
480369, 206, 204, 478, 479syl31anc 1370 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
481364, 480eqbrtrd 5052 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
482310, 331, 207, 362, 481xrletrd 12543 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
483202, 310, 207, 322, 482xrletrd 12543 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
484176, 202, 207, 281, 483xrletrd 12543 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
485205rpred 12419 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ)
486 rexadd 12613 . . . . . . . . . . . . 13 ((Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
487203, 485, 486syl2anc 587 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
488484, 487breqtrd 5056 . . . . . . . . . . 11 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
489488anasss 470 . . . . . . . . . 10 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
490489ex 416 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
491490exlimdv 1934 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
492163, 491mpd 15 . . . . . . 7 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
493492ralrimiva 3149 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
494 xralrple 12586 . . . . . . . 8 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
495175, 494sylan 583 . . . . . . 7 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
496495adantr 484 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
497493, 496mpbird 260 . . . . 5 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
498497ex 416 . . . 4 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
499498exlimdv 1934 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
5008, 499mpd 15 . 2 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
501175adantr 484 . . . 4 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
502 pnfge 12513 . . . 4 ((𝑀 𝑦𝑋 𝐴) ∈ ℝ* → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
503501, 502syl 17 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
50446ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞))
50514esumcl 31399 . . . . 5 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
50611, 504, 505syl2anc 587 . . . 4 (𝜑 → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
507 xrge0nre 12831 . . . 4 ((Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
508506, 507sylan 583 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
509503, 508breqtrrd 5058 . 2 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
510500, 509pm2.61dan 812 1 (𝜑 → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2111  {cab 2776  wne 2987  wral 3106  wrex 3107  {crab 3110  Vcvv 3441  wss 3881  𝒫 cpw 4497   cuni 4800   ciun 4881   class class class wbr 5030  cmpt 5110   Or wor 5437  ccnv 5518  dom cdm 5519  ran crn 5520  Fun wfun 6318   Fn wfn 6319  wf 6320  1-1wf1 6321  cfv 6324  (class class class)co 7135  ωcom 7560  cen 8489  cdom 8490  infcinf 8889  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661  *cxr 10663   < clt 10664  cle 10665   / cdiv 11286  cn 11625  2c2 11680  cz 11969  +crp 12377   +𝑒 cxad 12493   ·e cxmu 12494  (,)cioo 12726  [,)cico 12728  [,]cicc 12729  seqcseq 13364  cexp 13425  cli 14833  Σcsu 15034  Σ*cesum 31396  toOMeascoms 31659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-reg 9040  ax-inf2 9088  ax-cc 9846  ax-ac2 9874  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-r1 9177  df-rank 9178  df-card 9352  df-acn 9355  df-ac 9527  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-xnn0 11956  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-ordt 16766  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-ps 17802  df-tsr 17803  df-plusf 17843  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-mhm 17948  df-submnd 17949  df-grp 18098  df-minusg 18099  df-sbg 18100  df-mulg 18217  df-subg 18268  df-cntz 18439  df-cmn 18900  df-abl 18901  df-mgp 19233  df-ur 19245  df-ring 19292  df-cring 19293  df-subrg 19526  df-abv 19581  df-lmod 19629  df-scaf 19630  df-sra 19937  df-rgmod 19938  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-fbas 20088  df-fg 20089  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626  df-nei 21703  df-lp 21741  df-perf 21742  df-cn 21832  df-cnp 21833  df-haus 21920  df-tx 22167  df-hmeo 22360  df-fil 22451  df-fm 22543  df-flim 22544  df-flf 22545  df-tmd 22677  df-tgp 22678  df-tsms 22732  df-trg 22765  df-xms 22927  df-ms 22928  df-tms 22929  df-nm 23189  df-ngp 23190  df-nrg 23192  df-nlm 23193  df-ii 23482  df-cncf 23483  df-limc 24469  df-dv 24470  df-log 25148  df-esum 31397  df-oms 31660
This theorem is referenced by:  omsmeas  31691
  Copyright terms: Public domain W3C validator