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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ )
65 64 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ )
66 rexadd ⊢ ( ( ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
67 51 65 66 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
68 13 46 sylan ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
69 dfrp2 ⊢ ℝ+ = ( 0 (,) +∞ )
70 ioossicc ⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
71 69 70 eqsstri ⊢ ℝ+ ⊆ ( 0 [,] +∞ )
72 71 63 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
73 72 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
74 68 73 xrge0addcld ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
75 67 74 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
76 52 53 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → 𝑒 ∈ ℝ )
77 76 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → 𝑒 ∈ ℝ )
78 52 61 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) = 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 biimtrid ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –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 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ∈ ( 0 [,] +∞ ) )
175 105 174 sselid ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ∈ ℝ* )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 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 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) ∈ ℝ* )
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 eqtrid ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) = 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 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑦 ) ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } )
292 186 291 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝒫 dom 𝑅 )
293 292 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑦 ) ⊆ dom 𝑅 )
294 288 293 fssdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑦 ) ⊆ 𝑄 )
295 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) )
296 294 295 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ) → 𝑤 ∈ 𝑄 )
297 288 296 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 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 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
326 325 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑦 ∈ 𝑋 → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) )
327 284 326 ralrimi ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
328 18 esumcl ⊢ ( ( 𝑋 ∈ V ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
329 178 327 328 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
330 105 329 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
341 340 biimpar ⊢ ( ( ( ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
342 335 337 339 341 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
343 342 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 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 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ∈ ℝ* )
348 334 rexrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
349 336 rexrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ* )
350 348 349 xaddcld ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℝ* )
351 xrltle ⊢ ( ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ∈ ℝ* ∧ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℝ* ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
352 347 350 351 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
353 343 352 syld ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
354 353 adantld ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
355 354 ex ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ( 𝑦 ∈ 𝑋 → ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) )
356 282 355 ralrimi ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
357 ralim ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
358 356 357 syl ⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
359 358 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
360 359 r19.21bi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
361 284 18 331 304 325 360 esumlef ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
362 164 46 sylan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
363 284 18 331 362 324 esumaddf ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 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 sselid ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 sselid ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –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 xmulrid ⊢ ( 𝑒 ∈ ℝ* → ( 𝑒 ·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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ≤ 𝑒 ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
479 368 205 203 477 478 syl31anc ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
480 363 479 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
481 309 330 206 361 480 xrletrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
482 201 309 206 321 481 xrletrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑐 ∈ ∪ ran 𝑔 ( 𝑅 ‘ 𝑐 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
483 176 201 206 280 482 xrletrd ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) )
484 204 rpred ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → 𝑒 ∈ ℝ )
485 rexadd ⊢ ( ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
486 202 484 485 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +e 𝑒 ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
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 ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) )