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 34477
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 13915 . . . . . . 7 ℕ ≈ ω
32ensymi 8953 . . . . . 6 ω ≈ ℕ
4 domentr 8962 . . . . . 6 ((𝑋 ≼ ω ∧ ω ≈ ℕ) → 𝑋 ≼ ℕ)
51, 3, 4sylancl 587 . . . . 5 (𝜑𝑋 ≼ ℕ)
6 brdomi 8908 . . . . 5 (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋1-1→ℕ)
75, 6syl 17 . . . 4 (𝜑 → ∃𝑓 𝑓:𝑋1-1→ℕ)
87adantr 480 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋1-1→ℕ)
9 simplll 775 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10 ctex 8912 . . . . . . . . . . 11 (𝑋 ≼ ω → 𝑋 ∈ V)
111, 10syl 17 . . . . . . . . . 10 (𝜑𝑋 ∈ V)
129, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13 nfv 1916 . . . . . . . . . . . . 13 𝑦𝜑
14 nfcv 2899 . . . . . . . . . . . . . . 15 𝑦𝑋
1514nfesum1 34217 . . . . . . . . . . . . . 14 𝑦Σ*𝑦𝑋(𝑀𝐴)
16 nfcv 2899 . . . . . . . . . . . . . 14 𝑦
1715, 16nfel 2914 . . . . . . . . . . . . 13 𝑦Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ
1813, 17nfan 1901 . . . . . . . . . . . 12 𝑦(𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
19 nfv 1916 . . . . . . . . . . . 12 𝑦 𝑓:𝑋1-1→ℕ
2018, 19nfan 1901 . . . . . . . . . . 11 𝑦((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ)
21 nfv 1916 . . . . . . . . . . 11 𝑦 𝑒 ∈ ℝ+
2220, 21nfan 1901 . . . . . . . . . 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 34473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 = (toOMeas‘𝑅)
3029feq1i 6661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀:𝒫 dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
3128, 30sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3226, 27, 31syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3332adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 𝑄)
3527fdmd 6680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom 𝑅 = 𝑄)
3635unieqd 4878 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 dom 𝑅 = 𝑄)
3736adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → dom 𝑅 = 𝑄)
3834, 37sseqtrrd 3973 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → 𝐴 dom 𝑅)
3926uniexd 7697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 𝑄 ∈ V)
4039adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑋) → 𝑄 ∈ V)
41 ssexg 5270 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 𝑄 𝑄 ∈ V) → 𝐴 ∈ V)
4234, 40, 41syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 ∈ V)
43 elpwg 4559 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ V → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4538, 44mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝐴 ∈ 𝒫 dom 𝑅)
4633, 45ffvelcdmd 7039 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
4746adantlr 716 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
4918, 25, 47, 48esumcvgre 34268 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5049adantlr 716 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5150adantlr 716 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
52 rpssre 12925 . . . . . . . . . . . . . . . . . . 19 + ⊆ ℝ
53 simplr 769 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
54 2rp 12922 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ+
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℝ+)
56 df-f1 6505 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun 𝑓))
5756simplbi 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → 𝑓:𝑋⟶ℕ)
5857adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑓:𝑋⟶ℕ)
5958ffvelcdmda 7038 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℕ)
6059nnzd 12526 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
6155, 60rpexpcld 14182 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6261adantlr 716 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6353, 62rpdivcld 12978 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ+)
6452, 63sselid 3933 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
6564adantl3r 751 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
66 rexadd 13159 . . . . . . . . . . . . . . . . 17 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
6751, 65, 66syl2anc 585 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
689, 46sylan 581 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
69 dfrp2 13322 . . . . . . . . . . . . . . . . . . . 20 + = (0(,)+∞)
70 ioossicc 13361 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
7169, 70eqsstri 3982 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
7271, 63sselid 3933 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7372adantl3r 751 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7468, 73xrge0addcld 32852 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7567, 74eqeltrrd 2838 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7652, 53sselid 3933 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7776adantl3r 751 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7852, 61sselid 3933 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
7978adantlr 716 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8079adantl3r 751 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
81 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
8281rpgt0d 12964 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 𝑒)
83 2re 12231 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 2 ∈ ℝ)
8560adantllr 720 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
8685adantlr 716 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
87 2pos 12260 . . . . . . . . . . . . . . . . . . . 20 0 < 2
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 2)
89 expgt0 14030 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ (𝑓𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓𝑦)))
9084, 86, 88, 89syl3anc 1374 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (2↑(𝑓𝑦)))
9177, 80, 82, 90divgt0d 12089 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (𝑒 / (2↑(𝑓𝑦))))
9265, 51ltaddposd 11733 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (0 < (𝑒 / (2↑(𝑓𝑦))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
9391, 92mpbid 232 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
9429fveq1i 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝐴) = ((toOMeas‘𝑅)‘𝐴)
9526adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑄𝑉)
9627adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑅:𝑄⟶(0[,]+∞))
97 omsfval 34471 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9895, 96, 34, 97syl3anc 1374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9994, 98eqtrid 2784 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
1009, 99sylan 581 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
101100eqcomd 2743 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) = (𝑀𝐴))
102101breq1d 5110 . . . . . . . . . . . . . . . 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 13358 . . . . . . . . . . . . . . . . . . 19 (0[,]+∞) ⊆ ℝ*
106 xrltso 13067 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
107 soss 5560 . . . . . . . . . . . . . . . . . . 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 34472 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
11395, 96, 45, 112syl3anc 1374 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
114 xrge0infss 32850 . . . . . . . . . . . . . . . . 17 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
115113, 114syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
116111, 115infglb 9406 . . . . . . . . . . . . . . 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 838 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
119 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
120 esumex 34206 . . . . . . . . . . . . . . . . . . 19 Σ*𝑤𝑥(𝑅𝑤) ∈ V
121119, 120elrnmpti 5919 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤))
122121anbi1i 625 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
123 r19.41v 3168 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
124122, 123bitr4i 278 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
125124exbii 1850 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
126 df-rex 3063 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
127 rexcom4 3265 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
128125, 126, 1273bitr4i 303 . . . . . . . . . . . . . 14 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
129 breq1 5103 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
130 idd 24 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
131129, 130sylbid 240 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
132131imp 406 . . . . . . . . . . . . . . . 16 ((𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
133132exlimiv 1932 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
134133reximi 3076 . . . . . . . . . . . . . 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 4030 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
140 rexss 4011 . . . . . . . . . . . . . 14 ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
141139, 140ax-mp 5 . . . . . . . . . . . . 13 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
142 unieq 4876 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 𝑧 = 𝑥)
143142sseq2d 3968 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐴 𝑧𝐴 𝑥))
144 breq1 5103 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
145143, 144anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝐴 𝑧𝑧 ≼ ω) ↔ (𝐴 𝑥𝑥 ≼ ω)))
146145elrab 3648 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 𝑥𝑥 ≼ ω)))
147146simprbi 497 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → (𝐴 𝑥𝑥 ≼ ω))
148147simpld 494 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥)
149148a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥))
150149anim1d 612 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
151150reximdv 3153 . . . . . . . . . . . . 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 3236 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
156 unieq 4876 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → 𝑥 = (𝑔𝑦))
157156sseq2d 3968 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (𝐴 𝑥𝐴 (𝑔𝑦)))
158 esumeq1 34211 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
159158breq1d 5110 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
160157, 159anbi12d 633 . . . . . . . . . . 11 (𝑥 = (𝑔𝑦) → ((𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
161160ac6sg 10410 . . . . . . . . . 10 (𝑋 ∈ V → (∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))))
162161imp 406 . . . . . . . . 9 ((𝑋 ∈ V ∧ ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
16312, 155, 162syl2anc 585 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
1649ad2antrr 727 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
16538ralrimiva 3130 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦𝑋 𝐴 dom 𝑅)
166 iunss 5002 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀𝑦𝑋 𝐴 dom 𝑅)
167165, 166sylibr 234 . . . . . . . . . . . . . . . . 17 (𝜑 𝑦𝑋 𝐴 dom 𝑅)
16842ralrimiva 3130 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦𝑋 𝐴 ∈ V)
169 iunexg 7917 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 𝐴 ∈ V) → 𝑦𝑋 𝐴 ∈ V)
17011, 168, 169syl2anc 585 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑦𝑋 𝐴 ∈ V)
171 elpwg 4559 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
172170, 171syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
173167, 172mpbird 257 . . . . . . . . . . . . . . . 16 (𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅)
17432, 173ffvelcdmd 7039 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ (0[,]+∞))
175105, 174sselid 3933 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
176164, 175syl 17 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
177 simplr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
17825ad4antr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
179177, 178fexd 7183 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 ∈ V)
180 rnexg 7854 . . . . . . . . . . . . . . . 16 (𝑔 ∈ V → ran 𝑔 ∈ V)
181 uniexg 7695 . . . . . . . . . . . . . . . 16 (ran 𝑔 ∈ V → ran 𝑔 ∈ V)
182179, 180, 1813syl 18 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ V)
183 simp-5l 785 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
18427ad2antrr 727 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
185 frn 6677 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
186 ssrab2 4034 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
187185, 186sstrdi 3948 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
188187unissd 4875 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 𝒫 dom 𝑅)
189 unipw 5405 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 dom 𝑅 = dom 𝑅
190188, 189sseqtrdi 3976 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
191190adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ⊆ dom 𝑅)
19235adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
193191, 192sseqtrd 3972 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔𝑄)
194193sselda 3935 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑐𝑄)
195184, 194ffvelcdmd 7039 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → (𝑅𝑐) ∈ (0[,]+∞))
196195ralrimiva 3130 . . . . . . . . . . . . . . . 16 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
197183, 177, 196syl2anc 585 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
198 nfcv 2899 . . . . . . . . . . . . . . . 16 𝑐 ran 𝑔
199198esumcl 34207 . . . . . . . . . . . . . . 15 (( ran 𝑔 ∈ V ∧ ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
200182, 197, 199syl2anc 585 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
201105, 200sselid 3933 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*)
202 simp-5r 786 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
203202rexrd 11194 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*)
204 simpllr 776 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ+)
205204rpxrd 12962 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ*)
206203, 205xaddcld 13228 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) ∈ ℝ*)
207185ad2antlr 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
208 sstr 3944 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
209186, 208mpan2 692 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
210 sspwuni 5057 . . . . . . . . . . . . . . . . . . . . . . 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 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑔 Fn 𝑋)
214213ad2antlr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 Fn 𝑋)
215164, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ≼ ω)
216 fnct 10459 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 Fn 𝑋𝑋 ≼ ω) → 𝑔 ≼ ω)
217 rnct 10447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 ≼ ω → ran 𝑔 ≼ ω)
218216, 217syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 Fn 𝑋𝑋 ≼ ω) → ran 𝑔 ≼ ω)
219 dfss3 3924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
220219biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
221 breq1 5103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
222221elrab 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω))
223222simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑤 ≼ ω)
224223ralimi 3075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
225220, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
226 unictb 10498 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ran 𝑔 ≼ ω)
227218, 225, 226syl2an 597 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn 𝑋𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ≼ ω)
228214, 215, 207, 227syl21anc 838 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ≼ ω)
229 ctex 8912 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V)
230 elpwg 4559 . . . . . . . . . . . . . . . . . . . . . 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 3075 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 𝐴 (𝑔𝑦))
235 fvssunirn 6873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔𝑦) ⊆ ran 𝑔
236235unissi 4874 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔𝑦) ⊆ ran 𝑔
237 sstr 3944 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 (𝑔𝑦) ∧ (𝑔𝑦) ⊆ ran 𝑔) → 𝐴 ran 𝑔)
238236, 237mpan2 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 (𝑔𝑦) → 𝐴 ran 𝑔)
239238ralimi 3075 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑋 𝐴 (𝑔𝑦) → ∀𝑦𝑋 𝐴 ran 𝑔)
240 iunss 5002 . . . . . . . . . . . . . . . . . . . . . . 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 4876 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ran 𝑔 𝑧 = ran 𝑔)
246245sseq2d 3968 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔))
247 breq1 5103 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → (𝑧 ≼ ω ↔ ran 𝑔 ≼ ω))
248246, 247anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ran 𝑔 → (( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
249248elrab 3648 . . . . . . . . . . . . . . . . . . 19 ( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
250244, 249sylibr 234 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)})
251 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑤 → (𝑅𝑐) = (𝑅𝑤))
252251cbvesumv 34220 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)
253 esumeq1 34211 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝑔 → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
254253rspceeqv 3601 . . . . . . . . . . . . . . . . . 18 (( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
255250, 252, 254sylancl 587 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
256 esumex 34206 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ V
257 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
258257elrnmpt 5915 . . . . . . . . . . . . . . . . . 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 34472 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
26326, 27, 173, 262syl3anc 1374 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
264 xrge0infss 32850 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
265263, 264syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
266261, 265inflb 9405 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
26729fveq1i 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑀 𝑦𝑋 𝐴) = ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴)
268167, 36sseqtrd 3972 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝑦𝑋 𝐴 𝑄)
269 omsfval 34471 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 𝑄) → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
27026, 27, 268, 269syl3anc 1374 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
271267, 270eqtrid 2784 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
272271breq2d 5112 . . . . . . . . . . . . . . . . . 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 11209 . . . . . . . . . . . . . . 15 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
279176, 201, 278syl2anc 585 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
280277, 279mpbird 257 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐))
281 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
28222, 281nfan 1901 . . . . . . . . . . . . . . . . . 18 𝑦((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
283 nfra1 3262 . . . . . . . . . . . . . . . . . 18 𝑦𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
284282, 283nfan 1901 . . . . . . . . . . . . . . . . 17 𝑦(((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
285 simp-6l 787 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝜑)
286 simpllr 776 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
287 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑦𝑋)
28827ad3antrrr 731 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
289 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
290 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑦𝑋)
291289, 290ffvelcdmd 7039 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
292186, 291sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ 𝒫 dom 𝑅)
293292elpwid 4565 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ dom 𝑅)
294288, 293fssdmd 6688 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ 𝑄)
295 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤 ∈ (𝑔𝑦))
296294, 295sseldd 3936 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤𝑄)
297288, 296ffvelcdmd 7039 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑅𝑤) ∈ (0[,]+∞))
298297ralrimiva 3130 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
299 fvex 6855 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑦) ∈ V
300 nfcv 2899 . . . . . . . . . . . . . . . . . . . . . 22 𝑤(𝑔𝑦)
301300esumcl 34207 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
302299, 301mpan 691 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
303298, 302syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
304285, 286, 287, 303syl21anc 838 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
305304ex 412 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)))
306284, 305ralrimi 3236 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
30714esumcl 34207 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
308178, 306, 307syl2anc 585 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
309105, 308sselid 3933 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
310 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑤(𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
311 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
312 fniunfv 7203 . . . . . . . . . . . . . . . . . . . 20 (𝑔 Fn 𝑋 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
313311, 213, 3123syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
314310, 313esumeq1d 34212 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
31511adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑋 ∈ V)
316299a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑔𝑦) ∈ V)
317315, 316, 297esumiun 34271 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
318314, 317eqbrtrrd 5124 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
3199, 318sylan 581 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
320319adantr 480 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
321252, 320eqbrtrid 5135 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
322285, 287, 46syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
323 simplll 775 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+))
324323, 287, 73syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
325322, 324xrge0addcld 32852 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
326325ex 412 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)))
327284, 326ralrimi 3236 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
32814esumcl 34207 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
329178, 327, 328syl2anc 585 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
330105, 329sselid 3933 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
331215, 10syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
332 simp-4l 783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ))
333 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑦𝑋)
334332, 333, 49syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
335334adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑀𝐴) ∈ ℝ)
33665adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5112 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
341340biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
342335, 337, 339, 341syl21anc 838 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
343342ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
344332simpld 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝜑)
345 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
346344, 345, 333, 303syl21anc 838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
347105, 346sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
348334rexrd 11194 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ*)
349336rexrd 11194 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
350348, 349xaddcld 13228 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
351 xrltle 13075 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ* ∧ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
352347, 350, 351syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 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 3236 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
357 ralim 3078 . . . . . . . . . . . . . . . . . . 19 (∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
358356, 357syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
359358imp 406 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
360359r19.21bi 3230 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
361284, 14, 331, 304, 325, 360esumlef 34239 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
362164, 46sylan 581 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
363284, 14, 331, 362, 324esumaddf 34238 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))))
364324ex 412 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)))
365284, 364ralrimi 3236 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
36614esumcl 34207 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
367178, 365, 366syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
368105, 367sselid 3933 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
369 simp-4r 784 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑓:𝑋1-1→ℕ)
370 vex 3446 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
371370rnex 7862 . . . . . . . . . . . . . . . . . . . . . . 23 ran 𝑓 ∈ V
372371a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V)
37358frnd 6678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 ⊆ ℕ)
374373adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
375374sselda 3935 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
37654a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
377 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
378377nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
379376, 378rpexpcld 14182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
380379rpreccld 12971 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
38171, 380sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
382381adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
383375, 382syldan 592 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
384383ralrimiva 3130 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
385 nfcv 2899 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧ran 𝑓
386385esumcl 34207 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
387372, 384, 386syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
388105, 387sselid 3933 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
389 1xr 11203 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
390389a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
39171sseli 3931 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+𝑒 ∈ (0[,]+∞))
392391adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
393 elxrge0 13385 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
394392, 393sylib 218 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
395 nfv 1916 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧(𝜑𝑓:𝑋1-1→ℕ)
396 nnex 12163 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ ∈ V
397396a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → ℕ ∈ V)
398395, 397, 381, 373esummono 34231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
399 oveq2 7376 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
400399oveq2d 7384 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
401 ioossico 13366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0(,)+∞) ⊆ (0[,)+∞)
40269, 401eqsstri 3982 . . . . . . . . . . . . . . . . . . . . . . . . 25 + ⊆ (0[,)+∞)
403402, 380sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
404 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
405 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
406405oveq2d 7384 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
407406oveq2d 7384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
408 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
409 ovexd 7403 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
410404, 407, 408, 409fvmptd 6957 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
411410adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
412 ax-1cn 11096 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
413 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
414413geo2lim 15810 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11144 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
418417a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 1 ∈ ℝ)
419400, 403, 411, 416, 418esumcvgsum 34265 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
420 geoihalfsum 15817 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
421419, 420eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
422398, 421breqtrd 5126 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
423422adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
424 xlemul2a 13216 . . . . . . . . . . . . . . . . . . . 20 (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
425388, 390, 394, 423, 424syl31anc 1376 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
42613, 19nfan 1901 . . . . . . . . . . . . . . . . . . . . . 22 𝑦(𝜑𝑓:𝑋1-1→ℕ)
427426, 21nfan 1901 . . . . . . . . . . . . . . . . . . . . 21 𝑦((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
42876recnd 11172 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℂ)
42978recnd 11172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
430429adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
431 2cn 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
432431a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℂ)
433 2ne0 12261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≠ 0
434433a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ≠ 0)
435432, 434, 60expne0d 14087 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
436435adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
437428, 430, 436divrecd 11932 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
438 1rp 12921 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℝ+
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 1 ∈ ℝ+)
440439, 61rpdivcld 12978 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ+)
44152, 440sselid 3933 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
442441adantlr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
443 rexmul 13198 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
44476, 442, 443syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
445437, 444eqtr4d 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
446445ralrimiva 3130 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
447427, 446esumeq2d 34214 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
44811ad2antrr 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
44971, 440sselid 3933 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
450449adantlr 716 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
451402a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
452451sselda 3935 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
453448, 450, 452esummulc2 34259 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
454 nfcv 2899 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦(1 / (2↑𝑧))
455 oveq2 7376 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑓𝑦) → (2↑𝑧) = (2↑(𝑓𝑦)))
456455oveq2d 7384 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑓𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓𝑦))))
45711adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑋 ∈ V)
45856simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → Fun 𝑓)
45957feqmptd 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
460459cnveqd 5832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
461460funeqd 6522 . . . . . . . . . . . . . . . . . . . . . . . . . 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 34228 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
465 ffn 6670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
466 fnrnfv 6901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
46758, 465, 4663syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
468395, 467esumeq1d 34212 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
469464, 468eqtr4d 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
470469adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
471470oveq2d 7384 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
472447, 453, 4713eqtr2rd 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))))
473394simpld 494 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
474 xmulrid 13206 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
475473, 474syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
476425, 472, 4753brtr3d 5131 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
477164, 369, 204, 476syl21anc 838 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
478 xleadd2a 13181 . . . . . . . . . . . . . . . . 17 (((Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*) ∧ Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
479368, 205, 203, 477, 478syl31anc 1376 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
480363, 479eqbrtrd 5122 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
481309, 330, 206, 361, 480xrletrd 13088 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
482201, 309, 206, 321, 481xrletrd 13088 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
483176, 201, 206, 280, 482xrletrd 13088 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
484204rpred 12961 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ)
485 rexadd 13159 . . . . . . . . . . . . 13 ((Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
486202, 484, 485syl2anc 585 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
487483, 486breqtrd 5126 . . . . . . . . . . 11 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
488487anasss 466 . . . . . . . . . 10 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
489488ex 412 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
490489exlimdv 1935 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
491163, 490mpd 15 . . . . . . 7 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
492491ralrimiva 3130 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
493 xralrple 13132 . . . . . . . 8 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
494175, 493sylan 581 . . . . . . 7 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
495494adantr 480 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
496492, 495mpbird 257 . . . . 5 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
497496ex 412 . . . 4 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
498497exlimdv 1935 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
4998, 498mpd 15 . 2 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
500175adantr 480 . . . 4 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
501 pnfge 13056 . . . 4 ((𝑀 𝑦𝑋 𝐴) ∈ ℝ* → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
502500, 501syl 17 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
50346ralrimiva 3130 . . . . 5 (𝜑 → ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞))
50414esumcl 34207 . . . . 5 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
50511, 503, 504syl2anc 585 . . . 4 (𝜑 → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
506 xrge0nre 13381 . . . 4 ((Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
507505, 506sylan 581 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
508502, 507breqtrrd 5128 . 2 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
509499, 508pm2.61dan 813 1 (𝜑 → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1542  wex 1781  wcel 2114  {cab 2715  wne 2933  wral 3052  wrex 3062  {crab 3401  Vcvv 3442  wss 3903  𝒫 cpw 4556   cuni 4865   ciun 4948   class class class wbr 5100  cmpt 5181   Or wor 5539  ccnv 5631  dom cdm 5632  ran crn 5633  Fun wfun 6494   Fn wfn 6495  wf 6496  1-1wf1 6497  cfv 6500  (class class class)co 7368  ωcom 7818  cen 8892  cdom 8893  infcinf 9356  cc 11036  cr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  +∞cpnf 11175  *cxr 11177   < clt 11178  cle 11179   / cdiv 11806  cn 12157  2c2 12212  cz 12500  +crp 12917   +𝑒 cxad 13036   ·e cxmu 13037  (,)cioo 13273  [,)cico 13275  [,]cicc 13276  seqcseq 13936  cexp 13996  cli 15419  Σcsu 15621  Σ*cesum 34204  toOMeascoms 34468
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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-reg 9509  ax-inf2 9562  ax-cc 10357  ax-ac2 10385  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117  ax-mulf 11118
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-fi 9326  df-sup 9357  df-inf 9358  df-oi 9427  df-r1 9688  df-rank 9689  df-card 9863  df-acn 9866  df-ac 10038  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-q 12874  df-rp 12918  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13436  df-fzo 13583  df-fl 13724  df-mod 13802  df-seq 13937  df-exp 13997  df-fac 14209  df-bc 14238  df-hash 14266  df-shft 15002  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-limsup 15406  df-clim 15423  df-rlim 15424  df-sum 15622  df-ef 16002  df-sin 16004  df-cos 16005  df-pi 16007  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-hom 17213  df-cco 17214  df-rest 17354  df-topn 17355  df-0g 17373  df-gsum 17374  df-topgen 17375  df-pt 17376  df-prds 17379  df-ordt 17434  df-xrs 17435  df-qtop 17440  df-imas 17441  df-xps 17443  df-mre 17517  df-mrc 17518  df-acs 17520  df-ps 18501  df-tsr 18502  df-plusf 18576  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-subg 19065  df-cntz 19258  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-ring 20182  df-cring 20183  df-subrng 20491  df-subrg 20515  df-abv 20754  df-lmod 20825  df-scaf 20826  df-sra 21137  df-rgmod 21138  df-psmet 21313  df-xmet 21314  df-met 21315  df-bl 21316  df-mopn 21317  df-fbas 21318  df-fg 21319  df-cnfld 21322  df-top 22850  df-topon 22867  df-topsp 22889  df-bases 22902  df-cld 22975  df-ntr 22976  df-cls 22977  df-nei 23054  df-lp 23092  df-perf 23093  df-cn 23183  df-cnp 23184  df-haus 23271  df-tx 23518  df-hmeo 23711  df-fil 23802  df-fm 23894  df-flim 23895  df-flf 23896  df-tmd 24028  df-tgp 24029  df-tsms 24083  df-trg 24116  df-xms 24276  df-ms 24277  df-tms 24278  df-nm 24538  df-ngp 24539  df-nrg 24541  df-nlm 24542  df-ii 24838  df-cncf 24839  df-limc 25835  df-dv 25836  df-log 26533  df-esum 34205  df-oms 34469
This theorem is referenced by:  omsmeas  34500
  Copyright terms: Public domain W3C validator