carageniuncllem2

Description: The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageniuncllem2.o	$⊢ φ \to O \in OutMeas$
	carageniuncllem2.s	$⊢ S = CaraGen (O)$
	carageniuncllem2.x	$⊢ X = ⋃ dom O$
	carageniuncllem2.a	$⊢ φ \to A \subseteq X$
	carageniuncllem2.re	$⊢ φ \to O (A) \in ℝ$
	carageniuncllem2.m	$⊢ φ \to M \in ℤ$
	carageniuncllem2.z	$⊢ Z = ℤ_{\geq M}$
	carageniuncllem2.e	$⊢ φ \to E : Z ⟶ S$
	carageniuncllem2.y	$⊢ φ \to Y \in ℝ^{+}$
	carageniuncllem2.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
	carageniuncllem2.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (M ..^n)} E (i))$
Assertion	carageniuncllem2	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y$

Proof

Step	Hyp	Ref	Expression
1		carageniuncllem2.o	$⊢ φ \to O \in OutMeas$
2		carageniuncllem2.s	$⊢ S = CaraGen (O)$
3		carageniuncllem2.x	$⊢ X = ⋃ dom O$
4		carageniuncllem2.a	$⊢ φ \to A \subseteq X$
5		carageniuncllem2.re	$⊢ φ \to O (A) \in ℝ$
6		carageniuncllem2.m	$⊢ φ \to M \in ℤ$
7		carageniuncllem2.z	$⊢ Z = ℤ_{\geq M}$
8		carageniuncllem2.e	$⊢ φ \to E : Z ⟶ S$
9		carageniuncllem2.y	$⊢ φ \to Y \in ℝ^{+}$
10		carageniuncllem2.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
11		carageniuncllem2.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (M ..^n)} E (i))$
12		inss1	$⊢ A \cap ⋃_{n \in Z} E (n) \subseteq A$
13	12	a1i	$⊢ φ \to A \cap ⋃_{n \in Z} E (n) \subseteq A$
14	1 3 4 5 13	omessre	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) \in ℝ$
15		difssd	$⊢ φ \to A ∖ ⋃_{n \in Z} E (n) \subseteq A$
16	1 3 4 5 15	omessre	$⊢ φ \to O (A ∖ ⋃_{n \in Z} E (n)) \in ℝ$
17		rexadd	$⊢ (O (A \cap ⋃_{n \in Z} E (n)) \in ℝ \land O (A ∖ ⋃_{n \in Z} E (n)) \in ℝ) \to O (A \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (A ∖ ⋃_{n \in Z} E (n)) = O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n))$
18	14 16 17	syl2anc	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (A ∖ ⋃_{n \in Z} E (n)) = O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n))$
19		ssinss1	$⊢ A \subseteq X \to A \cap F (n) \subseteq X$
20	4 19	syl	$⊢ φ \to A \cap F (n) \subseteq X$
21	1 3	unidmex	$⊢ φ \to X \in V$
22		ssexg	$⊢ (A \subseteq X \land X \in V) \to A \in V$
23	4 21 22	syl2anc	$⊢ φ \to A \in V$
24		inex1g	$⊢ A \in V \to A \cap F (n) \in V$
25	23 24	syl	$⊢ φ \to A \cap F (n) \in V$
26		elpwg	$⊢ A \cap F (n) \in V \to (A \cap F (n) \in 𝒫 X \leftrightarrow A \cap F (n) \subseteq X)$
27	25 26	syl	$⊢ φ \to (A \cap F (n) \in 𝒫 X \leftrightarrow A \cap F (n) \subseteq X)$
28	20 27	mpbird	$⊢ φ \to A \cap F (n) \in 𝒫 X$
29	28	adantr	$⊢ (φ \land n \in Z) \to A \cap F (n) \in 𝒫 X$
30		eqid	$⊢ (n \in Z ⟼ A \cap F (n)) = (n \in Z ⟼ A \cap F (n))$
31	29 30	fmptd	$⊢ φ \to (n \in Z ⟼ A \cap F (n)) : Z ⟶ 𝒫 X$
32		fveq2	$⊢ k = n \to F (k) = F (n)$
33	32	ineq2d	$⊢ k = n \to A \cap F (k) = A \cap F (n)$
34	33	cbvmptv	$⊢ (k \in Z ⟼ A \cap F (k)) = (n \in Z ⟼ A \cap F (n))$
35	34	feq1i	$⊢ (k \in Z ⟼ A \cap F (k)) : Z ⟶ 𝒫 X \leftrightarrow (n \in Z ⟼ A \cap F (n)) : Z ⟶ 𝒫 X$
36	35	a1i	$⊢ φ \to ((k \in Z ⟼ A \cap F (k)) : Z ⟶ 𝒫 X \leftrightarrow (n \in Z ⟼ A \cap F (n)) : Z ⟶ 𝒫 X)$
37	31 36	mpbird	$⊢ φ \to (k \in Z ⟼ A \cap F (k)) : Z ⟶ 𝒫 X$
38		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
39	25	adantr	$⊢ (φ \land n \in Z) \to A \cap F (n) \in V$
40	34	fvmpt2	$⊢ (n \in Z \land A \cap F (n) \in V) \to (k \in Z ⟼ A \cap F (k)) (n) = A \cap F (n)$
41	38 39 40	syl2anc	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ A \cap F (k)) (n) = A \cap F (n)$
42	41	iuneq2dv	$⊢ φ \to ⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n) = ⋃_{n \in Z} (A \cap F (n))$
43	42	fveq2d	$⊢ φ \to O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) = O (⋃_{n \in Z} (A \cap F (n)))$
44		nfv	$⊢ Ⅎ n φ$
45	44 7 8 11	iundjiun	$⊢ φ \to ((\forall m \in Z ⋃_{n = M}^{m} F (n) = ⋃_{n = M}^{m} E (n) \land ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)) \land \underset{n \in Z}{Disj} F (n))$
46	45	simplrd	$⊢ φ \to ⋃_{n \in Z} F (n) = ⋃_{n \in Z} E (n)$
47	46	eqcomd	$⊢ φ \to ⋃_{n \in Z} E (n) = ⋃_{n \in Z} F (n)$
48	47	ineq2d	$⊢ φ \to A \cap ⋃_{n \in Z} E (n) = A \cap ⋃_{n \in Z} F (n)$
49		iunin2	$⊢ ⋃_{n \in Z} (A \cap F (n)) = A \cap ⋃_{n \in Z} F (n)$
50	49	eqcomi	$⊢ A \cap ⋃_{n \in Z} F (n) = ⋃_{n \in Z} (A \cap F (n))$
51	50	a1i	$⊢ φ \to A \cap ⋃_{n \in Z} F (n) = ⋃_{n \in Z} (A \cap F (n))$
52	48 51	eqtrd	$⊢ φ \to A \cap ⋃_{n \in Z} E (n) = ⋃_{n \in Z} (A \cap F (n))$
53	52	fveq2d	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) = O (⋃_{n \in Z} (A \cap F (n)))$
54	53 14	eqeltrrd	$⊢ φ \to O (⋃_{n \in Z} (A \cap F (n))) \in ℝ$
55	43 54	eqeltrd	$⊢ φ \to O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) \in ℝ$
56	1 3 7 37 55 9	omeiunltfirp	$⊢ φ \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) < \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) + Y$
57	43	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) = O (⋃_{n \in Z} (A \cap F (n)))$
58		elpwinss	$⊢ z \in (𝒫 Z \cap Fin) \to z \subseteq Z$
59	58	adantr	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to z \subseteq Z$
60		simpr	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to n \in z$
61	59 60	sseldd	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to n \in Z$
62	61	adantll	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to n \in Z$
63	25	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to A \cap F (n) \in V$
64	62 63 40	syl2anc	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to (k \in Z ⟼ A \cap F (k)) (n) = A \cap F (n)$
65	64	fveq2d	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O ((k \in Z ⟼ A \cap F (k)) (n)) = O (A \cap F (n))$
66	65	sumeq2dv	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) = \sum_{n \in z} O (A \cap F (n))$
67	66	oveq1d	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) + Y = \sum_{n \in z} O (A \cap F (n)) + Y$
68	57 67	breq12d	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to (O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) < \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) + Y \leftrightarrow O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y)$
69	68	biimpd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to (O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) < \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) + Y \to O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y)$
70	69	reximdva	$⊢ φ \to (\exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} (k \in Z ⟼ A \cap F (k)) (n)) < \sum_{n \in z} O ((k \in Z ⟼ A \cap F (k)) (n)) + Y \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y)$
71	56 70	mpd	$⊢ φ \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y$
72	6	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to M \in ℤ$
73	58	adantl	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to z \subseteq Z$
74		elinel2	$⊢ z \in (𝒫 Z \cap Fin) \to z \in Fin$
75	74	adantl	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to z \in Fin$
76	72 7 73 75	uzfissfz	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \exists k \in Z z \subseteq (M \dots k)$
77	76	adantr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \to \exists k \in Z z \subseteq (M \dots k)$
78	54	ad3antrrr	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to O (⋃_{n \in Z} (A \cap F (n))) \in ℝ$
79		fzfid	$⊢ z \subseteq (M \dots k) \to (M \dots k) \in Fin$
80		id	$⊢ z \subseteq (M \dots k) \to z \subseteq (M \dots k)$
81		ssfi	$⊢ ((M \dots k) \in Fin \land z \subseteq (M \dots k)) \to z \in Fin$
82	79 80 81	syl2anc	$⊢ z \subseteq (M \dots k) \to z \in Fin$
83	82	adantl	$⊢ (φ \land z \subseteq (M \dots k)) \to z \in Fin$
84	1	ad2antrr	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in z) \to O \in OutMeas$
85	4	ad2antrr	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in z) \to A \subseteq X$
86	5	ad2antrr	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in z) \to O (A) \in ℝ$
87		inss1	$⊢ A \cap F (n) \subseteq A$
88	87	a1i	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in z) \to A \cap F (n) \subseteq A$
89	84 3 85 86 88	omessre	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in z) \to O (A \cap F (n)) \in ℝ$
90	83 89	fsumrecl	$⊢ (φ \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) \in ℝ$
91	9	rpred	$⊢ φ \to Y \in ℝ$
92	91	adantr	$⊢ (φ \land z \subseteq (M \dots k)) \to Y \in ℝ$
93	90 92	readdcld	$⊢ (φ \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) + Y \in ℝ$
94	93	ad4ant14	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) + Y \in ℝ$
95		fzfid	$⊢ φ \to (M \dots k) \in Fin$
96	87	a1i	$⊢ φ \to A \cap F (n) \subseteq A$
97	1 3 4 5 96	omessre	$⊢ φ \to O (A \cap F (n)) \in ℝ$
98	97	adantr	$⊢ (φ \land n \in (M \dots k)) \to O (A \cap F (n)) \in ℝ$
99	95 98	fsumrecl	$⊢ φ \to \sum_{n = M}^{k} O (A \cap F (n)) \in ℝ$
100	99	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n = M}^{k} O (A \cap F (n)) \in ℝ$
101	91	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to Y \in ℝ$
102	100 101	readdcld	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n = M}^{k} O (A \cap F (n)) + Y \in ℝ$
103	102	ad2antrr	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to \sum_{n = M}^{k} O (A \cap F (n)) + Y \in ℝ$
104		simplr	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y$
105	99	adantr	$⊢ (φ \land z \subseteq (M \dots k)) \to \sum_{n = M}^{k} O (A \cap F (n)) \in ℝ$
106		fzfid	$⊢ (φ \land z \subseteq (M \dots k)) \to (M \dots k) \in Fin$
107	98	adantlr	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in (M \dots k)) \to O (A \cap F (n)) \in ℝ$
108		0xr	$⊢ 0 \in ℝ^{*}$
109	108	a1i	$⊢ (φ \land n \in (M \dots k)) \to 0 \in ℝ^{*}$
110		pnfxr	$⊢ +∞ \in ℝ^{*}$
111	110	a1i	$⊢ (φ \land n \in (M \dots k)) \to +∞ \in ℝ^{*}$
112	1 3 20	omecl	$⊢ φ \to O (A \cap F (n)) \in [0, +∞]$
113	112	adantr	$⊢ (φ \land n \in (M \dots k)) \to O (A \cap F (n)) \in [0, +∞]$
114		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land O (A \cap F (n)) \in [0, +∞]) \to 0 \leq O (A \cap F (n))$
115	109 111 113 114	syl3anc	$⊢ (φ \land n \in (M \dots k)) \to 0 \leq O (A \cap F (n))$
116	115	adantlr	$⊢ ((φ \land z \subseteq (M \dots k)) \land n \in (M \dots k)) \to 0 \leq O (A \cap F (n))$
117		simpr	$⊢ (φ \land z \subseteq (M \dots k)) \to z \subseteq (M \dots k)$
118	106 107 116 117	fsumless	$⊢ (φ \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) \leq \sum_{n = M}^{k} O (A \cap F (n))$
119	90 105 92 118	leadd1dd	$⊢ (φ \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) + Y \leq \sum_{n = M}^{k} O (A \cap F (n)) + Y$
120	119	ad4ant14	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to \sum_{n \in z} O (A \cap F (n)) + Y \leq \sum_{n = M}^{k} O (A \cap F (n)) + Y$
121	78 94 103 104 120	ltletrd	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \land z \subseteq (M \dots k)) \to O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
122	121	ex	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \to (z \subseteq (M \dots k) \to O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y)$
123	122	reximdv	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \to (\exists k \in Z z \subseteq (M \dots k) \to \exists k \in Z O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y)$
124	77 123	mpd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y) \to \exists k \in Z O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
125	124	rexlimdva2	$⊢ φ \to (\exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n \in z} O (A \cap F (n)) + Y \to \exists k \in Z O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y)$
126	71 125	mpd	$⊢ φ \to \exists k \in Z O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
127	53	ad2antrr	$⊢ ((φ \land k \in Z) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) = O (⋃_{n \in Z} (A \cap F (n)))$
128		simpr	$⊢ ((φ \land k \in Z) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
129	127 128	eqbrtrd	$⊢ ((φ \land k \in Z) \land O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
130	129	ex	$⊢ (φ \land k \in Z) \to (O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y \to O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y)$
131	130	reximdva	$⊢ φ \to (\exists k \in Z O (⋃_{n \in Z} (A \cap F (n))) < \sum_{n = M}^{k} O (A \cap F (n)) + Y \to \exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y)$
132	126 131	mpd	$⊢ φ \to \exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
133		simpr	$⊢ ((φ \land k \in Z) \land O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y$
134	1	adantr	$⊢ (φ \land k \in Z) \to O \in OutMeas$
135	4	adantr	$⊢ (φ \land k \in Z) \to A \subseteq X$
136	5	adantr	$⊢ (φ \land k \in Z) \to O (A) \in ℝ$
137	8	adantr	$⊢ (φ \land k \in Z) \to E : Z ⟶ S$
138		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
139	134 2 3 135 136 7 137 10 11 138	carageniuncllem1	$⊢ (φ \land k \in Z) \to \sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k))$
140	139	oveq1d	$⊢ (φ \land k \in Z) \to \sum_{n = M}^{k} O (A \cap F (n)) + Y = O (A \cap G (k)) + Y$
141	140	adantr	$⊢ ((φ \land k \in Z) \land O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to \sum_{n = M}^{k} O (A \cap F (n)) + Y = O (A \cap G (k)) + Y$
142	133 141	breqtrd	$⊢ ((φ \land k \in Z) \land O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y$
143	142	ex	$⊢ (φ \land k \in Z) \to (O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y \to O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y)$
144	143	reximdva	$⊢ φ \to (\exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < \sum_{n = M}^{k} O (A \cap F (n)) + Y \to \exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y)$
145	132 144	mpd	$⊢ φ \to \exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y$
146	14	3ad2ant1	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) \in ℝ$
147	16	3ad2ant1	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A ∖ ⋃_{n \in Z} E (n)) \in ℝ$
148		inss1	$⊢ A \cap G (k) \subseteq A$
149	148	a1i	$⊢ (φ \land k \in Z) \to A \cap G (k) \subseteq A$
150	134 3 135 136 149	omessre	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) \in ℝ$
151	91	adantr	$⊢ (φ \land k \in Z) \to Y \in ℝ$
152	150 151	readdcld	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + Y \in ℝ$
153	152	3adant3	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap G (k)) + Y \in ℝ$
154		difssd	$⊢ (φ \land k \in Z) \to A ∖ G (k) \subseteq A$
155	134 3 135 136 154	omessre	$⊢ (φ \land k \in Z) \to O (A ∖ G (k)) \in ℝ$
156	155	3adant3	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A ∖ G (k)) \in ℝ$
157		simp3	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y$
158	146 153 157	ltled	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) \leq O (A \cap G (k)) + Y$
159	135	ssdifssd	$⊢ (φ \land k \in Z) \to A ∖ G (k) \subseteq X$
160		oveq2	$⊢ n = k \to (M \dots n) = (M \dots k)$
161	160	iuneq1d	$⊢ n = k \to ⋃_{i = M}^{n} E (i) = ⋃_{i = M}^{k} E (i)$
162		ovex	$⊢ (M \dots k) \in V$
163		fvex	$⊢ E (i) \in V$
164	162 163	iunex	$⊢ ⋃_{i = M}^{k} E (i) \in V$
165	161 10 164	fvmpt	$⊢ k \in Z \to G (k) = ⋃_{i = M}^{k} E (i)$
166		fveq2	$⊢ i = n \to E (i) = E (n)$
167	166	cbviunv	$⊢ ⋃_{i = M}^{k} E (i) = ⋃_{n = M}^{k} E (n)$
168	167	a1i	$⊢ k \in Z \to ⋃_{i = M}^{k} E (i) = ⋃_{n = M}^{k} E (n)$
169	165 168	eqtrd	$⊢ k \in Z \to G (k) = ⋃_{n = M}^{k} E (n)$
170		elfzuz	$⊢ i \in (M \dots k) \to i \in ℤ_{\geq M}$
171	7	eqcomi	$⊢ ℤ_{\geq M} = Z$
172	171	a1i	$⊢ i \in (M \dots k) \to ℤ_{\geq M} = Z$
173	170 172	eleqtrd	$⊢ i \in (M \dots k) \to i \in Z$
174	173	ssriv	$⊢ (M \dots k) \subseteq Z$
175		iunss1	$⊢ (M \dots k) \subseteq Z \to ⋃_{n = M}^{k} E (n) \subseteq ⋃_{n \in Z} E (n)$
176	174 175	ax-mp	$⊢ ⋃_{n = M}^{k} E (n) \subseteq ⋃_{n \in Z} E (n)$
177	176	a1i	$⊢ k \in Z \to ⋃_{n = M}^{k} E (n) \subseteq ⋃_{n \in Z} E (n)$
178	169 177	eqsstrd	$⊢ k \in Z \to G (k) \subseteq ⋃_{n \in Z} E (n)$
179	178	adantl	$⊢ (φ \land k \in Z) \to G (k) \subseteq ⋃_{n \in Z} E (n)$
180	179	sscond	$⊢ (φ \land k \in Z) \to A ∖ ⋃_{n \in Z} E (n) \subseteq A ∖ G (k)$
181	134 3 159 180	omessle	$⊢ (φ \land k \in Z) \to O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A ∖ G (k))$
182	181	3adant3	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A ∖ G (k))$
183	146 147 153 156 158 182	le2addd	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A \cap G (k)) + Y + O (A ∖ G (k))$
184	150	recnd	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) \in ℂ$
185	91	recnd	$⊢ φ \to Y \in ℂ$
186	185	adantr	$⊢ (φ \land k \in Z) \to Y \in ℂ$
187	155	recnd	$⊢ (φ \land k \in Z) \to O (A ∖ G (k)) \in ℂ$
188	184 186 187	add32d	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + Y + O (A ∖ G (k)) = O (A \cap G (k)) + O (A ∖ G (k)) + Y$
189		rexadd	$⊢ (O (A \cap G (k)) \in ℝ \land O (A ∖ G (k)) \in ℝ) \to O (A \cap G (k)) +_{𝑒} O (A ∖ G (k)) = O (A \cap G (k)) + O (A ∖ G (k))$
190	150 155 189	syl2anc	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) +_{𝑒} O (A ∖ G (k)) = O (A \cap G (k)) + O (A ∖ G (k))$
191	190	eqcomd	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + O (A ∖ G (k)) = O (A \cap G (k)) +_{𝑒} O (A ∖ G (k))$
192		nfv	$⊢ Ⅎ i φ$
193	8	adantr	$⊢ (φ \land i \in (M \dots k)) \to E : Z ⟶ S$
194	173	adantl	$⊢ (φ \land i \in (M \dots k)) \to i \in Z$
195	193 194	ffvelcdmd	$⊢ (φ \land i \in (M \dots k)) \to E (i) \in S$
196	192 1 2 95 195	caragenfiiuncl	$⊢ φ \to ⋃_{i = M}^{k} E (i) \in S$
197	196	adantr	$⊢ (φ \land k \in Z) \to ⋃_{i = M}^{k} E (i) \in S$
198	10 161 138 197	fvmptd3	$⊢ (φ \land k \in Z) \to G (k) = ⋃_{i = M}^{k} E (i)$
199	198 197	eqeltrd	$⊢ (φ \land k \in Z) \to G (k) \in S$
200	134 2 3 199 135	caragensplit	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) +_{𝑒} O (A ∖ G (k)) = O (A)$
201	191 200	eqtrd	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + O (A ∖ G (k)) = O (A)$
202	201	oveq1d	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + O (A ∖ G (k)) + Y = O (A) + Y$
203	188 202	eqtrd	$⊢ (φ \land k \in Z) \to O (A \cap G (k)) + Y + O (A ∖ G (k)) = O (A) + Y$
204	203	3adant3	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap G (k)) + Y + O (A ∖ G (k)) = O (A) + Y$
205	183 204	breqtrd	$⊢ (φ \land k \in Z \land O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y) \to O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y$
206	205	3exp	$⊢ φ \to (k \in Z \to (O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y \to O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y))$
207	206	rexlimdv	$⊢ φ \to (\exists k \in Z O (A \cap ⋃_{n \in Z} E (n)) < O (A \cap G (k)) + Y \to O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y)$
208	145 207	mpd	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) + O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y$
209	18 208	eqbrtrd	$⊢ φ \to O (A \cap ⋃_{n \in Z} E (n)) +_{𝑒} O (A ∖ ⋃_{n \in Z} E (n)) \leq O (A) + Y$

Metamath Proof Explorer

Theorem carageniuncllem2

Proof