omeiunltfirp

Description: If the outer measure of a countable union is not +oo , then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omeiunltfirp.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omeiunltfirp.x	⊢ 𝑋 = ∪ dom 𝑂
	omeiunltfirp.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑁 )
	omeiunltfirp.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
	omeiunltfirp.re	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
	omeiunltfirp.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ⁺ )
Assertion	omeiunltfirp	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		omeiunltfirp.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omeiunltfirp.x	⊢ 𝑋 = ∪ dom 𝑂
3		omeiunltfirp.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑁 )
4		omeiunltfirp.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
5		omeiunltfirp.re	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
6		omeiunltfirp.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ⁺ )
7	3	fvexi	⊢ 𝑍 ∈ V
8	7	a1i	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → 𝑍 ∈ V )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑂 ∈ OutMeas )
10	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
11		fvex	⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
12	11	elpw	⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 ↔ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
13	10 12	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
14	9 2 13	omecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
15		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
16	14 15	fmptd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑍 ⟶ ( 0 [,] +∞ ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑍 ⟶ ( 0 [,] +∞ ) )
18		simpr	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ )
19	5	adantr	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
20	8 17 18 19	sge0pnffigt	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) )
21		simpl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) )
22		simpr	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) )
23		elpwinss	⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑧 ⊆ 𝑍 )
24	23	resmptd	⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) = ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
25	24	fveq2d	⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
26	25	adantr	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) = ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
27	22 26	breqtrd	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
28	27	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
29	5	rexrd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ^* )
30	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ^* )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) )
32	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝑂 ∈ OutMeas )
33	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
34	23	adantr	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑧 ⊆ 𝑍 )
35		simpr	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑧 )
36	34 35	sseldd	⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑍 )
37	36	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑍 )
38	33 37	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
39	38 12	sylib	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
40	32 2 39	omecl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
41		eqid	⊢ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
42	40 41	fmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑧 ⟶ ( 0 [,] +∞ ) )
43	31 42	sge0xrcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ^* )
44	43	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ^* )
45		elinel2	⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑧 ∈ Fin )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ∈ Fin )
47		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
48		0xr	⊢ 0 ∈ ℝ^*
49	48	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 0 ∈ ℝ^* )
50		pnfxr	⊢ +∞ ∈ ℝ^*
51	50	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → +∞ ∈ ℝ^* )
52	32 2 39	omexrcl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ^* )
53		iccgelb	⊢ ( ( 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
54	49 51 40 53	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 0 ≤ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
55	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
56		iunss	⊢ ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
57	55 56	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
58	57	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
59	32 2 58	omexrcl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ^* )
60		ssiun2	⊢ ( 𝑛 ∈ 𝑍 → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
61	37 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
62	32 2 58 61	omessle	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
63	5	ltpnfd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < +∞ )
64	63	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < +∞ )
65	52 59 51 62 64	xrlelttrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ )
66	49 51 52 54 65	elicod	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) )
67	47 66	sseldi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
68	46 67	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
69	6	rpred	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
70	69	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑌 ∈ ℝ )
71	68 70	readdcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ∈ ℝ )
72	71	rexrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ∈ ℝ^* )
73	72	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ∈ ℝ^* )
74		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
75	66 41	fmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑧 ⟶ ( 0 [,) +∞ ) )
76	46 75	sge0fsum	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = Σ 𝑘 ∈ 𝑧 ( ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
77		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
78		2fveq3	⊢ ( 𝑛 = 𝑘 → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) )
79	78	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) ∧ 𝑛 = 𝑘 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) )
80		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → 𝑘 ∈ 𝑧 )
81		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) ∈ V )
82	77 79 80 81	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑧 ) → ( ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) )
83	82	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 ( ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) )
84		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
85	84	cbvsumv	⊢ Σ 𝑘 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) )
86	85	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑘 ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
87	76 83 86	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
88	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑌 ∈ ℝ⁺ )
89	68 88	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
90	87 89	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
91	90	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
92	30 44 73 74 91	xrlttrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
93	21 28 92	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
94	93	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ) )
95	94	adantlr	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ) )
96	95	reximdva	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ^{^} ‘ ( ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑧 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ) )
97	20 96	mpd	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
98		simpl	⊢ ( ( 𝜑 ∧ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → 𝜑 )
99		simpr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ )
100	7	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
101	100 16	sge0repnf	⊢ ( 𝜑 → ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) )
102	101	adantr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ↔ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) )
103	99 102	mpbird	⊢ ( ( 𝜑 ∧ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ )
104		nfv	⊢ Ⅎ 𝑛 𝜑
105		nfcv	⊢ Ⅎ 𝑛 Σ^{^}
106		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
107	105 106	nffv	⊢ Ⅎ 𝑛 ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
108		nfcv	⊢ Ⅎ 𝑛 ℝ
109	107 108	nfel	⊢ Ⅎ 𝑛 ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ
110	104 109	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ )
111	7	a1i	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → 𝑍 ∈ V )
112	14	adantlr	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
113	6	adantr	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → 𝑌 ∈ ℝ⁺ )
114		simpr	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ )
115	110 111 112 113 114	sge0ltfirpmpt	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) )
116	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ )
117	114	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ )
118	71	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ∈ ℝ )
119		nfcv	⊢ Ⅎ 𝑛 𝐸
120	104 119 1 2 3 4	omeiunle	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
121	120	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
122		simpr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) )
123		simpll	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝜑 )
124		2fveq3	⊢ ( 𝑛 = 𝑚 → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) )
125	124	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) )
126	125	fveq2i	⊢ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) )
127	126	eleq1i	⊢ ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ↔ ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ )
128	127	biimpi	⊢ ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ → ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ )
129	128	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ )
130		simpr	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) )
131	45	adantl	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ∈ Fin )
132	66	adantllr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) )
133	131 132	sge0fsummpt	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
134	123 129 130 133	syl21anc	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
135	134	oveq1d	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) = ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
136	135	adantr	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) = ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
137	122 136	breqtrd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
138	116 117 118 121 137	lelttrd	⊢ ( ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
139	138	ex	⊢ ( ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ) )
140	139	reximdva	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) < ( ( Σ^{^} ‘ ( 𝑛 ∈ 𝑧 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) + 𝑌 ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) ) )
141	115 140	mpd	⊢ ( ( 𝜑 ∧ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
142	98 103 141	syl2anc	⊢ ( ( 𝜑 ∧ ¬ ( Σ^{^} ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = +∞ ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )
143	97 142	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) + 𝑌 ) )

Metamath Proof Explorer

Theorem omeiunltfirp

Proof