Metamath Proof Explorer


Theorem omssubadd

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)

Ref Expression
Hypotheses oms.m 𝑀 = ( toOMeas ‘ 𝑅 )
oms.o ( 𝜑𝑄𝑉 )
oms.r ( 𝜑𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
omssubadd.a ( ( 𝜑𝑦𝑋 ) → 𝐴 𝑄 )
omssubadd.b ( 𝜑𝑋 ≼ ω )
Assertion omssubadd ( 𝜑 → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) )

Proof

Step Hyp Ref Expression
1 oms.m 𝑀 = ( toOMeas ‘ 𝑅 )
2 oms.o ( 𝜑𝑄𝑉 )
3 oms.r ( 𝜑𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
4 omssubadd.a ( ( 𝜑𝑦𝑋 ) → 𝐴 𝑄 )
5 omssubadd.b ( 𝜑𝑋 ≼ ω )
6 nnenom ℕ ≈ ω
7 6 ensymi ω ≈ ℕ
8 domentr ( ( 𝑋 ≼ ω ∧ ω ≈ ℕ ) → 𝑋 ≼ ℕ )
9 5 7 8 sylancl ( 𝜑𝑋 ≼ ℕ )
10 brdomi ( 𝑋 ≼ ℕ → ∃ 𝑓 𝑓 : 𝑋1-1→ ℕ )
11 9 10 syl ( 𝜑 → ∃ 𝑓 𝑓 : 𝑋1-1→ ℕ )
12 11 adantr ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ∃ 𝑓 𝑓 : 𝑋1-1→ ℕ )
13 simplll ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝜑 )
14 ctex ( 𝑋 ≼ ω → 𝑋 ∈ V )
15 5 14 syl ( 𝜑𝑋 ∈ V )
16 13 15 syl ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝑋 ∈ V )
17 nfv 𝑦 𝜑
18 nfcv 𝑦 𝑋
19 18 nfesum1 𝑦 Σ* 𝑦𝑋 ( 𝑀𝐴 )
20 nfcv 𝑦
21 19 20 nfel 𝑦 Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ
22 17 21 nfan 𝑦 ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ )
23 nfv 𝑦 𝑓 : 𝑋1-1→ ℕ
24 22 23 nfan 𝑦 ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ )
25 nfv 𝑦 𝑒 ∈ ℝ+
26 24 25 nfan 𝑦 ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ )
27 13 adantr ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝜑 )
28 simpr ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
29 15 adantr ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → 𝑋 ∈ V )
30 omsf ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) )
31 1 feq1i ( 𝑀 : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) ↔ ( toOMeas ‘ 𝑅 ) : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) )
32 30 31 sylibr ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → 𝑀 : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) )
33 2 3 32 syl2anc ( 𝜑𝑀 : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) )
34 33 adantr ( ( 𝜑𝑦𝑋 ) → 𝑀 : 𝒫 dom 𝑅 ⟶ ( 0 [,] +∞ ) )
35 3 fdmd ( 𝜑 → dom 𝑅 = 𝑄 )
36 35 unieqd ( 𝜑 dom 𝑅 = 𝑄 )
37 36 adantr ( ( 𝜑𝑦𝑋 ) → dom 𝑅 = 𝑄 )
38 4 37 sseqtrrd ( ( 𝜑𝑦𝑋 ) → 𝐴 dom 𝑅 )
39 2 uniexd ( 𝜑 𝑄 ∈ V )
40 39 adantr ( ( 𝜑𝑦𝑋 ) → 𝑄 ∈ V )
41 ssexg ( ( 𝐴 𝑄 𝑄 ∈ V ) → 𝐴 ∈ V )
42 4 40 41 syl2anc ( ( 𝜑𝑦𝑋 ) → 𝐴 ∈ V )
43 elpwg ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅 ) )
44 42 43 syl ( ( 𝜑𝑦𝑋 ) → ( 𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅 ) )
45 38 44 mpbird ( ( 𝜑𝑦𝑋 ) → 𝐴 ∈ 𝒫 dom 𝑅 )
46 34 45 ffvelrnd ( ( 𝜑𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
47 46 adantlr ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
48 simpr ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ )
49 22 29 47 48 esumcvgre ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ℝ )
50 49 adantlr ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ℝ )
51 50 adantlr ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ℝ )
52 rpssre + ⊆ ℝ
53 simplr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑒 ∈ ℝ+ )
54 2rp 2 ∈ ℝ+
55 54 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → 2 ∈ ℝ+ )
56 df-f1 ( 𝑓 : 𝑋1-1→ ℕ ↔ ( 𝑓 : 𝑋 ⟶ ℕ ∧ Fun 𝑓 ) )
57 56 simplbi ( 𝑓 : 𝑋1-1→ ℕ → 𝑓 : 𝑋 ⟶ ℕ )
58 57 adantl ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → 𝑓 : 𝑋 ⟶ ℕ )
59 58 ffvelrnda ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 𝑓𝑦 ) ∈ ℕ )
60 59 nnzd ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 𝑓𝑦 ) ∈ ℤ )
61 55 60 rpexpcld ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℝ+ )
62 61 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℝ+ )
63 53 62 rpdivcld ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ+ )
64 52 63 sseldi ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
65 64 adantl3r ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
66 rexadd ( ( ( 𝑀𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ ) → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
67 51 65 66 syl2anc ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
68 13 46 sylan ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
69 dfrp2 + = ( 0 (,) +∞ )
70 ioossicc ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
71 69 70 eqsstri + ⊆ ( 0 [,] +∞ )
72 71 63 sseldi ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
73 72 adantl3r ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
74 68 73 xrge0addcld ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
75 67 74 eqeltrrd ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
76 52 53 sseldi ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑒 ∈ ℝ )
77 76 adantl3r ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑒 ∈ ℝ )
78 52 61 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℝ )
79 78 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℝ )
80 79 adantl3r ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℝ )
81 simplr ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑒 ∈ ℝ+ )
82 81 rpgt0d ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 0 < 𝑒 )
83 2re 2 ∈ ℝ
84 83 a1i ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 2 ∈ ℝ )
85 60 adantllr ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 𝑓𝑦 ) ∈ ℤ )
86 85 adantlr ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑓𝑦 ) ∈ ℤ )
87 2pos 0 < 2
88 87 a1i ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 0 < 2 )
89 expgt0 ( ( 2 ∈ ℝ ∧ ( 𝑓𝑦 ) ∈ ℤ ∧ 0 < 2 ) → 0 < ( 2 ↑ ( 𝑓𝑦 ) ) )
90 84 86 88 89 syl3anc ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 0 < ( 2 ↑ ( 𝑓𝑦 ) ) )
91 77 80 82 90 divgt0d ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 0 < ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) )
92 65 51 ltaddposd ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 0 < ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ↔ ( 𝑀𝐴 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
93 91 92 mpbid ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
94 1 fveq1i ( 𝑀𝐴 ) = ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 )
95 2 adantr ( ( 𝜑𝑦𝑋 ) → 𝑄𝑉 )
96 3 adantr ( ( 𝜑𝑦𝑋 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
97 omsfval ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
98 95 96 4 97 syl3anc ( ( 𝜑𝑦𝑋 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
99 94 98 syl5eq ( ( 𝜑𝑦𝑋 ) → ( 𝑀𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
100 13 99 sylan ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
101 100 eqcomd ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) = ( 𝑀𝐴 ) )
102 101 breq1d ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ ( 𝑀𝐴 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
103 93 102 mpbird ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
104 75 103 jca ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
105 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
106 xrltso < Or ℝ*
107 soss ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
108 105 106 107 mp2 < Or ( 0 [,] +∞ )
109 biid ( < Or ( 0 [,] +∞ ) ↔ < Or ( 0 [,] +∞ ) )
110 108 109 mpbi < Or ( 0 [,] +∞ )
111 110 a1i ( ( 𝜑𝑦𝑋 ) → < Or ( 0 [,] +∞ ) )
112 omscl ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ 𝒫 dom 𝑅 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
113 95 96 45 112 syl3anc ( ( 𝜑𝑦𝑋 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
114 xrge0infss ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) → ∃ 𝑣 ∈ ( 0 [,] +∞ ) ( ∀ ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ¬ < 𝑣 ∧ ∀ ∈ ( 0 [,] +∞ ) ( 𝑣 < → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ) ) )
115 113 114 syl ( ( 𝜑𝑦𝑋 ) → ∃ 𝑣 ∈ ( 0 [,] +∞ ) ( ∀ ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ¬ < 𝑣 ∧ ∀ ∈ ( 0 [,] +∞ ) ( 𝑣 < → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ) ) )
116 111 115 infglb ( ( 𝜑𝑦𝑋 ) → ( ( ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
117 116 imp ( ( ( 𝜑𝑦𝑋 ) ∧ ( ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
118 27 28 104 117 syl21anc ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
119 eqid ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
120 esumex Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∈ V
121 119 120 elrnmpti ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
122 121 anbi1i ( ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
123 r19.41v ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
124 122 123 bitr4i ( ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
125 124 exbii ( ∃ 𝑢 ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ∃ 𝑢𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
126 df-rex ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
127 rexcom4 ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ∃ 𝑢𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
128 125 126 127 3bitr4i ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
129 breq1 ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) → ( 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
130 idd ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) → ( Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
131 129 130 sylbid ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) → ( 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
132 131 imp ( ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
133 132 exlimiv ( ∃ 𝑢 ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
134 133 reximi ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ∧ 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
135 128 134 sylbi ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
136 118 135 syl ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
137 simpr ( ( 𝐴 𝑧𝑧 ≼ ω ) → 𝑧 ≼ ω )
138 137 a1i ( 𝑧 ∈ 𝒫 dom 𝑅 → ( ( 𝐴 𝑧𝑧 ≼ ω ) → 𝑧 ≼ ω ) )
139 138 ss2rabi { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω }
140 rexss ( { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
141 139 140 ax-mp ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
142 unieq ( 𝑧 = 𝑥 𝑧 = 𝑥 )
143 142 sseq2d ( 𝑧 = 𝑥 → ( 𝐴 𝑧𝐴 𝑥 ) )
144 breq1 ( 𝑧 = 𝑥 → ( 𝑧 ≼ ω ↔ 𝑥 ≼ ω ) )
145 143 144 anbi12d ( 𝑧 = 𝑥 → ( ( 𝐴 𝑧𝑧 ≼ ω ) ↔ ( 𝐴 𝑥𝑥 ≼ ω ) ) )
146 145 elrab ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↔ ( 𝑥 ∈ 𝒫 dom 𝑅 ∧ ( 𝐴 𝑥𝑥 ≼ ω ) ) )
147 146 simprbi ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } → ( 𝐴 𝑥𝑥 ≼ ω ) )
148 147 simpld ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } → 𝐴 𝑥 )
149 148 a1i ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } → 𝐴 𝑥 ) )
150 149 anim1d ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
151 150 reximdv ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
152 141 151 syl5bi ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
153 136 152 mpd ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
154 153 ex ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑦𝑋 → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
155 26 154 ralrimi ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑦𝑋𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
156 unieq ( 𝑥 = ( 𝑔𝑦 ) → 𝑥 = ( 𝑔𝑦 ) )
157 156 sseq2d ( 𝑥 = ( 𝑔𝑦 ) → ( 𝐴 𝑥𝐴 ( 𝑔𝑦 ) ) )
158 esumeq1 ( 𝑥 = ( 𝑔𝑦 ) → Σ* 𝑤𝑥 ( 𝑅𝑤 ) = Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
159 158 breq1d ( 𝑥 = ( 𝑔𝑦 ) → ( Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
160 157 159 anbi12d ( 𝑥 = ( 𝑔𝑦 ) → ( ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ↔ ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
161 160 ac6sg ( 𝑋 ∈ V → ( ∀ 𝑦𝑋𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∃ 𝑔 ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ) )
162 161 imp ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ( 𝐴 𝑥 ∧ Σ* 𝑤𝑥 ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∃ 𝑔 ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
163 16 155 162 syl2anc ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑔 ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
164 13 ad2antrr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝜑 )
165 38 ralrimiva ( 𝜑 → ∀ 𝑦𝑋 𝐴 dom 𝑅 )
166 iunss ( 𝑦𝑋 𝐴 dom 𝑅 ↔ ∀ 𝑦𝑋 𝐴 dom 𝑅 )
167 165 166 sylibr ( 𝜑 𝑦𝑋 𝐴 dom 𝑅 )
168 42 ralrimiva ( 𝜑 → ∀ 𝑦𝑋 𝐴 ∈ V )
169 iunexg ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋 𝐴 ∈ V ) → 𝑦𝑋 𝐴 ∈ V )
170 15 168 169 syl2anc ( 𝜑 𝑦𝑋 𝐴 ∈ V )
171 elpwg ( 𝑦𝑋 𝐴 ∈ V → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅 ) )
172 170 171 syl ( 𝜑 → ( 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 𝑦𝑋 𝐴 dom 𝑅 ) )
173 167 172 mpbird ( 𝜑 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 )
174 33 173 ffvelrnd ( 𝜑 → ( 𝑀 𝑦𝑋 𝐴 ) ∈ ( 0 [,] +∞ ) )
175 105 174 sseldi ( 𝜑 → ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* )
176 164 175 syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* )
177 simplr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
178 29 ad4antr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑋 ∈ V )
179 177 178 fexd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑔 ∈ V )
180 rnexg ( 𝑔 ∈ V → ran 𝑔 ∈ V )
181 uniexg ( ran 𝑔 ∈ V → ran 𝑔 ∈ V )
182 179 180 181 3syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ∈ V )
183 simp-5l ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝜑 )
184 3 ad2antrr ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑐 ran 𝑔 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
185 frn ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
186 ssrab2 { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ⊆ 𝒫 dom 𝑅
187 185 186 sstrdi ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 ⊆ 𝒫 dom 𝑅 )
188 187 unissd ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 𝒫 dom 𝑅 )
189 unipw 𝒫 dom 𝑅 = dom 𝑅
190 188 189 sseqtrdi ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 ⊆ dom 𝑅 )
191 190 adantl ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ran 𝑔 ⊆ dom 𝑅 )
192 35 adantr ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → dom 𝑅 = 𝑄 )
193 191 192 sseqtrd ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ran 𝑔𝑄 )
194 193 sselda ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑐 ran 𝑔 ) → 𝑐𝑄 )
195 184 194 ffvelrnd ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑐 ran 𝑔 ) → ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) )
196 195 ralrimiva ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ∀ 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) )
197 183 177 196 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∀ 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) )
198 nfcv 𝑐 ran 𝑔
199 198 esumcl ( ( ran 𝑔 ∈ V ∧ ∀ 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) )
200 182 197 199 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ( 0 [,] +∞ ) )
201 105 200 sseldi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ℝ* )
202 simp-5r ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ )
203 202 rexrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ* )
204 simpllr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑒 ∈ ℝ+ )
205 204 rpxrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑒 ∈ ℝ* )
206 203 205 xaddcld ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) ∈ ℝ* )
207 185 ad2antlr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
208 sstr ( ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ⊆ 𝒫 dom 𝑅 ) → ran 𝑔 ⊆ 𝒫 dom 𝑅 )
209 186 208 mpan2 ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 ⊆ 𝒫 dom 𝑅 )
210 sspwuni ( ran 𝑔 ⊆ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅 )
211 209 210 sylib ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ran 𝑔 ⊆ dom 𝑅 )
212 207 211 syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ⊆ dom 𝑅 )
213 ffn ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → 𝑔 Fn 𝑋 )
214 213 ad2antlr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑔 Fn 𝑋 )
215 164 5 syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑋 ≼ ω )
216 fnct ( ( 𝑔 Fn 𝑋𝑋 ≼ ω ) → 𝑔 ≼ ω )
217 rnct ( 𝑔 ≼ ω → ran 𝑔 ≼ ω )
218 216 217 syl ( ( 𝑔 Fn 𝑋𝑋 ≼ ω ) → ran 𝑔 ≼ ω )
219 dfss3 ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ↔ ∀ 𝑤 ∈ ran 𝑔 𝑤 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
220 219 biimpi ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ∀ 𝑤 ∈ ran 𝑔 𝑤 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
221 breq1 ( 𝑧 = 𝑤 → ( 𝑧 ≼ ω ↔ 𝑤 ≼ ω ) )
222 221 elrab ( 𝑤 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ↔ ( 𝑤 ∈ 𝒫 dom 𝑅𝑤 ≼ ω ) )
223 222 simprbi ( 𝑤 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → 𝑤 ≼ ω )
224 223 ralimi ( ∀ 𝑤 ∈ ran 𝑔 𝑤 ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ∀ 𝑤 ∈ ran 𝑔 𝑤 ≼ ω )
225 220 224 syl ( ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } → ∀ 𝑤 ∈ ran 𝑔 𝑤 ≼ ω )
226 unictb ( ( ran 𝑔 ≼ ω ∧ ∀ 𝑤 ∈ ran 𝑔 𝑤 ≼ ω ) → ran 𝑔 ≼ ω )
227 218 225 226 syl2an ( ( ( 𝑔 Fn 𝑋𝑋 ≼ ω ) ∧ ran 𝑔 ⊆ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ran 𝑔 ≼ ω )
228 214 215 207 227 syl21anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ≼ ω )
229 ctex ( ran 𝑔 ≼ ω → ran 𝑔 ∈ V )
230 elpwg ( ran 𝑔 ∈ V → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅 ) )
231 228 229 230 3syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ran 𝑔 ⊆ dom 𝑅 ) )
232 212 231 mpbird ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ∈ 𝒫 dom 𝑅 )
233 simpl ( ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → 𝐴 ( 𝑔𝑦 ) )
234 233 ralimi ( ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∀ 𝑦𝑋 𝐴 ( 𝑔𝑦 ) )
235 fvssunirn ( 𝑔𝑦 ) ⊆ ran 𝑔
236 235 unissi ( 𝑔𝑦 ) ⊆ ran 𝑔
237 sstr ( ( 𝐴 ( 𝑔𝑦 ) ∧ ( 𝑔𝑦 ) ⊆ ran 𝑔 ) → 𝐴 ran 𝑔 )
238 236 237 mpan2 ( 𝐴 ( 𝑔𝑦 ) → 𝐴 ran 𝑔 )
239 238 ralimi ( ∀ 𝑦𝑋 𝐴 ( 𝑔𝑦 ) → ∀ 𝑦𝑋 𝐴 ran 𝑔 )
240 iunss ( 𝑦𝑋 𝐴 ran 𝑔 ↔ ∀ 𝑦𝑋 𝐴 ran 𝑔 )
241 239 240 sylibr ( ∀ 𝑦𝑋 𝐴 ( 𝑔𝑦 ) → 𝑦𝑋 𝐴 ran 𝑔 )
242 234 241 syl ( ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → 𝑦𝑋 𝐴 ran 𝑔 )
243 242 adantl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑦𝑋 𝐴 ran 𝑔 )
244 232 243 228 jca32 ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω ) ) )
245 unieq ( 𝑧 = ran 𝑔 𝑧 = ran 𝑔 )
246 245 sseq2d ( 𝑧 = ran 𝑔 → ( 𝑦𝑋 𝐴 𝑧 𝑦𝑋 𝐴 ran 𝑔 ) )
247 breq1 ( 𝑧 = ran 𝑔 → ( 𝑧 ≼ ω ↔ ran 𝑔 ≼ ω ) )
248 246 247 anbi12d ( 𝑧 = ran 𝑔 → ( ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) ↔ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω ) ) )
249 248 elrab ( ran 𝑔 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↔ ( ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ ( 𝑦𝑋 𝐴 ran 𝑔 ran 𝑔 ≼ ω ) ) )
250 244 249 sylibr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ran 𝑔 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } )
251 fveq2 ( 𝑐 = 𝑤 → ( 𝑅𝑐 ) = ( 𝑅𝑤 ) )
252 251 cbvesumv Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 )
253 esumeq1 ( 𝑥 = ran 𝑔 → Σ* 𝑤𝑥 ( 𝑅𝑤 ) = Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) )
254 253 rspceeqv ( ( ran 𝑔 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ∧ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
255 250 252 254 sylancl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
256 esumex Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ V
257 eqid ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
258 257 elrnmpt ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ V → ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) )
259 256 258 ax-mp ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) = Σ* 𝑤𝑥 ( 𝑅𝑤 ) )
260 255 259 sylibr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) )
261 110 a1i ( 𝜑 → < Or ( 0 [,] +∞ ) )
262 omscl ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝑦𝑋 𝐴 ∈ 𝒫 dom 𝑅 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
263 2 3 173 262 syl3anc ( 𝜑 → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
264 xrge0infss ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ⊆ ( 0 [,] +∞ ) → ∃ 𝑒 ∈ ( 0 [,] +∞ ) ( ∀ 𝑡 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ¬ 𝑡 < 𝑒 ∧ ∀ 𝑡 ∈ ( 0 [,] +∞ ) ( 𝑒 < 𝑡 → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < 𝑡 ) ) )
265 263 264 syl ( 𝜑 → ∃ 𝑒 ∈ ( 0 [,] +∞ ) ( ∀ 𝑡 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) ¬ 𝑡 < 𝑒 ∧ ∀ 𝑡 ∈ ( 0 [,] +∞ ) ( 𝑒 < 𝑡 → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) 𝑢 < 𝑡 ) ) )
266 261 265 inflb ( 𝜑 → ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) → ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) ) )
267 1 fveq1i ( 𝑀 𝑦𝑋 𝐴 ) = ( ( toOMeas ‘ 𝑅 ) ‘ 𝑦𝑋 𝐴 )
268 167 36 sseqtrd ( 𝜑 𝑦𝑋 𝐴 𝑄 )
269 omsfval ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝑦𝑋 𝐴 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝑦𝑋 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
270 2 3 268 269 syl3anc ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ 𝑦𝑋 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
271 267 270 syl5eq ( 𝜑 → ( 𝑀 𝑦𝑋 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
272 271 breq2d ( 𝜑 → ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ↔ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) ) )
273 272 notbid ( 𝜑 → ( ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ↔ ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) , ( 0 [,] +∞ ) , < ) ) )
274 266 273 sylibrd ( 𝜑 → ( Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑦𝑋 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑤𝑥 ( 𝑅𝑤 ) ) → ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ) )
275 164 260 274 sylc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) )
276 biid ( ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ↔ ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) )
277 275 276 sylib ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) )
278 xrlenlt ( ( ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* ∧ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ∈ ℝ* ) → ( ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ↔ ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ) )
279 176 201 278 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ↔ ¬ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) < ( 𝑀 𝑦𝑋 𝐴 ) ) )
280 277 279 mpbird ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) )
281 nfv 𝑦 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω }
282 26 281 nfan 𝑦 ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
283 nfra1 𝑦𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
284 282 283 nfan 𝑦 ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
285 simp-6l ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → 𝜑 )
286 simpllr ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
287 simpr ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
288 3 ad3antrrr ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
289 simpllr ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
290 simplr ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → 𝑦𝑋 )
291 289 290 ffvelrnd ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → ( 𝑔𝑦 ) ∈ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
292 186 291 sseldi ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → ( 𝑔𝑦 ) ∈ 𝒫 dom 𝑅 )
293 292 elpwid ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → ( 𝑔𝑦 ) ⊆ dom 𝑅 )
294 288 293 fssdmd ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → ( 𝑔𝑦 ) ⊆ 𝑄 )
295 simpr ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → 𝑤 ∈ ( 𝑔𝑦 ) )
296 294 295 sseldd ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → 𝑤𝑄 )
297 288 296 ffvelrnd ( ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ 𝑤 ∈ ( 𝑔𝑦 ) ) → ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
298 297 ralrimiva ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ∀ 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
299 fvex ( 𝑔𝑦 ) ∈ V
300 nfcv 𝑤 ( 𝑔𝑦 )
301 300 esumcl ( ( ( 𝑔𝑦 ) ∈ V ∧ ∀ 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
302 299 301 mpan ( ∀ 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
303 298 302 syl ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
304 285 286 287 303 syl21anc ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
305 304 ex ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑦𝑋 → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) ) )
306 284 305 ralrimi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∀ 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
307 18 esumcl ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
308 178 306 307 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
309 105 308 sseldi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ℝ* )
310 nfv 𝑤 ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
311 simpr ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
312 fniunfv ( 𝑔 Fn 𝑋 𝑦𝑋 ( 𝑔𝑦 ) = ran 𝑔 )
313 311 213 312 3syl ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → 𝑦𝑋 ( 𝑔𝑦 ) = ran 𝑔 )
314 310 313 esumeq1d ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → Σ* 𝑤 𝑦𝑋 ( 𝑔𝑦 ) ( 𝑅𝑤 ) = Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) )
315 15 adantr ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → 𝑋 ∈ V )
316 299 a1i ( ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝑔𝑦 ) ∈ V )
317 315 316 297 esumiun ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → Σ* 𝑤 𝑦𝑋 ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
318 314 317 eqbrtrrd ( ( 𝜑𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) ≤ Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
319 13 318 sylan ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) ≤ Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
320 319 adantr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑤 ran 𝑔 ( 𝑅𝑤 ) ≤ Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
321 252 320 eqbrtrid ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ≤ Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) )
322 285 287 46 syl2anc ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
323 simplll ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) )
324 323 287 73 syl2anc ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
325 322 324 xrge0addcld ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
326 325 ex ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑦𝑋 → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) )
327 284 326 ralrimi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∀ 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
328 18 esumcl ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
329 178 327 328 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
330 105 329 sseldi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ℝ* )
331 215 14 syl ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑋 ∈ V )
332 simp-4l ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) )
333 simpr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
334 332 333 49 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ℝ )
335 334 adantr ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ( 𝑀𝐴 ) ∈ ℝ )
336 65 adantlr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
337 336 adantr ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
338 id ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
339 338 adantl ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
340 66 breq2d ( ( ( 𝑀𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ ) → ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ↔ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
341 340 biimpar ( ( ( ( 𝑀𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
342 335 337 339 341 syl21anc ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
343 342 ex ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
344 332 simpld ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → 𝜑 )
345 simplr ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } )
346 344 345 333 303 syl21anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ( 0 [,] +∞ ) )
347 105 346 sseldi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ℝ* )
348 334 rexrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ℝ* )
349 336 rexrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ* )
350 348 349 xaddcld ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ℝ* )
351 xrltle ( ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ∈ ℝ* ∧ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ∈ ℝ* ) → ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
352 347 350 351 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
353 343 352 syld ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
354 353 adantld ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ 𝑦𝑋 ) → ( ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
355 354 ex ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ( 𝑦𝑋 → ( ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) )
356 282 355 ralrimi ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ∀ 𝑦𝑋 ( ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
357 ralim ( ∀ 𝑦𝑋 ( ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ( ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∀ 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
358 356 357 syl ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) → ( ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) → ∀ 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) )
359 358 imp ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∀ 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
360 359 r19.21bi ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
361 284 18 331 304 325 360 esumlef ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
362 164 46 sylan ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ∧ 𝑦𝑋 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
363 284 18 331 362 324 esumaddf ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
364 324 ex ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑦𝑋 → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) ) )
365 284 364 ralrimi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ∀ 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
366 18 esumcl ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
367 178 365 366 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
368 105 367 sseldi ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ* )
369 simp-4r ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑓 : 𝑋1-1→ ℕ )
370 vex 𝑓 ∈ V
371 370 rnex ran 𝑓 ∈ V
372 371 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ran 𝑓 ∈ V )
373 58 frnd ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → ran 𝑓 ⊆ ℕ )
374 373 adantr ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ran 𝑓 ⊆ ℕ )
375 374 sselda ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑧 ∈ ℕ )
376 54 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → 2 ∈ ℝ+ )
377 simpr ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → 𝑧 ∈ ℕ )
378 377 nnzd ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → 𝑧 ∈ ℤ )
379 376 378 rpexpcld ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2 ↑ 𝑧 ) ∈ ℝ+ )
380 379 rpreccld ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ℝ+ )
381 71 380 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
382 381 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
383 375 382 syldan ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ran 𝑓 ) → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
384 383 ralrimiva ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
385 nfcv 𝑧 ran 𝑓
386 385 esumcl ( ( ran 𝑓 ∈ V ∧ ∀ 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
387 372 384 386 syl2anc ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,] +∞ ) )
388 105 387 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ℝ* )
389 1xr 1 ∈ ℝ*
390 389 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 1 ∈ ℝ* )
391 71 sseli ( 𝑒 ∈ ℝ+𝑒 ∈ ( 0 [,] +∞ ) )
392 391 adantl ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ( 0 [,] +∞ ) )
393 elxrge0 ( 𝑒 ∈ ( 0 [,] +∞ ) ↔ ( 𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒 ) )
394 392 393 sylib ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒 ) )
395 nfv 𝑧 ( 𝜑𝑓 : 𝑋1-1→ ℕ )
396 nnex ℕ ∈ V
397 396 a1i ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → ℕ ∈ V )
398 395 397 381 373 esummono ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ≤ Σ* 𝑧 ∈ ℕ ( 1 / ( 2 ↑ 𝑧 ) ) )
399 oveq2 ( 𝑧 = 𝑤 → ( 2 ↑ 𝑧 ) = ( 2 ↑ 𝑤 ) )
400 399 oveq2d ( 𝑧 = 𝑤 → ( 1 / ( 2 ↑ 𝑧 ) ) = ( 1 / ( 2 ↑ 𝑤 ) ) )
401 ioossico ( 0 (,) +∞ ) ⊆ ( 0 [,) +∞ )
402 69 401 eqsstri + ⊆ ( 0 [,) +∞ )
403 402 380 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ( 0 [,) +∞ ) )
404 eqidd ( 𝑧 ∈ ℕ → ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) = ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) )
405 simpr ( ( 𝑧 ∈ ℕ ∧ 𝑤 = 𝑧 ) → 𝑤 = 𝑧 )
406 405 oveq2d ( ( 𝑧 ∈ ℕ ∧ 𝑤 = 𝑧 ) → ( 2 ↑ 𝑤 ) = ( 2 ↑ 𝑧 ) )
407 406 oveq2d ( ( 𝑧 ∈ ℕ ∧ 𝑤 = 𝑧 ) → ( 1 / ( 2 ↑ 𝑤 ) ) = ( 1 / ( 2 ↑ 𝑧 ) ) )
408 id ( 𝑧 ∈ ℕ → 𝑧 ∈ ℕ )
409 ovexd ( 𝑧 ∈ ℕ → ( 1 / ( 2 ↑ 𝑧 ) ) ∈ V )
410 404 407 408 409 fvmptd ( 𝑧 ∈ ℕ → ( ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) ‘ 𝑧 ) = ( 1 / ( 2 ↑ 𝑧 ) ) )
411 410 adantl ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) ‘ 𝑧 ) = ( 1 / ( 2 ↑ 𝑧 ) ) )
412 ax-1cn 1 ∈ ℂ
413 eqid ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) = ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) )
414 413 geo2lim ( 1 ∈ ℂ → seq 1 ( + , ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) ) ⇝ 1 )
415 412 414 ax-mp seq 1 ( + , ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) ) ⇝ 1
416 415 a1i ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → seq 1 ( + , ( 𝑤 ∈ ℕ ↦ ( 1 / ( 2 ↑ 𝑤 ) ) ) ) ⇝ 1 )
417 1re 1 ∈ ℝ
418 417 a1i ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → 1 ∈ ℝ )
419 400 403 411 416 418 esumcvgsum ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑧 ∈ ℕ ( 1 / ( 2 ↑ 𝑧 ) ) = Σ 𝑧 ∈ ℕ ( 1 / ( 2 ↑ 𝑧 ) ) )
420 geoihalfsum Σ 𝑧 ∈ ℕ ( 1 / ( 2 ↑ 𝑧 ) ) = 1
421 419 420 eqtrdi ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑧 ∈ ℕ ( 1 / ( 2 ↑ 𝑧 ) ) = 1 )
422 398 421 breqtrd ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ≤ 1 )
423 422 adantr ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ≤ 1 )
424 xlemul2a ( ( ( Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 𝑒 ∈ ℝ* ∧ 0 ≤ 𝑒 ) ) ∧ Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ≤ 1 ) → ( 𝑒 ·e Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ) ≤ ( 𝑒 ·e 1 ) )
425 388 390 394 423 424 syl31anc ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ·e Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ) ≤ ( 𝑒 ·e 1 ) )
426 17 23 nfan 𝑦 ( 𝜑𝑓 : 𝑋1-1→ ℕ )
427 426 25 nfan 𝑦 ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ )
428 76 recnd ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → 𝑒 ∈ ℂ )
429 78 recnd ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℂ )
430 429 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ∈ ℂ )
431 2cn 2 ∈ ℂ
432 431 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → 2 ∈ ℂ )
433 2ne0 2 ≠ 0
434 433 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → 2 ≠ 0 )
435 432 434 60 expne0d ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ≠ 0 )
436 435 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 2 ↑ ( 𝑓𝑦 ) ) ≠ 0 )
437 428 430 436 divrecd ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = ( 𝑒 · ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
438 1rp 1 ∈ ℝ+
439 438 a1i ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → 1 ∈ ℝ+ )
440 439 61 rpdivcld ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ+ )
441 52 440 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
442 441 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ )
443 rexmul ( ( 𝑒 ∈ ℝ ∧ ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ ) → ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( 𝑒 · ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
444 76 442 443 syl2anc ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( 𝑒 · ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
445 437 444 eqtr4d ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
446 445 ralrimiva ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
447 427 446 esumeq2d ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = Σ* 𝑦𝑋 ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
448 15 ad2antrr ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝑋 ∈ V )
449 71 440 sseldi ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑦𝑋 ) → ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
450 449 adantlr ( ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦𝑋 ) → ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
451 402 a1i ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → ℝ+ ⊆ ( 0 [,) +∞ ) )
452 451 sselda ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ( 0 [,) +∞ ) )
453 448 450 452 esummulc2 ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ·e Σ* 𝑦𝑋 ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = Σ* 𝑦𝑋 ( 𝑒 ·e ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) )
454 nfcv 𝑦 ( 1 / ( 2 ↑ 𝑧 ) )
455 oveq2 ( 𝑧 = ( 𝑓𝑦 ) → ( 2 ↑ 𝑧 ) = ( 2 ↑ ( 𝑓𝑦 ) ) )
456 455 oveq2d ( 𝑧 = ( 𝑓𝑦 ) → ( 1 / ( 2 ↑ 𝑧 ) ) = ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) )
457 15 adantr ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → 𝑋 ∈ V )
458 56 simprbi ( 𝑓 : 𝑋1-1→ ℕ → Fun 𝑓 )
459 57 feqmptd ( 𝑓 : 𝑋1-1→ ℕ → 𝑓 = ( 𝑦𝑋 ↦ ( 𝑓𝑦 ) ) )
460 459 cnveqd ( 𝑓 : 𝑋1-1→ ℕ → 𝑓 = ( 𝑦𝑋 ↦ ( 𝑓𝑦 ) ) )
461 460 funeqd ( 𝑓 : 𝑋1-1→ ℕ → ( Fun 𝑓 ↔ Fun ( 𝑦𝑋 ↦ ( 𝑓𝑦 ) ) ) )
462 458 461 mpbid ( 𝑓 : 𝑋1-1→ ℕ → Fun ( 𝑦𝑋 ↦ ( 𝑓𝑦 ) ) )
463 462 adantl ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Fun ( 𝑦𝑋 ↦ ( 𝑓𝑦 ) ) )
464 454 426 18 456 457 463 449 59 esumc ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑦𝑋 ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = Σ* 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦𝑋 𝑥 = ( 𝑓𝑦 ) } ( 1 / ( 2 ↑ 𝑧 ) ) )
465 ffn ( 𝑓 : 𝑋 ⟶ ℕ → 𝑓 Fn 𝑋 )
466 fnrnfv ( 𝑓 Fn 𝑋 → ran 𝑓 = { 𝑥 ∣ ∃ 𝑦𝑋 𝑥 = ( 𝑓𝑦 ) } )
467 58 465 466 3syl ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → ran 𝑓 = { 𝑥 ∣ ∃ 𝑦𝑋 𝑥 = ( 𝑓𝑦 ) } )
468 395 467 esumeq1d ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) = Σ* 𝑧 ∈ { 𝑥 ∣ ∃ 𝑦𝑋 𝑥 = ( 𝑓𝑦 ) } ( 1 / ( 2 ↑ 𝑧 ) ) )
469 464 468 eqtr4d ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) → Σ* 𝑦𝑋 ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) )
470 469 adantr ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑦𝑋 ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) = Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) )
471 470 oveq2d ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ·e Σ* 𝑦𝑋 ( 1 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) = ( 𝑒 ·e Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ) )
472 447 453 471 3eqtr2rd ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ·e Σ* 𝑧 ∈ ran 𝑓 ( 1 / ( 2 ↑ 𝑧 ) ) ) = Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) )
473 394 simpld ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ* )
474 xmulid1 ( 𝑒 ∈ ℝ* → ( 𝑒 ·e 1 ) = 𝑒 )
475 473 474 syl ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 ·e 1 ) = 𝑒 )
476 425 472 475 3brtr3d ( ( ( 𝜑𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ≤ 𝑒 )
477 164 369 204 476 syl21anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ≤ 𝑒 )
478 xleadd2a ( ( ( Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ∈ ℝ*𝑒 ∈ ℝ* ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ* ) ∧ Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ≤ 𝑒 ) → ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
479 368 205 203 477 478 syl31anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 Σ* 𝑦𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
480 363 479 eqbrtrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 ( ( 𝑀𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
481 309 330 206 361 480 xrletrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑦𝑋 Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
482 201 309 206 321 481 xrletrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → Σ* 𝑐 ran 𝑔 ( 𝑅𝑐 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
483 176 201 206 280 482 xrletrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) )
484 204 rpred ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → 𝑒 ∈ ℝ )
485 rexadd ( ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) = ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
486 202 484 485 syl2anc ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) +𝑒 𝑒 ) = ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
487 483 486 breqtrd ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ) ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
488 487 anasss ( ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
489 488 ex ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) ) )
490 489 exlimdv ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑔 ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅𝑧 ≼ ω } ∧ ∀ 𝑦𝑋 ( 𝐴 ( 𝑔𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔𝑦 ) ( 𝑅𝑤 ) < ( ( 𝑀𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓𝑦 ) ) ) ) ) ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) ) )
491 163 490 mpd ( ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
492 491 ralrimiva ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) → ∀ 𝑒 ∈ ℝ+ ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) )
493 xralrple ( ( ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) ) )
494 175 493 sylan ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) ) )
495 494 adantr ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) → ( ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 𝑦𝑋 𝐴 ) ≤ ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) + 𝑒 ) ) )
496 492 495 mpbird ( ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋1-1→ ℕ ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) )
497 496 ex ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( 𝑓 : 𝑋1-1→ ℕ → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ) )
498 497 exlimdv ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( ∃ 𝑓 𝑓 : 𝑋1-1→ ℕ → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ) )
499 12 498 mpd ( ( 𝜑 ∧ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) )
500 175 adantr ( ( 𝜑 ∧ ¬ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* )
501 pnfge ( ( 𝑀 𝑦𝑋 𝐴 ) ∈ ℝ* → ( 𝑀 𝑦𝑋 𝐴 ) ≤ +∞ )
502 500 501 syl ( ( 𝜑 ∧ ¬ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ +∞ )
503 46 ralrimiva ( 𝜑 → ∀ 𝑦𝑋 ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
504 18 esumcl ( ( 𝑋 ∈ V ∧ ∀ 𝑦𝑋 ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
505 15 503 504 syl2anc ( 𝜑 → Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
506 xrge0nre ( ( Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) ∧ ¬ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) = +∞ )
507 505 506 sylan ( ( 𝜑 ∧ ¬ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → Σ* 𝑦𝑋 ( 𝑀𝐴 ) = +∞ )
508 502 507 breqtrrd ( ( 𝜑 ∧ ¬ Σ* 𝑦𝑋 ( 𝑀𝐴 ) ∈ ℝ ) → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) )
509 499 508 pm2.61dan ( 𝜑 → ( 𝑀 𝑦𝑋 𝐴 ) ≤ Σ* 𝑦𝑋 ( 𝑀𝐴 ) )