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 34265
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 14031 . . . . . . 7 ℕ ≈ ω
32ensymi 9064 . . . . . 6 ω ≈ ℕ
4 domentr 9073 . . . . . 6 ((𝑋 ≼ ω ∧ ω ≈ ℕ) → 𝑋 ≼ ℕ)
51, 3, 4sylancl 585 . . . . 5 (𝜑𝑋 ≼ ℕ)
6 brdomi 9018 . . . . 5 (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋1-1→ℕ)
75, 6syl 17 . . . 4 (𝜑 → ∃𝑓 𝑓:𝑋1-1→ℕ)
87adantr 480 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋1-1→ℕ)
9 simplll 774 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10 ctex 9023 . . . . . . . . . . 11 (𝑋 ≼ ω → 𝑋 ∈ V)
111, 10syl 17 . . . . . . . . . 10 (𝜑𝑋 ∈ V)
129, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13 nfv 1913 . . . . . . . . . . . . 13 𝑦𝜑
14 nfcv 2908 . . . . . . . . . . . . . . 15 𝑦𝑋
1514nfesum1 34004 . . . . . . . . . . . . . 14 𝑦Σ*𝑦𝑋(𝑀𝐴)
16 nfcv 2908 . . . . . . . . . . . . . 14 𝑦
1715, 16nfel 2923 . . . . . . . . . . . . 13 𝑦Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ
1813, 17nfan 1898 . . . . . . . . . . . 12 𝑦(𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
19 nfv 1913 . . . . . . . . . . . 12 𝑦 𝑓:𝑋1-1→ℕ
2018, 19nfan 1898 . . . . . . . . . . 11 𝑦((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ)
21 nfv 1913 . . . . . . . . . . 11 𝑦 𝑒 ∈ ℝ+
2220, 21nfan 1898 . . . . . . . . . 10 𝑦(((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
239adantr 480 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝜑)
24 simpr 484 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑦𝑋)
2511adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → 𝑋 ∈ V)
26 oms.o . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄𝑉)
27 oms.r . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅:𝑄⟶(0[,]+∞))
28 omsf 34261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 = (toOMeas‘𝑅)
3029feq1i 6738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀:𝒫 dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
3128, 30sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3226, 27, 31syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3332adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 𝑄)
3527fdmd 6757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom 𝑅 = 𝑄)
3635unieqd 4944 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 dom 𝑅 = 𝑄)
3736adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → dom 𝑅 = 𝑄)
3834, 37sseqtrrd 4050 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → 𝐴 dom 𝑅)
3926uniexd 7777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 𝑄 ∈ V)
4039adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑋) → 𝑄 ∈ V)
41 ssexg 5341 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 𝑄 𝑄 ∈ V) → 𝐴 ∈ V)
4234, 40, 41syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 ∈ V)
43 elpwg 4625 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ V → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4538, 44mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝐴 ∈ 𝒫 dom 𝑅)
4633, 45ffvelcdmd 7119 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
4746adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
4918, 25, 47, 48esumcvgre 34055 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5049adantlr 714 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5150adantlr 714 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
52 rpssre 13064 . . . . . . . . . . . . . . . . . . 19 + ⊆ ℝ
53 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
54 2rp 13062 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ+
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℝ+)
56 df-f1 6578 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun 𝑓))
5756simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → 𝑓:𝑋⟶ℕ)
5857adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑓:𝑋⟶ℕ)
5958ffvelcdmda 7118 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℕ)
6059nnzd 12666 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
6155, 60rpexpcld 14296 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6261adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6353, 62rpdivcld 13116 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ+)
6452, 63sselid 4006 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
6564adantl3r 749 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
66 rexadd 13294 . . . . . . . . . . . . . . . . 17 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
6751, 65, 66syl2anc 583 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
689, 46sylan 579 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
69 dfrp2 13456 . . . . . . . . . . . . . . . . . . . 20 + = (0(,)+∞)
70 ioossicc 13493 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
7169, 70eqsstri 4043 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
7271, 63sselid 4006 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7372adantl3r 749 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7468, 73xrge0addcld 32769 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7567, 74eqeltrrd 2845 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7652, 53sselid 4006 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7776adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7852, 61sselid 4006 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
7978adantlr 714 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8079adantl3r 749 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
81 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
8281rpgt0d 13102 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 𝑒)
83 2re 12367 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 2 ∈ ℝ)
8560adantllr 718 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
8685adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
87 2pos 12396 . . . . . . . . . . . . . . . . . . . 20 0 < 2
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 2)
89 expgt0 14146 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ (𝑓𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓𝑦)))
9084, 86, 88, 89syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (2↑(𝑓𝑦)))
9177, 80, 82, 90divgt0d 12230 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (𝑒 / (2↑(𝑓𝑦))))
9265, 51ltaddposd 11874 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (0 < (𝑒 / (2↑(𝑓𝑦))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
9391, 92mpbid 232 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
9429fveq1i 6921 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝐴) = ((toOMeas‘𝑅)‘𝐴)
9526adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑄𝑉)
9627adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑅:𝑄⟶(0[,]+∞))
97 omsfval 34259 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9895, 96, 34, 97syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9994, 98eqtrid 2792 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
1009, 99sylan 579 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
101100eqcomd 2746 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) = (𝑀𝐴))
102101breq1d 5176 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
10393, 102mpbird 257 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
10475, 103jca 511 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
105 iccssxr 13490 . . . . . . . . . . . . . . . . . . 19 (0[,]+∞) ⊆ ℝ*
106 xrltso 13203 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
107 soss 5628 . . . . . . . . . . . . . . . . . . 19 ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
108105, 106, 107mp2 9 . . . . . . . . . . . . . . . . . 18 < Or (0[,]+∞)
109 biid 261 . . . . . . . . . . . . . . . . . 18 ( < Or (0[,]+∞) ↔ < Or (0[,]+∞))
110108, 109mpbi 230 . . . . . . . . . . . . . . . . 17 < Or (0[,]+∞)
111110a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → < Or (0[,]+∞))
112 omscl 34260 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
11395, 96, 45, 112syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
114 xrge0infss 32767 . . . . . . . . . . . . . . . . 17 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
115113, 114syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
116111, 115infglb 9559 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → ((((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
117116imp 406 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑋) ∧ (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
11823, 24, 104, 117syl21anc 837 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
119 eqid 2740 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
120 esumex 33993 . . . . . . . . . . . . . . . . . . 19 Σ*𝑤𝑥(𝑅𝑤) ∈ V
121119, 120elrnmpti 5985 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤))
122121anbi1i 623 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
123 r19.41v 3195 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
124122, 123bitr4i 278 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
125124exbii 1846 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
126 df-rex 3077 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
127 rexcom4 3294 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
128125, 126, 1273bitr4i 303 . . . . . . . . . . . . . 14 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
129 breq1 5169 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
130 idd 24 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
131129, 130sylbid 240 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
132131imp 406 . . . . . . . . . . . . . . . 16 ((𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
133132exlimiv 1929 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
134133reximi 3090 . . . . . . . . . . . . . 14 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
135128, 134sylbi 217 . . . . . . . . . . . . 13 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
136118, 135syl 17 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
137 simpr 484 . . . . . . . . . . . . . . . 16 ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω)
138137a1i 11 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω))
139138ss2rabi 4100 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
140 rexss 4084 . . . . . . . . . . . . . 14 ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
141139, 140ax-mp 5 . . . . . . . . . . . . 13 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
142 unieq 4942 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 𝑧 = 𝑥)
143142sseq2d 4041 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐴 𝑧𝐴 𝑥))
144 breq1 5169 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
145143, 144anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝐴 𝑧𝑧 ≼ ω) ↔ (𝐴 𝑥𝑥 ≼ ω)))
146145elrab 3708 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 𝑥𝑥 ≼ ω)))
147146simprbi 496 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → (𝐴 𝑥𝑥 ≼ ω))
148147simpld 494 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥)
149148a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥))
150149anim1d 610 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
151150reximdv 3176 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
152141, 151biimtrid 242 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
153136, 152mpd 15 . . . . . . . . . . 11 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
154153ex 412 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
15522, 154ralrimi 3263 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
156 unieq 4942 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → 𝑥 = (𝑔𝑦))
157156sseq2d 4041 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (𝐴 𝑥𝐴 (𝑔𝑦)))
158 esumeq1 33998 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
159158breq1d 5176 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
160157, 159anbi12d 631 . . . . . . . . . . 11 (𝑥 = (𝑔𝑦) → ((𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
161160ac6sg 10557 . . . . . . . . . 10 (𝑋 ∈ V → (∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))))
162161imp 406 . . . . . . . . 9 ((𝑋 ∈ V ∧ ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
16312, 155, 162syl2anc 583 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
1649ad2antrr 725 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
16538ralrimiva 3152 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦𝑋 𝐴 dom 𝑅)
166 iunss 5068 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀𝑦𝑋 𝐴 dom 𝑅)
167165, 166sylibr 234 . . . . . . . . . . . . . . . . 17 (𝜑 𝑦𝑋 𝐴 dom 𝑅)
16842ralrimiva 3152 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦𝑋 𝐴 ∈ V)
169 iunexg 8004 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 𝐴 ∈ V) → 𝑦𝑋 𝐴 ∈ V)
17011, 168, 169syl2anc 583 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑦𝑋 𝐴 ∈ V)
171 elpwg 4625 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
172170, 171syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
173167, 172mpbird 257 . . . . . . . . . . . . . . . 16 (𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅)
17432, 173ffvelcdmd 7119 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ (0[,]+∞))
175105, 174sselid 4006 . . . . . . . . . . . . . 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)
179177, 178fexd 7264 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 ∈ V)
180 rnexg 7942 . . . . . . . . . . . . . . . 16 (𝑔 ∈ V → ran 𝑔 ∈ V)
181 uniexg 7775 . . . . . . . . . . . . . . . 16 (ran 𝑔 ∈ V → ran 𝑔 ∈ V)
182179, 180, 1813syl 18 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ V)
183 simp-5l 784 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
18427ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
185 frn 6754 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
186 ssrab2 4103 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
187185, 186sstrdi 4021 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
188187unissd 4941 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 𝒫 dom 𝑅)
189 unipw 5470 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 dom 𝑅 = dom 𝑅
190188, 189sseqtrdi 4059 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
191190adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ⊆ dom 𝑅)
19235adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
193191, 192sseqtrd 4049 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔𝑄)
194193sselda 4008 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑐𝑄)
195184, 194ffvelcdmd 7119 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → (𝑅𝑐) ∈ (0[,]+∞))
196195ralrimiva 3152 . . . . . . . . . . . . . . . 16 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
197183, 177, 196syl2anc 583 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
198 nfcv 2908 . . . . . . . . . . . . . . . 16 𝑐 ran 𝑔
199198esumcl 33994 . . . . . . . . . . . . . . 15 (( ran 𝑔 ∈ V ∧ ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
200182, 197, 199syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
201105, 200sselid 4006 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*)
202 simp-5r 785 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
203202rexrd 11340 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*)
204 simpllr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ+)
205204rpxrd 13100 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ*)
206203, 205xaddcld 13363 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) ∈ ℝ*)
207185ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
208 sstr 4017 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
209186, 208mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
210 sspwuni 5123 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅)
211209, 210sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
212207, 211syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ dom 𝑅)
213 ffn 6747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑔 Fn 𝑋)
214213ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 Fn 𝑋)
215164, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ≼ ω)
216 fnct 10606 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 Fn 𝑋𝑋 ≼ ω) → 𝑔 ≼ ω)
217 rnct 10594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 ≼ ω → ran 𝑔 ≼ ω)
218216, 217syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 Fn 𝑋𝑋 ≼ ω) → ran 𝑔 ≼ ω)
219 dfss3 3997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
220219biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
221 breq1 5169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
222221elrab 3708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω))
223222simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑤 ≼ ω)
224223ralimi 3089 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
225220, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
226 unictb 10644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ran 𝑔 ≼ ω)
227218, 225, 226syl2an 595 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn 𝑋𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ≼ ω)
228214, 215, 207, 227syl21anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ≼ ω)
229 ctex 9023 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V)
230 elpwg 4625 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ∈ V → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
231228, 229, 2303syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
232212, 231mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ 𝒫 dom 𝑅)
233 simpl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝐴 (𝑔𝑦))
234233ralimi 3089 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 𝐴 (𝑔𝑦))
235 fvssunirn 6953 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔𝑦) ⊆ ran 𝑔
236235unissi 4940 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔𝑦) ⊆ ran 𝑔
237 sstr 4017 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 (𝑔𝑦) ∧ (𝑔𝑦) ⊆ ran 𝑔) → 𝐴 ran 𝑔)
238236, 237mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 (𝑔𝑦) → 𝐴 ran 𝑔)
239238ralimi 3089 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑋 𝐴 (𝑔𝑦) → ∀𝑦𝑋 𝐴 ran 𝑔)
240 iunss 5068 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑦𝑋 𝐴 ran 𝑔 ↔ ∀𝑦𝑋 𝐴 ran 𝑔)
241239, 240sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 𝐴 (𝑔𝑦) → 𝑦𝑋 𝐴 ran 𝑔)
242234, 241syl 17 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝑦𝑋 𝐴 ran 𝑔)
243242adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑦𝑋 𝐴 ran 𝑔)
244232, 243, 228jca32 515 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
245 unieq 4942 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ran 𝑔 𝑧 = ran 𝑔)
246245sseq2d 4041 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔))
247 breq1 5169 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → (𝑧 ≼ ω ↔ ran 𝑔 ≼ ω))
248246, 247anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ran 𝑔 → (( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
249248elrab 3708 . . . . . . . . . . . . . . . . . . 19 ( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
250244, 249sylibr 234 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)})
251 fveq2 6920 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑤 → (𝑅𝑐) = (𝑅𝑤))
252251cbvesumv 34007 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)
253 esumeq1 33998 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝑔 → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
254253rspceeqv 3658 . . . . . . . . . . . . . . . . . 18 (( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
255250, 252, 254sylancl 585 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
256 esumex 33993 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ V
257 eqid 2740 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
258257elrnmpt 5981 . . . . . . . . . . . . . . . . . 18 *𝑐 ran 𝑔(𝑅𝑐) ∈ V → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤)))
259256, 258ax-mp 5 . . . . . . . . . . . . . . . . 17 *𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
260255, 259sylibr 234 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)))
261110a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → < Or (0[,]+∞))
262 omscl 34260 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
26326, 27, 173, 262syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
264 xrge0infss 32767 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
265263, 264syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
266261, 265inflb 9558 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
26729fveq1i 6921 . . . . . . . . . . . . . . . . . . . 20 (𝑀 𝑦𝑋 𝐴) = ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴)
268167, 36sseqtrd 4049 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝑦𝑋 𝐴 𝑄)
269 omsfval 34259 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 𝑄) → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
27026, 27, 268, 269syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
271267, 270eqtrid 2792 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
272271breq2d 5178 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
273272notbid 318 . . . . . . . . . . . . . . . . 17 (𝜑 → (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
274266, 273sylibrd 259 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
275164, 260, 274sylc 65 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
276 biid 261 . . . . . . . . . . . . . . 15 (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
277275, 276sylib 218 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
278 xrlenlt 11355 . . . . . . . . . . . . . . 15 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
279176, 201, 278syl2anc 583 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
280277, 279mpbird 257 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐))
281 nfv 1913 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
28222, 281nfan 1898 . . . . . . . . . . . . . . . . . 18 𝑦((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
283 nfra1 3290 . . . . . . . . . . . . . . . . . 18 𝑦𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
284282, 283nfan 1898 . . . . . . . . . . . . . . . . 17 𝑦(((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
285 simp-6l 786 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝜑)
286 simpllr 775 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
287 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑦𝑋)
28827ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
289 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
290 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑦𝑋)
291289, 290ffvelcdmd 7119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
292186, 291sselid 4006 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ 𝒫 dom 𝑅)
293292elpwid 4631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ dom 𝑅)
294288, 293fssdmd 6765 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ 𝑄)
295 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤 ∈ (𝑔𝑦))
296294, 295sseldd 4009 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤𝑄)
297288, 296ffvelcdmd 7119 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑅𝑤) ∈ (0[,]+∞))
298297ralrimiva 3152 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
299 fvex 6933 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑦) ∈ V
300 nfcv 2908 . . . . . . . . . . . . . . . . . . . . . 22 𝑤(𝑔𝑦)
301300esumcl 33994 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
302299, 301mpan 689 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
303298, 302syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
304285, 286, 287, 303syl21anc 837 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
305304ex 412 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)))
306284, 305ralrimi 3263 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
30714esumcl 33994 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
308178, 306, 307syl2anc 583 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
309105, 308sselid 4006 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
310 nfv 1913 . . . . . . . . . . . . . . . . . . 19 𝑤(𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
311 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
312 fniunfv 7284 . . . . . . . . . . . . . . . . . . . 20 (𝑔 Fn 𝑋 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
313311, 213, 3123syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
314310, 313esumeq1d 33999 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
31511adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑋 ∈ V)
316299a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑔𝑦) ∈ V)
317315, 316, 297esumiun 34058 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
318314, 317eqbrtrrd 5190 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
3199, 318sylan 579 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
320319adantr 480 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
321252, 320eqbrtrid 5201 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
322285, 287, 46syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
323 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+))
324323, 287, 73syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
325322, 324xrge0addcld 32769 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
326325ex 412 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)))
327284, 326ralrimi 3263 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
32814esumcl 33994 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
329178, 327, 328syl2anc 583 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
330105, 329sselid 4006 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
331215, 10syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
332 simp-4l 782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ))
333 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑦𝑋)
334332, 333, 49syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
335334adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑀𝐴) ∈ ℝ)
33665adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
337336adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
338 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 *𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
339338adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
34066breq2d 5178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
341340biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
342335, 337, 339, 341syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
343342ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
344332simpld 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝜑)
345 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
346344, 345, 333, 303syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
347105, 346sselid 4006 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
348334rexrd 11340 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ*)
349336rexrd 11340 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
350348, 349xaddcld 13363 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
351 xrltle 13211 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ* ∧ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
352347, 350, 351syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
353343, 352syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
354353adantld 490 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
355354ex 412 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (𝑦𝑋 → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))))
356282, 355ralrimi 3263 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
357 ralim 3092 . . . . . . . . . . . . . . . . . . 19 (∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
358356, 357syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
359358imp 406 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
360359r19.21bi 3257 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
361284, 14, 331, 304, 325, 360esumlef 34026 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
362164, 46sylan 579 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
363284, 14, 331, 362, 324esumaddf 34025 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))))
364324ex 412 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)))
365284, 364ralrimi 3263 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
36614esumcl 33994 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
367178, 365, 366syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
368105, 367sselid 4006 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
369 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑓:𝑋1-1→ℕ)
370 vex 3492 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
371370rnex 7950 . . . . . . . . . . . . . . . . . . . . . . 23 ran 𝑓 ∈ V
372371a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V)
37358frnd 6755 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 ⊆ ℕ)
374373adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
375374sselda 4008 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
37654a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
377 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
378377nnzd 12666 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
379376, 378rpexpcld 14296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
380379rpreccld 13109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
38171, 380sselid 4006 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
382381adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
383375, 382syldan 590 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
384383ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
385 nfcv 2908 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧ran 𝑓
386385esumcl 33994 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
387372, 384, 386syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
388105, 387sselid 4006 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
389 1xr 11349 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
390389a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
39171sseli 4004 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+𝑒 ∈ (0[,]+∞))
392391adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
393 elxrge0 13517 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
394392, 393sylib 218 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
395 nfv 1913 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧(𝜑𝑓:𝑋1-1→ℕ)
396 nnex 12299 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ ∈ V
397396a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → ℕ ∈ V)
398395, 397, 381, 373esummono 34018 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
399 oveq2 7456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
400399oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
401 ioossico 13498 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0(,)+∞) ⊆ (0[,)+∞)
40269, 401eqsstri 4043 . . . . . . . . . . . . . . . . . . . . . . . . 25 + ⊆ (0[,)+∞)
403402, 380sselid 4006 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
404 eqidd 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
405 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
406405oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
407406oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
408 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
409 ovexd 7483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
410404, 407, 408, 409fvmptd 7036 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
411410adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
412 ax-1cn 11242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
413 eqid 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
414413geo2lim 15923 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℂ → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
415412, 414ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1
416415a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
417 1re 11290 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
418417a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 1 ∈ ℝ)
419400, 403, 411, 416, 418esumcvgsum 34052 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
420 geoihalfsum 15930 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
421419, 420eqtrdi 2796 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
422398, 421breqtrd 5192 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
423422adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
424 xlemul2a 13351 . . . . . . . . . . . . . . . . . . . 20 (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
425388, 390, 394, 423, 424syl31anc 1373 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
42613, 19nfan 1898 . . . . . . . . . . . . . . . . . . . . . 22 𝑦(𝜑𝑓:𝑋1-1→ℕ)
427426, 21nfan 1898 . . . . . . . . . . . . . . . . . . . . 21 𝑦((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
42876recnd 11318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℂ)
42978recnd 11318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
430429adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
431 2cn 12368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
432431a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℂ)
433 2ne0 12397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≠ 0
434433a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ≠ 0)
435432, 434, 60expne0d 14202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
436435adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
437428, 430, 436divrecd 12073 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
438 1rp 13061 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℝ+
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 1 ∈ ℝ+)
440439, 61rpdivcld 13116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ+)
44152, 440sselid 4006 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
442441adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
443 rexmul 13333 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
44476, 442, 443syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
445437, 444eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
446445ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
447427, 446esumeq2d 34001 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
44811ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
44971, 440sselid 4006 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
450449adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
451402a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
452451sselda 4008 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
453448, 450, 452esummulc2 34046 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
454 nfcv 2908 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦(1 / (2↑𝑧))
455 oveq2 7456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑓𝑦) → (2↑𝑧) = (2↑(𝑓𝑦)))
456455oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑓𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓𝑦))))
45711adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑋 ∈ V)
45856simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → Fun 𝑓)
45957feqmptd 6990 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
460459cnveqd 5900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
461460funeqd 6600 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → (Fun 𝑓 ↔ Fun (𝑦𝑋 ↦ (𝑓𝑦))))
462458, 461mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
463462adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
464454, 426, 14, 456, 457, 463, 449, 59esumc 34015 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
465 ffn 6747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
466 fnrnfv 6981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
46758, 465, 4663syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
468395, 467esumeq1d 33999 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
469464, 468eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
470469adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
471470oveq2d 7464 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
472447, 453, 4713eqtr2rd 2787 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))))
473394simpld 494 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
474 xmulrid 13341 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
475473, 474syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
476425, 472, 4753brtr3d 5197 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
477164, 369, 204, 476syl21anc 837 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
478 xleadd2a 13316 . . . . . . . . . . . . . . . . 17 (((Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*) ∧ Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
479368, 205, 203, 477, 478syl31anc 1373 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
480363, 479eqbrtrd 5188 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
481309, 330, 206, 361, 480xrletrd 13224 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
482201, 309, 206, 321, 481xrletrd 13224 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
483176, 201, 206, 280, 482xrletrd 13224 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
484204rpred 13099 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ)
485 rexadd 13294 . . . . . . . . . . . . 13 ((Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
486202, 484, 485syl2anc 583 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
487483, 486breqtrd 5192 . . . . . . . . . . 11 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
488487anasss 466 . . . . . . . . . 10 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
489488ex 412 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
490489exlimdv 1932 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
491163, 490mpd 15 . . . . . . 7 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
492491ralrimiva 3152 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
493 xralrple 13267 . . . . . . . 8 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
494175, 493sylan 579 . . . . . . 7 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
495494adantr 480 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
496492, 495mpbird 257 . . . . 5 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
497496ex 412 . . . 4 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
498497exlimdv 1932 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
4998, 498mpd 15 . 2 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
500175adantr 480 . . . 4 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
501 pnfge 13193 . . . 4 ((𝑀 𝑦𝑋 𝐴) ∈ ℝ* → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
502500, 501syl 17 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
50346ralrimiva 3152 . . . . 5 (𝜑 → ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞))
50414esumcl 33994 . . . . 5 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
50511, 503, 504syl2anc 583 . . . 4 (𝜑 → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
506 xrge0nre 13513 . . . 4 ((Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
507505, 506sylan 579 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
508502, 507breqtrrd 5194 . 2 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
509499, 508pm2.61dan 812 1 (𝜑 → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2108  {cab 2717  wne 2946  wral 3067  wrex 3076  {crab 3443  Vcvv 3488  wss 3976  𝒫 cpw 4622   cuni 4931   ciun 5015   class class class wbr 5166  cmpt 5249   Or wor 5606  ccnv 5699  dom cdm 5700  ran crn 5701  Fun wfun 6567   Fn wfn 6568  wf 6569  1-1wf1 6570  cfv 6573  (class class class)co 7448  ωcom 7903  cen 9000  cdom 9001  infcinf 9510  cc 11182  cr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  +∞cpnf 11321  *cxr 11323   < clt 11324  cle 11325   / cdiv 11947  cn 12293  2c2 12348  cz 12639  +crp 13057   +𝑒 cxad 13173   ·e cxmu 13174  (,)cioo 13407  [,)cico 13409  [,]cicc 13410  seqcseq 14052  cexp 14112  cli 15530  Σcsu 15734  Σ*cesum 33991  toOMeascoms 34256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-reg 9661  ax-inf2 9710  ax-cc 10504  ax-ac2 10532  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263  ax-mulf 11264
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-r1 9833  df-rank 9834  df-card 10008  df-acn 10011  df-ac 10185  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-xnn0 12626  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ioc 13412  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-fac 14323  df-bc 14352  df-hash 14380  df-shft 15116  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-limsup 15517  df-clim 15534  df-rlim 15535  df-sum 15735  df-ef 16115  df-sin 16117  df-cos 16118  df-pi 16120  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-ordt 17561  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-ps 18636  df-tsr 18637  df-plusf 18677  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-submnd 18819  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-cntz 19357  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-cring 20263  df-subrng 20572  df-subrg 20597  df-abv 20832  df-lmod 20882  df-scaf 20883  df-sra 21195  df-rgmod 21196  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-fbas 21384  df-fg 21385  df-cnfld 21388  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-lp 23165  df-perf 23166  df-cn 23256  df-cnp 23257  df-haus 23344  df-tx 23591  df-hmeo 23784  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-tmd 24101  df-tgp 24102  df-tsms 24156  df-trg 24189  df-xms 24351  df-ms 24352  df-tms 24353  df-nm 24616  df-ngp 24617  df-nrg 24619  df-nlm 24620  df-ii 24922  df-cncf 24923  df-limc 25921  df-dv 25922  df-log 26616  df-esum 33992  df-oms 34257
This theorem is referenced by:  omsmeas  34288
  Copyright terms: Public domain W3C validator