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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
67	51 65 66	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
68	13 46	sylan	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
69		dfrp2	⊢ ℝ+ = ( 0 (,) +∞ )
70		ioossicc	⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
71	69 70	eqsstri	⊢ ℝ+ ⊆ ( 0 [,] +∞ )
72	71 63	sselid	⊢ ( ( ( ( 𝜑 ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
73	72	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
74	68 73	xrge0addcld	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
75	67 74	eqeltrrd	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
76	52 53	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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) ∈ ℝ* )
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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
326	325	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑦 ∈ 𝑋 → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) )
327	284 326	ralrimi	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
328	18	esumcl	⊢ ( ( 𝑋 ∈ V ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
329	178 327 328	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ( 0 [,] +∞ ) )
330	105 329	sselid	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℝ* )
331	215 14	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → 𝑋 ∈ V )
332		simp-4l	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) )
333		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
334	332 333 49	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
335	334	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
336	65	adantlr	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ )
337	336	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ )
338		id	⊢ ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
339	338	adantl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
340	66	breq2d	⊢ ( ( ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
341	340	biimpar	⊢ ( ( ( ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
342	335 337 339 341	syl21anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
343	342	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
344	332	simpld	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → 𝜑 )
345		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } )
346	344 345 333 303	syl21anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ∈ ( 0 [,] +∞ ) )
347	105 346	sselid	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ∈ ℝ* )
348	334	rexrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
349	336	rexrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ℝ* )
350	348 349	xaddcld	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℝ* )
351		xrltle	⊢ ( ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ∈ ℝ* ∧ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℝ* ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
352	347 350 351	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
353	343 352	syld	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
354	353	adantld	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
355	354	ex	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ( 𝑦 ∈ 𝑋 → ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) )
356	282 355	ralrimi	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
357		ralim	⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
358	356 357	syl	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
359	358	imp	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
360	359	r19.21bi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
361	284 18 331 304 325 360	esumlef	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
362	164 46	sylan	⊢ ( ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
363	284 18 331 362 324	esumaddf	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) )
364	324	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑦 ∈ 𝑋 → ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) ) )
365	284 364	ralrimi	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
366	18	esumcl	⊢ ( ( 𝑋 ∈ V ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
367	178 365 366	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ∈ ( 0 [,] +∞ ) )
368	105 367	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 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ≤ 𝑒 ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
479	368 205 203 477 478	syl31anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 Σ* 𝑦 ∈ 𝑋 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
480	363 479	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
481	309 330 206 361 480	xrletrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑦 ∈ 𝑋 Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
482	201 309 206 321 481	xrletrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → Σ* 𝑐 ∈ ∪ ran 𝑔 ( 𝑅 ‘ 𝑐 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
483	176 201 206 280 482	xrletrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) )
484	204	rpred	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → 𝑒 ∈ ℝ )
485		rexadd	⊢ ( ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
486	202 484 485	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) +𝑒 𝑒 ) = ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
487	483 486	breqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
488	487	anasss	⊢ ( ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
489	488	ex	⊢ ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) ) )
490	489	exlimdv	⊢ ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑔 ( 𝑔 : 𝑋 ⟶ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω } ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐴 ⊆ ∪ ( 𝑔 ‘ 𝑦 ) ∧ Σ* 𝑤 ∈ ( 𝑔 ‘ 𝑦 ) ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + ( 𝑒 / ( 2 ↑ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) ) )
491	163 490	mpd	⊢ ( ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
492	491	ralrimiva	⊢ ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) → ∀ 𝑒 ∈ ℝ+ ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) )
493		xralrple	⊢ ( ( ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ∈ ℝ* ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) ) )
494	175 493	sylan	⊢ ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) ) )
495	494	adantr	⊢ ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) → ( ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ+ ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) + 𝑒 ) ) )
496	492 495	mpbird	⊢ ( ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑓 : 𝑋 –1-1→ ℕ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) )
497	496	ex	⊢ ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( 𝑓 : 𝑋 –1-1→ ℕ → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ) )
498	497	exlimdv	⊢ ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( ∃ 𝑓 𝑓 : 𝑋 –1-1→ ℕ → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ) )
499	12 498	mpd	⊢ ( ( 𝜑 ∧ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) )
500	175	adantr	⊢ ( ( 𝜑 ∧ ¬ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ∈ ℝ* )
501		pnfge	⊢ ( ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ∈ ℝ* → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ +∞ )
502	500 501	syl	⊢ ( ( 𝜑 ∧ ¬ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ +∞ )
503	46	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
504	18	esumcl	⊢ ( ( 𝑋 ∈ V ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
505	15 503 504	syl2anc	⊢ ( 𝜑 → Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
506		xrge0nre	⊢ ( ( Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ∧ ¬ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) = +∞ )
507	505 506	sylan	⊢ ( ( 𝜑 ∧ ¬ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) = +∞ )
508	502 507	breqtrrd	⊢ ( ( 𝜑 ∧ ¬ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) ∈ ℝ ) → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) )
509	499 508	pm2.61dan	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑦 ∈ 𝑋 𝐴 ) ≤ Σ* 𝑦 ∈ 𝑋 ( 𝑀 ‘ 𝐴 ) )