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 30362
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 12779 . . . . . . 7 ℕ ≈ ω
32ensymi 8006 . . . . . 6 ω ≈ ℕ
4 domentr 8015 . . . . . 6 ((𝑋 ≼ ω ∧ ω ≈ ℕ) → 𝑋 ≼ ℕ)
51, 3, 4sylancl 694 . . . . 5 (𝜑𝑋 ≼ ℕ)
6 brdomi 7966 . . . . 5 (𝑋 ≼ ℕ → ∃𝑓 𝑓:𝑋1-1→ℕ)
75, 6syl 17 . . . 4 (𝜑 → ∃𝑓 𝑓:𝑋1-1→ℕ)
87adantr 481 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋1-1→ℕ)
9 simplll 798 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑)
10 ctex 7970 . . . . . . . . . . 11 (𝑋 ≼ ω → 𝑋 ∈ V)
111, 10syl 17 . . . . . . . . . 10 (𝜑𝑋 ∈ V)
129, 11syl 17 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
13 nfv 1843 . . . . . . . . . . . . 13 𝑦𝜑
14 nfcv 2764 . . . . . . . . . . . . . . 15 𝑦𝑋
1514nfesum1 30102 . . . . . . . . . . . . . 14 𝑦Σ*𝑦𝑋(𝑀𝐴)
16 nfcv 2764 . . . . . . . . . . . . . 14 𝑦
1715, 16nfel 2777 . . . . . . . . . . . . 13 𝑦Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ
1813, 17nfan 1828 . . . . . . . . . . . 12 𝑦(𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
19 nfv 1843 . . . . . . . . . . . 12 𝑦 𝑓:𝑋1-1→ℕ
2018, 19nfan 1828 . . . . . . . . . . 11 𝑦((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ)
21 nfv 1843 . . . . . . . . . . 11 𝑦 𝑒 ∈ ℝ+
2220, 21nfan 1828 . . . . . . . . . 10 𝑦(((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
239adantr 481 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝜑)
24 simpr 477 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑦𝑋)
2511adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → 𝑋 ∈ V)
26 oms.o . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄𝑉)
27 oms.r . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅:𝑄⟶(0[,]+∞))
28 omsf 30358 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
29 oms.m . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 = (toOMeas‘𝑅)
3029feq1i 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀:𝒫 dom 𝑅⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
3128, 30sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3226, 27, 31syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
3332adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝑀:𝒫 dom 𝑅⟶(0[,]+∞))
34 omssubadd.a . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 𝑄)
35 fdm 6051 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄)
3627, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → dom 𝑅 = 𝑄)
3736unieqd 4446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 dom 𝑅 = 𝑄)
3837adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → dom 𝑅 = 𝑄)
3934, 38sseqtr4d 3642 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → 𝐴 dom 𝑅)
40 uniexg 6955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄𝑉 𝑄 ∈ V)
4126, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 𝑄 ∈ V)
4241adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦𝑋) → 𝑄 ∈ V)
43 ssexg 4804 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 𝑄 𝑄 ∈ V) → 𝐴 ∈ V)
4434, 42, 43syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦𝑋) → 𝐴 ∈ V)
45 elpwg 4166 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ V → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦𝑋) → (𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅))
4739, 46mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦𝑋) → 𝐴 ∈ 𝒫 dom 𝑅)
4833, 47ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
4948adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
50 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
5118, 25, 49, 50esumcvgre 30153 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5251adantlr 751 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
5352adantlr 751 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
54 rpssre 11843 . . . . . . . . . . . . . . . . . . 19 + ⊆ ℝ
55 simplr 792 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
56 2rp 11837 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ+
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℝ+)
58 df-f1 5893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun 𝑓))
5958simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → 𝑓:𝑋⟶ℕ)
6059adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑓:𝑋⟶ℕ)
6160ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℕ)
6261nnzd 11481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
6357, 62rpexpcld 13032 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6463adantlr 751 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ+)
6555, 64rpdivcld 11889 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ+)
6654, 65sseldi 3601 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
6766adantl3r 786 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
68 rexadd 12063 . . . . . . . . . . . . . . . . 17 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
6953, 67, 68syl2anc 693 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
709, 48sylan 488 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
71 dfrp2 29532 . . . . . . . . . . . . . . . . . . . 20 + = (0(,)+∞)
72 ioossicc 12259 . . . . . . . . . . . . . . . . . . . 20 (0(,)+∞) ⊆ (0[,]+∞)
7371, 72eqsstri 3635 . . . . . . . . . . . . . . . . . . 19 + ⊆ (0[,]+∞)
7473, 65sseldi 3601 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7574adantl3r 786 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
7670, 75xrge0addcld 29527 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7769, 76eqeltrrd 2702 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
7854, 55sseldi 3601 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
7978adantl3r 786 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ)
8054, 63sseldi 3601 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8180adantlr 751 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
8281adantl3r 786 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℝ)
83 simplr 792 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℝ+)
8483rpgt0d 11875 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 𝑒)
85 2re 11090 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
8685a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 2 ∈ ℝ)
8762adantllr 755 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
8887adantlr 751 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑓𝑦) ∈ ℤ)
89 2pos 11112 . . . . . . . . . . . . . . . . . . . 20 0 < 2
9089a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < 2)
91 expgt0 12893 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ (𝑓𝑦) ∈ ℤ ∧ 0 < 2) → 0 < (2↑(𝑓𝑦)))
9286, 88, 90, 91syl3anc 1326 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (2↑(𝑓𝑦)))
9379, 82, 84, 92divgt0d 10959 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 0 < (𝑒 / (2↑(𝑓𝑦))))
9467, 53ltaddposd 10611 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (0 < (𝑒 / (2↑(𝑓𝑦))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
9593, 94mpbid 222 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
9629fveq1i 6192 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝐴) = ((toOMeas‘𝑅)‘𝐴)
9726adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑄𝑉)
9827adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦𝑋) → 𝑅:𝑄⟶(0[,]+∞))
99 omsfval 30356 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
10097, 98, 34, 99syl3anc 1326 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
10196, 100syl5eq 2668 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
1029, 101sylan 488 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑀𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
103102eqcomd 2628 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) = (𝑀𝐴))
104103breq1d 4663 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ (𝑀𝐴) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
10595, 104mpbird 247 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
10677, 105jca 554 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
107 iccssxr 12256 . . . . . . . . . . . . . . . . . . 19 (0[,]+∞) ⊆ ℝ*
108 xrltso 11974 . . . . . . . . . . . . . . . . . . 19 < Or ℝ*
109 soss 5053 . . . . . . . . . . . . . . . . . . 19 ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
110107, 108, 109mp2 9 . . . . . . . . . . . . . . . . . 18 < Or (0[,]+∞)
111 biid 251 . . . . . . . . . . . . . . . . . 18 ( < Or (0[,]+∞) ↔ < Or (0[,]+∞))
112110, 111mpbi 220 . . . . . . . . . . . . . . . . 17 < Or (0[,]+∞)
113112a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → < Or (0[,]+∞))
114 omscl 30357 . . . . . . . . . . . . . . . . . 18 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
11597, 98, 47, 114syl3anc 1326 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
116 xrge0infss 29525 . . . . . . . . . . . . . . . . 17 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
117115, 116syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ < 𝑣 ∧ ∀ ∈ (0[,]+∞)(𝑣 < → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < )))
118113, 117infglb 8396 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → ((((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
119118imp 445 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑋) ∧ (((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞) ∧ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
12023, 24, 106, 119syl21anc 1325 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
121 eqid 2622 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
122 esumex 30091 . . . . . . . . . . . . . . . . . . 19 Σ*𝑤𝑥(𝑅𝑤) ∈ V
123121, 122elrnmpti 5376 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤))
124123anbi1i 731 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
125 r19.41v 3089 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
126124, 125bitr4i 267 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
127126exbii 1774 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
128 df-rex 2918 . . . . . . . . . . . . . . 15 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
129 rexcom4 3225 . . . . . . . . . . . . . . 15 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ ∃𝑢𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} (𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
130127, 128, 1293bitr4i 292 . . . . . . . . . . . . . 14 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
131 breq1 4656 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
132 idd 24 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
133131, 132sylbid 230 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ*𝑤𝑥(𝑅𝑤) → (𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
134133imp 445 . . . . . . . . . . . . . . . 16 ((𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
135134exlimiv 1858 . . . . . . . . . . . . . . 15 (∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
136135reximi 3011 . . . . . . . . . . . . . 14 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤𝑥(𝑅𝑤) ∧ 𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
137130, 136sylbi 207 . . . . . . . . . . . . 13 (∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
138120, 137syl 17 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
139 simpr 477 . . . . . . . . . . . . . . . 16 ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω)
140139a1i 11 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 𝑧𝑧 ≼ ω) → 𝑧 ≼ ω))
141140ss2rabi 3684 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
142 rexss 3669 . . . . . . . . . . . . . 14 ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
143141, 142ax-mp 5 . . . . . . . . . . . . 13 (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
144 unieq 4444 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 𝑧 = 𝑥)
145144sseq2d 3633 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐴 𝑧𝐴 𝑥))
146 breq1 4656 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω))
147145, 146anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝐴 𝑧𝑧 ≼ ω) ↔ (𝐴 𝑥𝑥 ≼ ω)))
148147elrab 3363 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 𝑥𝑥 ≼ ω)))
149148simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → (𝐴 𝑥𝑥 ≼ ω))
150149simpld 475 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥)
151150a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} → 𝐴 𝑥))
152151anim1d 588 . . . . . . . . . . . . . 14 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
153152reximdv 3016 . . . . . . . . . . . . 13 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
154143, 153syl5bi 232 . . . . . . . . . . . 12 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 𝑧𝑧 ≼ ω)}Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
155138, 154mpd 15 . . . . . . . . . . 11 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
156155ex 450 . . . . . . . . . 10 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
15722, 156ralrimi 2957 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
158 unieq 4444 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → 𝑥 = (𝑔𝑦))
159158sseq2d 3633 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (𝐴 𝑥𝐴 (𝑔𝑦)))
160 esumeq1 30096 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑦) → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
161160breq1d 4663 . . . . . . . . . . . 12 (𝑥 = (𝑔𝑦) → (Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
162159, 161anbi12d 747 . . . . . . . . . . 11 (𝑥 = (𝑔𝑦) → ((𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) ↔ (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
163162ac6sg 9310 . . . . . . . . . 10 (𝑋 ∈ V → (∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))))
164163imp 445 . . . . . . . . 9 ((𝑋 ∈ V ∧ ∀𝑦𝑋𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} (𝐴 𝑥 ∧ Σ*𝑤𝑥(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
16512, 157, 164syl2anc 693 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))))
1669ad2antrr 762 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
16739ralrimiva 2966 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦𝑋 𝐴 dom 𝑅)
168 iunss 4561 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀𝑦𝑋 𝐴 dom 𝑅)
169167, 168sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑 𝑦𝑋 𝐴 dom 𝑅)
17044ralrimiva 2966 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦𝑋 𝐴 ∈ V)
171 iunexg 7143 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 𝐴 ∈ V) → 𝑦𝑋 𝐴 ∈ V)
17211, 170, 171syl2anc 693 . . . . . . . . . . . . . . . . . 18 (𝜑 𝑦𝑋 𝐴 ∈ V)
173 elpwg 4166 . . . . . . . . . . . . . . . . . 18 ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
174172, 173syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅))
175169, 174mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅)
17632, 175ffvelrnd 6360 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ (0[,]+∞))
177107, 176sseldi 3601 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
178166, 177syl 17 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
179 simplr 792 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
18025ad4antr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
181 fex 6490 . . . . . . . . . . . . . . . . 17 ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ 𝑋 ∈ V) → 𝑔 ∈ V)
182179, 180, 181syl2anc 693 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 ∈ V)
183 rnexg 7098 . . . . . . . . . . . . . . . 16 (𝑔 ∈ V → ran 𝑔 ∈ V)
184 uniexg 6955 . . . . . . . . . . . . . . . 16 (ran 𝑔 ∈ V → ran 𝑔 ∈ V)
185182, 183, 1843syl 18 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ V)
186 simp-5l 808 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝜑)
18727ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑅:𝑄⟶(0[,]+∞))
188 frn 6053 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
189 ssrab2 3687 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅
190188, 189syl6ss 3615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
191190unissd 4462 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 𝒫 dom 𝑅)
192 unipw 4918 . . . . . . . . . . . . . . . . . . . . . 22 𝒫 dom 𝑅 = dom 𝑅
193191, 192syl6sseq 3651 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
194193adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ⊆ dom 𝑅)
19536adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → dom 𝑅 = 𝑄)
196194, 195sseqtrd 3641 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔𝑄)
197196sselda 3603 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → 𝑐𝑄)
198187, 197ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑐 ran 𝑔) → (𝑅𝑐) ∈ (0[,]+∞))
199198ralrimiva 2966 . . . . . . . . . . . . . . . 16 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
200186, 179, 199syl2anc 693 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
201 nfcv 2764 . . . . . . . . . . . . . . . 16 𝑐 ran 𝑔
202201esumcl 30092 . . . . . . . . . . . . . . 15 (( ran 𝑔 ∈ V ∧ ∀𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞)) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
203185, 200, 202syl2anc 693 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ (0[,]+∞))
204107, 203sseldi 3601 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*)
205 simp-5r 809 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ)
206205rexrd 10089 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*)
207 simpllr 799 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ+)
208207rpxrd 11873 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ*)
209206, 208xaddcld 12131 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) ∈ ℝ*)
210188ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
211 sstr 3611 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅)
212189, 211mpan2 707 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅)
213 sspwuni 4611 . . . . . . . . . . . . . . . . . . . . . . 23 (ran 𝑔 ⊆ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅)
214212, 213sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ran 𝑔 ⊆ dom 𝑅)
215210, 214syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ⊆ dom 𝑅)
216 ffn 6045 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑔 Fn 𝑋)
217216ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑔 Fn 𝑋)
218166, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ≼ ω)
219 fnct 9359 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 Fn 𝑋𝑋 ≼ ω) → 𝑔 ≼ ω)
220 rnct 9347 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 ≼ ω → ran 𝑔 ≼ ω)
221219, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 Fn 𝑋𝑋 ≼ ω) → ran 𝑔 ≼ ω)
222 dfss3 3592 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
223222biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
224 breq1 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω))
225224elrab 3363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω))
226225simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → 𝑤 ≼ ω)
227226ralimi 2952 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
228223, 227syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω)
229 unictb 9397 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑔 ≼ ω ∧ ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ran 𝑔 ≼ ω)
230221, 228, 229syl2an 494 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔 Fn 𝑋𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ran 𝑔 ≼ ω)
231217, 218, 210, 230syl21anc 1325 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ≼ ω)
232 ctex 7970 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V)
233 elpwg 4166 . . . . . . . . . . . . . . . . . . . . . 22 ( ran 𝑔 ∈ V → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
234231, 232, 2333syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅))
235215, 234mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ 𝒫 dom 𝑅)
236 simpl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝐴 (𝑔𝑦))
237236ralimi 2952 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 𝐴 (𝑔𝑦))
238 fvssunirn 6217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔𝑦) ⊆ ran 𝑔
239238unissi 4461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔𝑦) ⊆ ran 𝑔
240 sstr 3611 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 (𝑔𝑦) ∧ (𝑔𝑦) ⊆ ran 𝑔) → 𝐴 ran 𝑔)
241239, 240mpan2 707 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 (𝑔𝑦) → 𝐴 ran 𝑔)
242241ralimi 2952 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑋 𝐴 (𝑔𝑦) → ∀𝑦𝑋 𝐴 ran 𝑔)
243 iunss 4561 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑦𝑋 𝐴 ran 𝑔 ↔ ∀𝑦𝑋 𝐴 ran 𝑔)
244242, 243sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑦𝑋 𝐴 (𝑔𝑦) → 𝑦𝑋 𝐴 ran 𝑔)
245237, 244syl 17 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → 𝑦𝑋 𝐴 ran 𝑔)
246245adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑦𝑋 𝐴 ran 𝑔)
247235, 246, 231jca32 558 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
248 unieq 4444 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ran 𝑔 𝑧 = ran 𝑔)
249248sseq2d 3633 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔))
250 breq1 4656 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ran 𝑔 → (𝑧 ≼ ω ↔ ran 𝑔 ≼ ω))
251249, 250anbi12d 747 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ran 𝑔 → (( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
252251elrab 3363 . . . . . . . . . . . . . . . . . . 19 ( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω)))
253247, 252sylibr 224 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)})
254 fveq2 6191 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑤 → (𝑅𝑐) = (𝑅𝑤))
255254cbvesumv 30105 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)
256 esumeq1 30096 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ran 𝑔 → Σ*𝑤𝑥(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
257256eqeq2d 2632 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ran 𝑔 → (Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤) ↔ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)))
258257rspcev 3309 . . . . . . . . . . . . . . . . . 18 (( ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤 ran 𝑔(𝑅𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
259253, 255, 258sylancl 694 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
260 esumex 30091 . . . . . . . . . . . . . . . . . 18 Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ V
261 eqid 2622 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))
262261elrnmpt 5372 . . . . . . . . . . . . . . . . . 18 *𝑐 ran 𝑔(𝑅𝑐) ∈ V → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤)))
263260, 262ax-mp 5 . . . . . . . . . . . . . . . . 17 *𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)}Σ*𝑐 ran 𝑔(𝑅𝑐) = Σ*𝑤𝑥(𝑅𝑤))
264259, 263sylibr 224 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)))
265112a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → < Or (0[,]+∞))
266 omscl 30357 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
26726, 27, 175, 266syl3anc 1326 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞))
268 xrge0infss 29525 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
269267, 268syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤))𝑢 < 𝑡)))
270265, 269inflb 8395 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
27129fveq1i 6192 . . . . . . . . . . . . . . . . . . . 20 (𝑀 𝑦𝑋 𝐴) = ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴)
272169, 37sseqtrd 3641 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 𝑦𝑋 𝐴 𝑄)
273 omsfval 30356 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞) ∧ 𝑦𝑋 𝐴 𝑄) → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
27426, 27, 272, 273syl3anc 1326 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((toOMeas‘𝑅)‘ 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
275271, 274syl5eq 2668 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 𝑦𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < ))
276275breq2d 4665 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
277276notbid 308 . . . . . . . . . . . . . . . . 17 (𝜑 → (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)), (0[,]+∞), < )))
278270, 277sylibrd 249 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω)} ↦ Σ*𝑤𝑥(𝑅𝑤)) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
279166, 264, 278sylc 65 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
280 biid 251 . . . . . . . . . . . . . . 15 (¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
281279, 280sylib 208 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴))
282 xrlenlt 10103 . . . . . . . . . . . . . . 15 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑐 ran 𝑔(𝑅𝑐) ∈ ℝ*) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
283178, 204, 282syl2anc 693 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐) ↔ ¬ Σ*𝑐 ran 𝑔(𝑅𝑐) < (𝑀 𝑦𝑋 𝐴)))
284281, 283mpbird 247 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑐 ran 𝑔(𝑅𝑐))
285 nfv 1843 . . . . . . . . . . . . . . . . . . 19 𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}
28622, 285nfan 1828 . . . . . . . . . . . . . . . . . 18 𝑦((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
287 nfra1 2941 . . . . . . . . . . . . . . . . . 18 𝑦𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
288286, 287nfan 1828 . . . . . . . . . . . . . . . . 17 𝑦(((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
289 simp-6l 810 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝜑)
290 simpllr 799 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
291 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → 𝑦𝑋)
29227ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑅:𝑄⟶(0[,]+∞))
293 simpllr 799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
294 simplr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑦𝑋)
295293, 294ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
296189, 295sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ∈ 𝒫 dom 𝑅)
297296elpwid 4170 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ dom 𝑅)
298292, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → dom 𝑅 = 𝑄)
299297, 298sseqtrd 3641 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑔𝑦) ⊆ 𝑄)
300 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤 ∈ (𝑔𝑦))
301299, 300sseldd 3604 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → 𝑤𝑄)
302292, 301ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ 𝑤 ∈ (𝑔𝑦)) → (𝑅𝑤) ∈ (0[,]+∞))
303302ralrimiva 2966 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
304 fvex 6201 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑦) ∈ V
305 nfcv 2764 . . . . . . . . . . . . . . . . . . . . . 22 𝑤(𝑔𝑦)
306305esumcl 30092 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
307304, 306mpan 706 . . . . . . . . . . . . . . . . . . . 20 (∀𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
308303, 307syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
309289, 290, 291, 308syl21anc 1325 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
310309ex 450 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)))
311288, 310ralrimi 2957 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
31214esumcl 30092 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ V ∧ ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞)) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
313180, 311, 312syl2anc 693 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
314107, 313sseldi 3601 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
315 nfv 1843 . . . . . . . . . . . . . . . . . . 19 𝑤(𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
316 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
317 fniunfv 6505 . . . . . . . . . . . . . . . . . . . 20 (𝑔 Fn 𝑋 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
318316, 216, 3173syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑦𝑋 (𝑔𝑦) = ran 𝑔)
319315, 318esumeq1d 30097 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) = Σ*𝑤 ran 𝑔(𝑅𝑤))
32011adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → 𝑋 ∈ V)
321304a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑔𝑦) ∈ V)
322320, 321, 302esumiun 30156 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 𝑦𝑋 (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
323319, 322eqbrtrrd 4677 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
3249, 323sylan 488 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
325324adantr 481 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑤 ran 𝑔(𝑅𝑤) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
326255, 325syl5eqbr 4688 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤))
327289, 291, 48syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
328 simplll 798 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+))
329328, 291, 75syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
330327, 329xrge0addcld 29527 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
331330ex 450 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)))
332288, 331ralrimi 2957 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
33314esumcl 30092 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ ∀𝑦𝑋 ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞)) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
334180, 332, 333syl2anc 693 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ (0[,]+∞))
335107, 334sseldi 3601 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
336218, 10syl 17 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑋 ∈ V)
337 simp-4l 806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ))
338 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑦𝑋)
339337, 338, 51syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ)
340339adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑀𝐴) ∈ ℝ)
34167adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
342341adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ)
343 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 *𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
344343adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))
34568breq2d 4665 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ↔ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))
346345biimpar 502 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
347340, 342, 344, 346syl21anc 1325 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
348347ex 450 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
349337simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝜑)
350 simplr 792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω})
351349, 350, 338, 308syl21anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ (0[,]+∞))
352107, 351sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ*)
353339rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ ℝ*)
354341rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
355353, 354xaddcld 12131 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*)
356 xrltle 11982 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ∈ ℝ* ∧ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ∈ ℝ*) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
357352, 355, 356syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
358348, 357syld 47 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → (Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
359358adantld 483 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ 𝑦𝑋) → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
360359ex 450 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (𝑦𝑋 → ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))))
361286, 360ralrimi 2957 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → ∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
362 ralim 2948 . . . . . . . . . . . . . . . . . . 19 (∀𝑦𝑋 ((𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
363361, 362syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) → (∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦))))))
364363imp 445 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
365364r19.21bi 2932 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ ((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
366288, 14, 336, 309, 330, 365esumlef 30124 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))))
367166, 48sylan 488 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) ∧ 𝑦𝑋) → (𝑀𝐴) ∈ (0[,]+∞))
368288, 14, 336, 367, 329esumaddf 30123 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) = (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))))
369329ex 450 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑦𝑋 → (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)))
370288, 369ralrimi 2957 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
37114esumcl 30092 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
372180, 370, 371syl2anc 693 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
373107, 372sseldi 3601 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*)
374 simp-4r 807 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑓:𝑋1-1→ℕ)
375 vex 3203 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
376375rnex 7100 . . . . . . . . . . . . . . . . . . . . . . 23 ran 𝑓 ∈ V
377376a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V)
378 frn 6053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋⟶ℕ → ran 𝑓 ⊆ ℕ)
37960, 378syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 ⊆ ℕ)
380379adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆ ℕ)
381380sselda 3603 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ)
38256a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈ ℝ+)
383 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ)
384383nnzd 11481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ)
385382, 384rpexpcld 13032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈ ℝ+)
386385rpreccld 11882 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ ℝ+)
38773, 386sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
388387adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
389381, 388syldan 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞))
390389ralrimiva 2966 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
391 nfcv 2764 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧ran 𝑓
392391esumcl 30092 . . . . . . . . . . . . . . . . . . . . . 22 ((ran 𝑓 ∈ V ∧ ∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
393377, 390, 392syl2anc 693 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞))
394107, 393sseldi 3601 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ*)
395 1re 10039 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ
396 rexr 10085 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℝ → 1 ∈ ℝ*)
397395, 396ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
398397a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈ ℝ*)
39973sseli 3599 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ ℝ+𝑒 ∈ (0[,]+∞))
400399adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,]+∞))
401 elxrge0 12281 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (0[,]+∞) ↔ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
402400, 401sylib 208 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒))
403 nfv 1843 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧(𝜑𝑓:𝑋1-1→ℕ)
404 nnex 11026 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ ∈ V
405404a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → ℕ ∈ V)
406403, 405, 387, 379esummono 30116 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)))
407 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤))
408407oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤)))
409 ioossico 12262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0(,)+∞) ⊆ (0[,)+∞)
41071, 409eqsstri 3635 . . . . . . . . . . . . . . . . . . . . . . . . 25 + ⊆ (0[,)+∞)
411410, 386sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈ (0[,)+∞))
412 eqidd 2623 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))))
413 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧)
414413oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧))
415414oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧)))
416 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
417 ovexd 6680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ ℕ → (1 / (2↑𝑧)) ∈ V)
418412, 415, 416, 417fvmptd 6288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
419418adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧)))
420 ax-1cn 9994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
421 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))
422421geo2lim 14606 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℂ → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
423420, 422ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1
424423a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1)
425395a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 1 ∈ ℝ)
426408, 411, 419, 424, 425esumcvgsum 30150 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = Σ𝑧 ∈ ℕ (1 / (2↑𝑧)))
427 geoihalfsum 14614 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑧 ∈ ℕ (1 / (2↑𝑧)) = 1
428426, 427syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 / (2↑𝑧)) = 1)
429406, 428breqtrd 4679 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
430429adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1)
431 xlemul2a 12119 . . . . . . . . . . . . . . . . . . . 20 (((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒)) ∧ Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
432394, 398, 402, 430, 431syl31anc 1329 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1))
43313, 19nfan 1828 . . . . . . . . . . . . . . . . . . . . . 22 𝑦(𝜑𝑓:𝑋1-1→ℕ)
434433, 21nfan 1828 . . . . . . . . . . . . . . . . . . . . 21 𝑦((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+)
43578recnd 10068 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → 𝑒 ∈ ℂ)
43680recnd 10068 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
437436adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ∈ ℂ)
438 2cn 11091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ∈ ℂ)
440 2ne0 11113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ≠ 0
441440a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 2 ≠ 0)
442439, 441, 62expne0d 13014 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
443442adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (2↑(𝑓𝑦)) ≠ 0)
444435, 437, 443divrecd 10804 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
445 1rp 11836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℝ+
446445a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → 1 ∈ ℝ+)
447446, 63rpdivcld 11889 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ+)
44854, 447sseldi 3601 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
449448adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ ℝ)
450 rexmul 12101 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑒 ∈ ℝ ∧ (1 / (2↑(𝑓𝑦))) ∈ ℝ) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
45178, 449, 450syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 ·e (1 / (2↑(𝑓𝑦)))) = (𝑒 · (1 / (2↑(𝑓𝑦)))))
452444, 451eqtr4d 2659 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
453452ralrimiva 2966 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ∀𝑦𝑋 (𝑒 / (2↑(𝑓𝑦))) = (𝑒 ·e (1 / (2↑(𝑓𝑦)))))
454434, 453esumeq2d 30099 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
45511ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V)
45673, 447sseldi 3601 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
457456adantlr 751 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦𝑋) → (1 / (2↑(𝑓𝑦))) ∈ (0[,]+∞))
458410a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → ℝ+ ⊆ (0[,)+∞))
459458sselda 3603 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ (0[,)+∞))
460455, 457, 459esummulc2 30144 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = Σ*𝑦𝑋(𝑒 ·e (1 / (2↑(𝑓𝑦)))))
461 nfcv 2764 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦(1 / (2↑𝑧))
462 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑓𝑦) → (2↑𝑧) = (2↑(𝑓𝑦)))
463462oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑓𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓𝑦))))
46411adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → 𝑋 ∈ V)
46558simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → Fun 𝑓)
46659feqmptd 6249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
467466cnveqd 5298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑋1-1→ℕ → 𝑓 = (𝑦𝑋 ↦ (𝑓𝑦)))
468467funeqd 5910 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑋1-1→ℕ → (Fun 𝑓 ↔ Fun (𝑦𝑋 ↦ (𝑓𝑦))))
469465, 468mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋1-1→ℕ → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
470469adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → Fun (𝑦𝑋 ↦ (𝑓𝑦)))
471461, 433, 14, 463, 464, 470, 456, 61esumc 30113 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
472 ffn 6045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋)
473 fnrnfv 6242 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
47460, 472, 4733syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓:𝑋1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)})
475403, 474esumeq1d 30097 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦𝑋 𝑥 = (𝑓𝑦)} (1 / (2↑𝑧)))
476471, 475eqtr4d 2659 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓:𝑋1-1→ℕ) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
477476adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(1 / (2↑(𝑓𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)))
478477oveq2d 6666 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑦𝑋(1 / (2↑(𝑓𝑦)))) = (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))))
479454, 460, 4783eqtr2rd 2663 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))))
480402simpld 475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ*)
481 xmulid1 12109 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ ℝ* → (𝑒 ·e 1) = 𝑒)
482480, 481syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒)
483432, 479, 4823brtr3d 4684 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
484166, 374, 207, 483syl21anc 1325 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒)
485 xleadd2a 12084 . . . . . . . . . . . . . . . . 17 (((Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ*) ∧ Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦))) ≤ 𝑒) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
486373, 208, 206, 484, 485syl31anc 1329 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 Σ*𝑦𝑋(𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
487368, 486eqbrtrd 4675 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋((𝑀𝐴) +𝑒 (𝑒 / (2↑(𝑓𝑦)))) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
488314, 335, 209, 366, 487xrletrd 11993 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑦𝑋Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
489204, 314, 209, 326, 488xrletrd 11993 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → Σ*𝑐 ran 𝑔(𝑅𝑐) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
490178, 204, 209, 284, 489xrletrd 11993 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒))
491207rpred 11872 . . . . . . . . . . . . 13 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → 𝑒 ∈ ℝ)
492 rexadd 12063 . . . . . . . . . . . . 13 ((Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
493205, 491, 492syl2anc 693 . . . . . . . . . . . 12 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (Σ*𝑦𝑋(𝑀𝐴) +𝑒 𝑒) = (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
494490, 493breqtrd 4679 . . . . . . . . . . 11 ((((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω}) ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
495494anasss 679 . . . . . . . . . 10 (((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦))))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
496495ex 450 . . . . . . . . 9 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
497496exlimdv 1861 . . . . . . . 8 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω} ∧ ∀𝑦𝑋 (𝐴 (𝑔𝑦) ∧ Σ*𝑤 ∈ (𝑔𝑦)(𝑅𝑤) < ((𝑀𝐴) + (𝑒 / (2↑(𝑓𝑦)))))) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
498165, 497mpd 15 . . . . . . 7 ((((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
499498ralrimiva 2966 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒))
500 xralrple 12036 . . . . . . . 8 (((𝑀 𝑦𝑋 𝐴) ∈ ℝ* ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
501177, 500sylan 488 . . . . . . 7 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
502501adantr 481 . . . . . 6 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → ((𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀 𝑦𝑋 𝐴) ≤ (Σ*𝑦𝑋(𝑀𝐴) + 𝑒)))
503499, 502mpbird 247 . . . . 5 (((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) ∧ 𝑓:𝑋1-1→ℕ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
504503ex 450 . . . 4 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
505504exlimdv 1861 . . 3 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋1-1→ℕ → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴)))
5068, 505mpd 15 . 2 ((𝜑 ∧ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
507177adantr 481 . . . 4 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ∈ ℝ*)
508 pnfge 11964 . . . 4 ((𝑀 𝑦𝑋 𝐴) ∈ ℝ* → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
509507, 508syl 17 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ +∞)
51048ralrimiva 2966 . . . . 5 (𝜑 → ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞))
51114esumcl 30092 . . . . 5 ((𝑋 ∈ V ∧ ∀𝑦𝑋 (𝑀𝐴) ∈ (0[,]+∞)) → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
51211, 510, 511syl2anc 693 . . . 4 (𝜑 → Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞))
513 xrge0nre 12277 . . . 4 ((Σ*𝑦𝑋(𝑀𝐴) ∈ (0[,]+∞) ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
514512, 513sylan 488 . . 3 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → Σ*𝑦𝑋(𝑀𝐴) = +∞)
515509, 514breqtrrd 4681 . 2 ((𝜑 ∧ ¬ Σ*𝑦𝑋(𝑀𝐴) ∈ ℝ) → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
516506, 515pm2.61dan 832 1 (𝜑 → (𝑀 𝑦𝑋 𝐴) ≤ Σ*𝑦𝑋(𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1483  wex 1704  wcel 1990  {cab 2608  wne 2794  wral 2912  wrex 2913  {crab 2916  Vcvv 3200  wss 3574  𝒫 cpw 4158   cuni 4436   ciun 4520   class class class wbr 4653  cmpt 4729   Or wor 5034  ccnv 5113  dom cdm 5114  ran crn 5115  Fun wfun 5882   Fn wfn 5883  wf 5884  1-1wf1 5885  cfv 5888  (class class class)co 6650  ωcom 7065  cen 7952  cdom 7953  infcinf 8347  cc 9934  cr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941  +∞cpnf 10071  *cxr 10073   < clt 10074  cle 10075   / cdiv 10684  cn 11020  2c2 11070  cz 11377  +crp 11832   +𝑒 cxad 11944   ·e cxmu 11945  (,)cioo 12175  [,)cico 12177  [,]cicc 12178  seqcseq 12801  cexp 12860  cli 14215  Σcsu 14416  Σ*cesum 30089  toOMeascoms 30353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-reg 8497  ax-inf2 8538  ax-cc 9257  ax-ac2 9285  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-r1 8627  df-rank 8628  df-card 8765  df-acn 8768  df-ac 8939  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-pi 14803  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-ordt 16161  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-ps 17200  df-tsr 17201  df-plusf 17241  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-subrg 18778  df-abv 18817  df-lmod 18865  df-scaf 18866  df-sra 19172  df-rgmod 19173  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-tmd 21876  df-tgp 21877  df-tsms 21930  df-trg 21963  df-xms 22125  df-ms 22126  df-tms 22127  df-nm 22387  df-ngp 22388  df-nrg 22390  df-nlm 22391  df-ii 22680  df-cncf 22681  df-limc 23630  df-dv 23631  df-log 24303  df-esum 30090  df-oms 30354
This theorem is referenced by:  omsmeas  30385
  Copyright terms: Public domain W3C validator