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) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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