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 34311
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 13887 . . . . . . 7 ℕ ≈ ω
32ensymi 8926 . . . . . 6 ω ≈ ℕ
4 domentr 8935 . . . . . 6 ((𝑋 ≼ ω ∧ ω ≈ ℕ) → 𝑋 ≼ ℕ)
51, 3, 4sylancl 586 . . . . 5 (𝜑𝑋 ≼ ℕ)
6 brdomi 8882 . . . . 5 (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋1-1→ℕ)
75, 6syl 17 . . . 4 (𝜑 → ∃𝑓 𝑓:𝑋1-1→ℕ)
87adantr 480 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋1-1→ℕ)
9 simplll 774 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10 ctex 8886 . . . . . . . . . . 11 (𝑋 ≼ ω → 𝑋 ∈ V)
111, 10syl 17 . . . . . . . . . 10 (𝜑𝑋 ∈ V)
129, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13 nfv 1915 . . . . . . . . . . . . 13 𝑦𝜑
14 nfcv 2894 . . . . . . . . . . . . . . 15 𝑦𝑋
1514nfesum1 34051 . . . . . . . . . . . . . 14 𝑦Σ*𝑦𝑋(𝑀𝐴)
16 nfcv 2894 . . . . . . . . . . . . . 14 𝑦
1715, 16nfel 2909 . . . . . . . . . . . . 13 𝑦Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ
1813, 17nfan 1900 . . . . . . . . . . . 12 𝑦(𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
19 nfv 1915 . . . . . . . . . . . 12 𝑦 𝑓:𝑋1-1→ℕ
2018, 19nfan 1900 . . . . . . . . . . 11 𝑦((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ)
21 nfv 1915 . . . . . . . . . . 11 𝑦 𝑒 ∈ ℝ+
2220, 21nfan 1900 . . . . . . . . . 10 𝑦(((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
239adantr 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 34307 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 = (toOMeas‘𝑅)
3029feq1i 6642 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀:𝒫 dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
3128, 30sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3226, 27, 31syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3332adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 𝑄)
3527fdmd 6661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom 𝑅 = 𝑄)
3635unieqd 4872 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 dom 𝑅 = 𝑄)
3736adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → dom 𝑅 = 𝑄)
3834, 37sseqtrrd 3972 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → 𝐴 dom 𝑅)
3926uniexd 7675 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 𝑄 ∈ V)
4039adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑋) → 𝑄 ∈ V)
41 ssexg 5261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 𝑄 𝑄 ∈ V) → 𝐴 ∈ V)
4234, 40, 41syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 ∈ V)
43 elpwg 4553 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ V → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4538, 44mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝐴 ∈ 𝒫 dom 𝑅)
4633, 45ffvelcdmd 7018 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
4746adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
4918, 25, 47, 48esumcvgre 34102 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5049adantlr 715 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5150adantlr 715 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
52 rpssre 12898 . . . . . . . . . . . . . . . . . . 19 + ⊆ ℝ
53 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
54 2rp 12895 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ+
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℝ+)
56 df-f1 6486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun 𝑓))
5756simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → 𝑓:𝑋⟶ℕ)
5857adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑓:𝑋⟶ℕ)
5958ffvelcdmda 7017 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℕ)
6059nnzd 12495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
6155, 60rpexpcld 14154 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6261adantlr 715 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6353, 62rpdivcld 12951 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ+)
6452, 63sselid 3932 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
6564adantl3r 750 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
66 rexadd 13131 . . . . . . . . . . . . . . . . 17 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
6751, 65, 66syl2anc 584 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
689, 46sylan 580 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
69 dfrp2 13294 . . . . . . . . . . . . . . . . . . . 20 + = (0(,)+∞)
70 ioossicc 13333 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
7169, 70eqsstri 3981 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
7271, 63sselid 3932 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7372adantl3r 750 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7468, 73xrge0addcld 32743 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7567, 74eqeltrrd 2832 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7652, 53sselid 3932 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7776adantl3r 750 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7852, 61sselid 3932 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
7978adantlr 715 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8079adantl3r 750 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
81 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
8281rpgt0d 12937 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 𝑒)
83 2re 12199 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
8483a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 2 ∈ ℝ)
8560adantllr 719 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
8685adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
87 2pos 12228 . . . . . . . . . . . . . . . . . . . 20 0 < 2
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 2)
89 expgt0 14002 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ (𝑓𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓𝑦)))
9084, 86, 88, 89syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (2↑(𝑓𝑦)))
9177, 80, 82, 90divgt0d 12057 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (𝑒 / (2↑(𝑓𝑦))))
9265, 51ltaddposd 11701 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (0 < (𝑒 / (2↑(𝑓𝑦))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
9391, 92mpbid 232 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
9429fveq1i 6823 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝐴) = ((toOMeas‘𝑅)‘𝐴)
9526adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑄𝑉)
9627adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑅:𝑄⟶(0[,]+∞))
97 omsfval 34305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9895, 96, 34, 97syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
9994, 98eqtrid 2778 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
1009, 99sylan 580 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
101100eqcomd 2737 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) = (𝑀𝐴))
102101breq1d 5101 . . . . . . . . . . . . . . . 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 13330 . . . . . . . . . . . . . . . . . . 19 (0[,]+∞) ⊆ ℝ*
106 xrltso 13040 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
107 soss 5544 . . . . . . . . . . . . . . . . . . 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 34306 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
11395, 96, 45, 112syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
114 xrge0infss 32741 . . . . . . . . . . . . . . . . 17 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
115113, 114syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
116111, 115infglb 9375 . . . . . . . . . . . . . . 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 2731 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
120 esumex 34040 . . . . . . . . . . . . . . . . . . 19 Σ*𝑤𝑥(𝑅𝑤) ∈ V
121119, 120elrnmpti 5902 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤))
122121anbi1i 624 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
123 r19.41v 3162 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
124122, 123bitr4i 278 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
125124exbii 1849 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
126 df-rex 3057 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
127 rexcom4 3259 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
128125, 126, 1273bitr4i 303 . . . . . . . . . . . . . 14 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
129 breq1 5094 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
130 idd 24 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
131129, 130sylbid 240 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
132131imp 406 . . . . . . . . . . . . . . . 16 ((𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
133132exlimiv 1931 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
134133reximi 3070 . . . . . . . . . . . . . 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 4027 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
140 rexss 4010 . . . . . . . . . . . . . 14 ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
141139, 140ax-mp 5 . . . . . . . . . . . . 13 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
142 unieq 4870 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 𝑧 = 𝑥)
143142sseq2d 3967 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐴 𝑧𝐴 𝑥))
144 breq1 5094 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
145143, 144anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝐴 𝑧𝑧 ≼ ω) ↔ (𝐴 𝑥𝑥 ≼ ω)))
146145elrab 3647 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 𝑥𝑥 ≼ ω)))
147146simprbi 496 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → (𝐴 𝑥𝑥 ≼ ω))
148147simpld 494 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥)
149148a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥))
150149anim1d 611 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
151150reximdv 3147 . . . . . . . . . . . . 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 3230 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
156 unieq 4870 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → 𝑥 = (𝑔𝑦))
157156sseq2d 3967 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (𝐴 𝑥𝐴 (𝑔𝑦)))
158 esumeq1 34045 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
159158breq1d 5101 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
160157, 159anbi12d 632 . . . . . . . . . . 11 (𝑥 = (𝑔𝑦) → ((𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
161160ac6sg 10379 . . . . . . . . . 10 (𝑋 ∈ V → (∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))))
162161imp 406 . . . . . . . . 9 ((𝑋 ∈ V ∧ ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
16312, 155, 162syl2anc 584 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
1649ad2antrr 726 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
16538ralrimiva 3124 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦𝑋 𝐴 dom 𝑅)
166 iunss 4994 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀𝑦𝑋 𝐴 dom 𝑅)
167165, 166sylibr 234 . . . . . . . . . . . . . . . . 17 (𝜑 𝑦𝑋 𝐴 dom 𝑅)
16842ralrimiva 3124 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦𝑋 𝐴 ∈ V)
169 iunexg 7895 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 𝐴 ∈ V) → 𝑦𝑋 𝐴 ∈ V)
17011, 168, 169syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑦𝑋 𝐴 ∈ V)
171 elpwg 4553 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
172170, 171syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
173167, 172mpbird 257 . . . . . . . . . . . . . . . 16 (𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅)
17432, 173ffvelcdmd 7018 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ (0[,]+∞))
175105, 174sselid 3932 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
176164, 175syl 17 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
177 simplr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
17825ad4antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
179177, 178fexd 7161 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 ∈ V)
180 rnexg 7832 . . . . . . . . . . . . . . . 16 (𝑔 ∈ V → ran 𝑔 ∈ V)
181 uniexg 7673 . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
185 frn 6658 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
186 ssrab2 4030 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
187185, 186sstrdi 3947 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
188187unissd 4869 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 𝒫 dom 𝑅)
189 unipw 5391 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 dom 𝑅 = dom 𝑅
190188, 189sseqtrdi 3975 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
191190adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ⊆ dom 𝑅)
19235adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
193191, 192sseqtrd 3971 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔𝑄)
194193sselda 3934 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑐𝑄)
195184, 194ffvelcdmd 7018 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → (𝑅𝑐) ∈ (0[,]+∞))
196195ralrimiva 3124 . . . . . . . . . . . . . . . 16 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
197183, 177, 196syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
198 nfcv 2894 . . . . . . . . . . . . . . . 16 𝑐 ran 𝑔
199198esumcl 34041 . . . . . . . . . . . . . . 15 (( ran 𝑔 ∈ V ∧ ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
200182, 197, 199syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
201105, 200sselid 3932 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*)
202 simp-5r 785 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
203202rexrd 11162 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*)
204 simpllr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ+)
205204rpxrd 12935 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ*)
206203, 205xaddcld 13200 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) ∈ ℝ*)
207185ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
208 sstr 3943 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
209186, 208mpan2 691 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
210 sspwuni 5048 . . . . . . . . . . . . . . . . . . . . . . 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 6651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑔 Fn 𝑋)
214213ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 Fn 𝑋)
215164, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ≼ ω)
216 fnct 10428 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 Fn 𝑋𝑋 ≼ ω) → 𝑔 ≼ ω)
217 rnct 10416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 ≼ ω → ran 𝑔 ≼ ω)
218216, 217syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 Fn 𝑋𝑋 ≼ ω) → ran 𝑔 ≼ ω)
219 dfss3 3923 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
220219biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
221 breq1 5094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
222221elrab 3647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω))
223222simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑤 ≼ ω)
224223ralimi 3069 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
225220, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
226 unictb 10466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ran 𝑔 ≼ ω)
227218, 225, 226syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn 𝑋𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ≼ ω)
228214, 215, 207, 227syl21anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ≼ ω)
229 ctex 8886 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V)
230 elpwg 4553 . . . . . . . . . . . . . . . . . . . . . 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 3069 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 𝐴 (𝑔𝑦))
235 fvssunirn 6853 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔𝑦) ⊆ ran 𝑔
236235unissi 4868 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔𝑦) ⊆ ran 𝑔
237 sstr 3943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 (𝑔𝑦) ∧ (𝑔𝑦) ⊆ ran 𝑔) → 𝐴 ran 𝑔)
238236, 237mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 (𝑔𝑦) → 𝐴 ran 𝑔)
239238ralimi 3069 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑋 𝐴 (𝑔𝑦) → ∀𝑦𝑋 𝐴 ran 𝑔)
240 iunss 4994 . . . . . . . . . . . . . . . . . . . . . . 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 4870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ran 𝑔 𝑧 = ran 𝑔)
246245sseq2d 3967 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔))
247 breq1 5094 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → (𝑧 ≼ ω ↔ ran 𝑔 ≼ ω))
248246, 247anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ran 𝑔 → (( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
249248elrab 3647 . . . . . . . . . . . . . . . . . . 19 ( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
250244, 249sylibr 234 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)})
251 fveq2 6822 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑤 → (𝑅𝑐) = (𝑅𝑤))
252251cbvesumv 34054 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)
253 esumeq1 34045 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝑔 → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
254253rspceeqv 3600 . . . . . . . . . . . . . . . . . 18 (( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
255250, 252, 254sylancl 586 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
256 esumex 34040 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ V
257 eqid 2731 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
258257elrnmpt 5898 . . . . . . . . . . . . . . . . . 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 34306 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
26326, 27, 173, 262syl3anc 1373 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
264 xrge0infss 32741 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
265263, 264syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
266261, 265inflb 9374 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
26729fveq1i 6823 . . . . . . . . . . . . . . . . . . . 20 (𝑀 𝑦𝑋 𝐴) = ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴)
268167, 36sseqtrd 3971 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝑦𝑋 𝐴 𝑄)
269 omsfval 34305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 𝑄) → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
27026, 27, 268, 269syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
271267, 270eqtrid 2778 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
272271breq2d 5103 . . . . . . . . . . . . . . . . . 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 11177 . . . . . . . . . . . . . . 15 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
279176, 201, 278syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
280277, 279mpbird 257 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐))
281 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
28222, 281nfan 1900 . . . . . . . . . . . . . . . . . 18 𝑦((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
283 nfra1 3256 . . . . . . . . . . . . . . . . . 18 𝑦𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
284282, 283nfan 1900 . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
289 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
290 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑦𝑋)
291289, 290ffvelcdmd 7018 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
292186, 291sselid 3932 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ 𝒫 dom 𝑅)
293292elpwid 4559 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ dom 𝑅)
294288, 293fssdmd 6669 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ 𝑄)
295 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤 ∈ (𝑔𝑦))
296294, 295sseldd 3935 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤𝑄)
297288, 296ffvelcdmd 7018 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑅𝑤) ∈ (0[,]+∞))
298297ralrimiva 3124 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
299 fvex 6835 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑦) ∈ V
300 nfcv 2894 . . . . . . . . . . . . . . . . . . . . . 22 𝑤(𝑔𝑦)
301300esumcl 34041 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
302299, 301mpan 690 . . . . . . . . . . . . . . . . . . . 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 3230 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
30714esumcl 34041 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
308178, 306, 307syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
309105, 308sselid 3932 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
310 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑤(𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
311 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
312 fniunfv 7181 . . . . . . . . . . . . . . . . . . . 20 (𝑔 Fn 𝑋 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
313311, 213, 3123syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
314310, 313esumeq1d 34046 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
31511adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑋 ∈ V)
316299a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑔𝑦) ∈ V)
317315, 316, 297esumiun 34105 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
318314, 317eqbrtrrd 5115 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
3199, 318sylan 580 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
320319adantr 480 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
321252, 320eqbrtrid 5126 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
322285, 287, 46syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
323 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+))
324323, 287, 73syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
325322, 324xrge0addcld 32743 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
326325ex 412 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)))
327284, 326ralrimi 3230 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
32814esumcl 34041 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
329178, 327, 328syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
330105, 329sselid 3932 . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
335334adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑀𝐴) ∈ ℝ)
33665adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5103 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3932 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
348334rexrd 11162 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ*)
349336rexrd 11162 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
350348, 349xaddcld 13200 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
351 xrltle 13048 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ* ∧ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
352347, 350, 351syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 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 3230 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
357 ralim 3072 . . . . . . . . . . . . . . . . . . 19 (∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
358356, 357syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
359358imp 406 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
360359r19.21bi 3224 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
361284, 14, 331, 304, 325, 360esumlef 34073 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
362164, 46sylan 580 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
363284, 14, 331, 362, 324esumaddf 34072 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))))
364324ex 412 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)))
365284, 364ralrimi 3230 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
36614esumcl 34041 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
367178, 365, 366syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
368105, 367sselid 3932 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
369 simp-4r 783 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑓:𝑋1-1→ℕ)
370 vex 3440 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
371370rnex 7840 . . . . . . . . . . . . . . . . . . . . . . 23 ran 𝑓 ∈ V
372371a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V)
37358frnd 6659 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 ⊆ ℕ)
374373adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
375374sselda 3934 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
37654a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
377 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
378377nnzd 12495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
379376, 378rpexpcld 14154 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
380379rpreccld 12944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
38171, 380sselid 3932 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
382381adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
383375, 382syldan 591 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
384383ralrimiva 3124 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
385 nfcv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧ran 𝑓
386385esumcl 34041 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
387372, 384, 386syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
388105, 387sselid 3932 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
389 1xr 11171 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
390389a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
39171sseli 3930 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+𝑒 ∈ (0[,]+∞))
392391adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
393 elxrge0 13357 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
394392, 393sylib 218 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
395 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧(𝜑𝑓:𝑋1-1→ℕ)
396 nnex 12131 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ ∈ V
397396a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → ℕ ∈ V)
398395, 397, 381, 373esummono 34065 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
399 oveq2 7354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
400399oveq2d 7362 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
401 ioossico 13338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0(,)+∞) ⊆ (0[,)+∞)
40269, 401eqsstri 3981 . . . . . . . . . . . . . . . . . . . . . . . . 25 + ⊆ (0[,)+∞)
403402, 380sselid 3932 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
404 eqidd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
405 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
406405oveq2d 7362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
407406oveq2d 7362 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
408 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
409 ovexd 7381 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
410404, 407, 408, 409fvmptd 6936 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
411410adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
412 ax-1cn 11064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
413 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
414413geo2lim 15782 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11112 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
418417a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 1 ∈ ℝ)
419400, 403, 411, 416, 418esumcvgsum 34099 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
420 geoihalfsum 15789 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
421419, 420eqtrdi 2782 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
422398, 421breqtrd 5117 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
423422adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
424 xlemul2a 13188 . . . . . . . . . . . . . . . . . . . 20 (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
425388, 390, 394, 423, 424syl31anc 1375 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
42613, 19nfan 1900 . . . . . . . . . . . . . . . . . . . . . 22 𝑦(𝜑𝑓:𝑋1-1→ℕ)
427426, 21nfan 1900 . . . . . . . . . . . . . . . . . . . . 21 𝑦((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
42876recnd 11140 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℂ)
42978recnd 11140 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
430429adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
431 2cn 12200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
432431a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℂ)
433 2ne0 12229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≠ 0
434433a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ≠ 0)
435432, 434, 60expne0d 14059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
436435adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
437428, 430, 436divrecd 11900 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
438 1rp 12894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℝ+
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 1 ∈ ℝ+)
440439, 61rpdivcld 12951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ+)
44152, 440sselid 3932 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
442441adantlr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
443 rexmul 13170 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
44476, 442, 443syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
445437, 444eqtr4d 2769 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
446445ralrimiva 3124 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
447427, 446esumeq2d 34048 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
44811ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
44971, 440sselid 3932 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
450449adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
451402a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
452451sselda 3934 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
453448, 450, 452esummulc2 34093 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
454 nfcv 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦(1 / (2↑𝑧))
455 oveq2 7354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑓𝑦) → (2↑𝑧) = (2↑(𝑓𝑦)))
456455oveq2d 7362 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑓𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓𝑦))))
45711adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑋 ∈ V)
45856simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → Fun 𝑓)
45957feqmptd 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
460459cnveqd 5815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
461460funeqd 6503 . . . . . . . . . . . . . . . . . . . . . . . . . 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 34062 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
465 ffn 6651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
466 fnrnfv 6881 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
46758, 465, 4663syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
468395, 467esumeq1d 34046 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
469464, 468eqtr4d 2769 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
470469adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
471470oveq2d 7362 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
472447, 453, 4713eqtr2rd 2773 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))))
473394simpld 494 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
474 xmulrid 13178 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
475473, 474syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
476425, 472, 4753brtr3d 5122 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
477164, 369, 204, 476syl21anc 837 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
478 xleadd2a 13153 . . . . . . . . . . . . . . . . 17 (((Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*) ∧ Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
479368, 205, 203, 477, 478syl31anc 1375 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
480363, 479eqbrtrd 5113 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
481309, 330, 206, 361, 480xrletrd 13061 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
482201, 309, 206, 321, 481xrletrd 13061 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
483176, 201, 206, 280, 482xrletrd 13061 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
484204rpred 12934 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ)
485 rexadd 13131 . . . . . . . . . . . . 13 ((Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
486202, 484, 485syl2anc 584 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
487483, 486breqtrd 5117 . . . . . . . . . . 11 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
488487anasss 466 . . . . . . . . . 10 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
489488ex 412 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
490489exlimdv 1934 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
491163, 490mpd 15 . . . . . . 7 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
492491ralrimiva 3124 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
493 xralrple 13104 . . . . . . . 8 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
494175, 493sylan 580 . . . . . . 7 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
495494adantr 480 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
496492, 495mpbird 257 . . . . 5 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
497496ex 412 . . . 4 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
498497exlimdv 1934 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
4998, 498mpd 15 . 2 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
500175adantr 480 . . . 4 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
501 pnfge 13029 . . . 4 ((𝑀 𝑦𝑋 𝐴) ∈ ℝ* → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
502500, 501syl 17 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
50346ralrimiva 3124 . . . . 5 (𝜑 → ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞))
50414esumcl 34041 . . . . 5 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
50511, 503, 504syl2anc 584 . . . 4 (𝜑 → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
506 xrge0nre 13353 . . . 4 ((Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
507505, 506sylan 580 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
508502, 507breqtrrd 5119 . 2 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
509499, 508pm2.61dan 812 1 (𝜑 → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1541  wex 1780  wcel 2111  {cab 2709  wne 2928  wral 3047  wrex 3056  {crab 3395  Vcvv 3436  wss 3902  𝒫 cpw 4550   cuni 4859   ciun 4941   class class class wbr 5091  cmpt 5172   Or wor 5523  ccnv 5615  dom cdm 5616  ran crn 5617  Fun wfun 6475   Fn wfn 6476  wf 6477  1-1wf1 6478  cfv 6481  (class class class)co 7346  ωcom 7796  cen 8866  cdom 8867  infcinf 9325  cc 11004  cr 11005  0cc0 11006  1c1 11007   + caddc 11009   · cmul 11011  +∞cpnf 11143  *cxr 11145   < clt 11146  cle 11147   / cdiv 11774  cn 12125  2c2 12180  cz 12468  +crp 12890   +𝑒 cxad 13009   ·e cxmu 13010  (,)cioo 13245  [,)cico 13247  [,]cicc 13248  seqcseq 13908  cexp 13968  cli 15391  Σcsu 15593  Σ*cesum 34038  toOMeascoms 34302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-reg 9478  ax-inf2 9531  ax-cc 10326  ax-ac2 10354  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084  ax-addf 11085  ax-mulf 11086
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-tp 4581  df-op 4583  df-uni 4860  df-int 4898  df-iun 4943  df-iin 4944  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-se 5570  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7610  df-om 7797  df-1st 7921  df-2nd 7922  df-supp 8091  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-oadd 8389  df-er 8622  df-map 8752  df-pm 8753  df-ixp 8822  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-fsupp 9246  df-fi 9295  df-sup 9326  df-inf 9327  df-oi 9396  df-r1 9657  df-rank 9658  df-card 9832  df-acn 9835  df-ac 10007  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194  df-9 12195  df-n0 12382  df-xnn0 12455  df-z 12469  df-dec 12589  df-uz 12733  df-q 12847  df-rp 12891  df-xneg 13011  df-xadd 13012  df-xmul 13013  df-ioo 13249  df-ioc 13250  df-ico 13251  df-icc 13252  df-fz 13408  df-fzo 13555  df-fl 13696  df-mod 13774  df-seq 13909  df-exp 13969  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14974  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-limsup 15378  df-clim 15395  df-rlim 15396  df-sum 15594  df-ef 15974  df-sin 15976  df-cos 15977  df-pi 15979  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-starv 17176  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-unif 17184  df-hom 17185  df-cco 17186  df-rest 17326  df-topn 17327  df-0g 17345  df-gsum 17346  df-topgen 17347  df-pt 17348  df-prds 17351  df-ordt 17405  df-xrs 17406  df-qtop 17411  df-imas 17412  df-xps 17414  df-mre 17488  df-mrc 17489  df-acs 17491  df-ps 18472  df-tsr 18473  df-plusf 18547  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-mhm 18691  df-submnd 18692  df-grp 18849  df-minusg 18850  df-sbg 18851  df-mulg 18981  df-subg 19036  df-cntz 19230  df-cmn 19695  df-abl 19696  df-mgp 20060  df-rng 20072  df-ur 20101  df-ring 20154  df-cring 20155  df-subrng 20462  df-subrg 20486  df-abv 20725  df-lmod 20796  df-scaf 20797  df-sra 21108  df-rgmod 21109  df-psmet 21284  df-xmet 21285  df-met 21286  df-bl 21287  df-mopn 21288  df-fbas 21289  df-fg 21290  df-cnfld 21293  df-top 22810  df-topon 22827  df-topsp 22849  df-bases 22862  df-cld 22935  df-ntr 22936  df-cls 22937  df-nei 23014  df-lp 23052  df-perf 23053  df-cn 23143  df-cnp 23144  df-haus 23231  df-tx 23478  df-hmeo 23671  df-fil 23762  df-fm 23854  df-flim 23855  df-flf 23856  df-tmd 23988  df-tgp 23989  df-tsms 24043  df-trg 24076  df-xms 24236  df-ms 24237  df-tms 24238  df-nm 24498  df-ngp 24499  df-nrg 24501  df-nlm 24502  df-ii 24798  df-cncf 24799  df-limc 25795  df-dv 25796  df-log 26493  df-esum 34039  df-oms 34303
This theorem is referenced by:  omsmeas  34334
  Copyright terms: Public domain W3C validator