hoidmvlelem3

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvlelem3.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvlelem3.x	$⊢ φ \to X \in Fin$
	hoidmvlelem3.y	$⊢ φ \to Y \subseteq X$
	hoidmvlelem3.z	$⊢ φ \to Z \in (X ∖ Y)$
	hoidmvlelem3.w	$⊢ W = Y \cup \{Z\}$
	hoidmvlelem3.a	$⊢ φ \to A : W ⟶ ℝ$
	hoidmvlelem3.b	$⊢ φ \to B : W ⟶ ℝ$
	hoidmvlelem3.lt	$⊢ (φ \land k \in W) \to A (k) < B (k)$
	hoidmvlelem3.f	$⊢ F = (y \in Y ⟼ 0)$
	hoidmvlelem3.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
	hoidmvlelem3.j	$⊢ J = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F))$
	hoidmvlelem3.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
	hoidmvlelem3.k	$⊢ K = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F))$
	hoidmvlelem3.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
	hoidmvlelem3.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
	hoidmvlelem3.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
	hoidmvlelem3.e	$⊢ φ \to E \in ℝ^{+}$
	hoidmvlelem3.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
	hoidmvlelem3.s	$⊢ φ \to S \in U$
	hoidmvlelem3.sb	$⊢ φ \to S < B (Z)$
	hoidmvlelem3.p	$⊢ P = (j \in ℕ ⟼ J (j) L (Y) K (j))$
	hoidmvlelem3.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
	hoidmvlelem3.i2	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
	hoidmvlelem3.o	$⊢ O = (x \in \underset{k \in Y}{⨉} [A (k), B (k)) ⟼ (k \in W ⟼ if (k \in Y, x (k), S)))$
Assertion	hoidmvlelem3	$⊢ φ \to \exists u \in U S < u$

Proof

Step	Hyp	Ref	Expression
1		hoidmvlelem3.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
2		hoidmvlelem3.x	$⊢ φ \to X \in Fin$
3		hoidmvlelem3.y	$⊢ φ \to Y \subseteq X$
4		hoidmvlelem3.z	$⊢ φ \to Z \in (X ∖ Y)$
5		hoidmvlelem3.w	$⊢ W = Y \cup \{Z\}$
6		hoidmvlelem3.a	$⊢ φ \to A : W ⟶ ℝ$
7		hoidmvlelem3.b	$⊢ φ \to B : W ⟶ ℝ$
8		hoidmvlelem3.lt	$⊢ (φ \land k \in W) \to A (k) < B (k)$
9		hoidmvlelem3.f	$⊢ F = (y \in Y ⟼ 0)$
10		hoidmvlelem3.c	$⊢ φ \to C : ℕ ⟶ ℝ^{W}$
11		hoidmvlelem3.j	$⊢ J = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F))$
12		hoidmvlelem3.d	$⊢ φ \to D : ℕ ⟶ ℝ^{W}$
13		hoidmvlelem3.k	$⊢ K = (j \in ℕ ⟼ if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F))$
14		hoidmvlelem3.r	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (W) D (j))) \in ℝ$
15		hoidmvlelem3.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
16		hoidmvlelem3.g	$⊢ G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
17		hoidmvlelem3.e	$⊢ φ \to E \in ℝ^{+}$
18		hoidmvlelem3.u	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\}$
19		hoidmvlelem3.s	$⊢ φ \to S \in U$
20		hoidmvlelem3.sb	$⊢ φ \to S < B (Z)$
21		hoidmvlelem3.p	$⊢ P = (j \in ℕ ⟼ J (j) L (Y) K (j))$
22		hoidmvlelem3.i	$⊢ φ \to \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
23		hoidmvlelem3.i2	$⊢ φ \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
24		hoidmvlelem3.o	$⊢ O = (x \in \underset{k \in Y}{⨉} [A (k), B (k)) ⟼ (k \in W ⟼ if (k \in Y, x (k), S)))$
25		1nn	$⊢ 1 \in ℕ$
26	25	a1i	$⊢ (φ \land Y = \emptyset) \to 1 \in ℕ$
27		0le0	$⊢ 0 \leq 0$
28	27	a1i	$⊢ (φ \land Y = \emptyset) \to 0 \leq 0$
29	16	a1i	$⊢ (φ \land Y = \emptyset) \to G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
30		fveq2	$⊢ Y = \emptyset \to L (Y) = L (\emptyset)$
31		reseq2	$⊢ Y = \emptyset \to {A ↾}_{Y} = {A ↾}_{\emptyset}$
32		res0	$⊢ {A ↾}_{\emptyset} = \emptyset$
33	32	a1i	$⊢ Y = \emptyset \to {A ↾}_{\emptyset} = \emptyset$
34	31 33	eqtrd	$⊢ Y = \emptyset \to {A ↾}_{Y} = \emptyset$
35		reseq2	$⊢ Y = \emptyset \to {B ↾}_{Y} = {B ↾}_{\emptyset}$
36		res0	$⊢ {B ↾}_{\emptyset} = \emptyset$
37	36	a1i	$⊢ Y = \emptyset \to {B ↾}_{\emptyset} = \emptyset$
38	35 37	eqtrd	$⊢ Y = \emptyset \to {B ↾}_{Y} = \emptyset$
39	30 34 38	oveq123d	$⊢ Y = \emptyset \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) = \emptyset L (\emptyset) \emptyset$
40	39	adantl	$⊢ (φ \land Y = \emptyset) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) = \emptyset L (\emptyset) \emptyset$
41		f0	$⊢ \emptyset : \emptyset ⟶ ℝ$
42	41	a1i	$⊢ (φ \land Y = \emptyset) \to \emptyset : \emptyset ⟶ ℝ$
43	1 42 42	hoidmv0val	$⊢ (φ \land Y = \emptyset) \to \emptyset L (\emptyset) \emptyset = 0$
44	29 40 43	3eqtrd	$⊢ (φ \land Y = \emptyset) \to G = 0$
45		nfcvd	$⊢ φ \to \underline{Ⅎ} j P (1)$
46		nfv	$⊢ Ⅎ j φ$
47		simpr	$⊢ (φ \land j = 1) \to j = 1$
48	47	fveq2d	$⊢ (φ \land j = 1) \to P (j) = P (1)$
49		1red	$⊢ φ \to 1 \in ℝ$
50		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
51		id	$⊢ φ \to φ$
52	25	a1i	$⊢ φ \to 1 \in ℕ$
53	25	elexi	$⊢ 1 \in V$
54		eleq1	$⊢ j = 1 \to (j \in ℕ \leftrightarrow 1 \in ℕ)$
55	54	anbi2d	$⊢ j = 1 \to ((φ \land j \in ℕ) \leftrightarrow (φ \land 1 \in ℕ))$
56		fveq2	$⊢ j = 1 \to P (j) = P (1)$
57	56	eleq1d	$⊢ j = 1 \to (P (j) \in [0, +∞) \leftrightarrow P (1) \in [0, +∞))$
58	55 57	imbi12d	$⊢ j = 1 \to (((φ \land j \in ℕ) \to P (j) \in [0, +∞)) \leftrightarrow ((φ \land 1 \in ℕ) \to P (1) \in [0, +∞)))$
59		id	$⊢ j \in ℕ \to j \in ℕ$
60		ovexd	$⊢ j \in ℕ \to J (j) L (Y) K (j) \in V$
61	21	fvmpt2	$⊢ (j \in ℕ \land J (j) L (Y) K (j) \in V) \to P (j) = J (j) L (Y) K (j)$
62	59 60 61	syl2anc	$⊢ j \in ℕ \to P (j) = J (j) L (Y) K (j)$
63	62	adantl	$⊢ (φ \land j \in ℕ) \to P (j) = J (j) L (Y) K (j)$
64	5	a1i	$⊢ φ \to W = Y \cup \{Z\}$
65	4	eldifad	$⊢ φ \to Z \in X$
66		snssi	$⊢ Z \in X \to \{Z\} \subseteq X$
67	65 66	syl	$⊢ φ \to \{Z\} \subseteq X$
68	3 67	unssd	$⊢ φ \to Y \cup \{Z\} \subseteq X$
69	64 68	eqsstrd	$⊢ φ \to W \subseteq X$
70	2 69	ssfid	$⊢ φ \to W \in Fin$
71		ssun1	$⊢ Y \subseteq Y \cup \{Z\}$
72	5	eqcomi	$⊢ Y \cup \{Z\} = W$
73	71 72	sseqtri	$⊢ Y \subseteq W$
74	73	a1i	$⊢ φ \to Y \subseteq W$
75	70 74	ssfid	$⊢ φ \to Y \in Fin$
76	75	adantr	$⊢ (φ \land j \in ℕ) \to Y \in Fin$
77		iftrue	$⊢ S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
78	77	adantl	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
79	10	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{W})$
80		elmapi	$⊢ C (j) \in (ℝ^{W}) \to C (j) : W ⟶ ℝ$
81	79 80	syl	$⊢ (φ \land j \in ℕ) \to C (j) : W ⟶ ℝ$
82	71 5	sseqtrri	$⊢ Y \subseteq W$
83	82	a1i	$⊢ (φ \land j \in ℕ) \to Y \subseteq W$
84	81 83	fssresd	$⊢ (φ \land j \in ℕ) \to ({C (j) ↾}_{Y}) : Y ⟶ ℝ$
85		reex	$⊢ ℝ \in V$
86	85	a1i	$⊢ (φ \land j \in ℕ) \to ℝ \in V$
87	70 74	ssexd	$⊢ φ \to Y \in V$
88	87	adantr	$⊢ (φ \land j \in ℕ) \to Y \in V$
89	86 88	elmapd	$⊢ (φ \land j \in ℕ) \to ({C (j) ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({C (j) ↾}_{Y}) : Y ⟶ ℝ)$
90	84 89	mpbird	$⊢ (φ \land j \in ℕ) \to {C (j) ↾}_{Y} \in (ℝ^{Y})$
91	90	adantr	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to {C (j) ↾}_{Y} \in (ℝ^{Y})$
92	78 91	eqeltrd	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in (ℝ^{Y})$
93		iffalse	$⊢ \neg S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = F$
94	93	adantl	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = F$
95		0red	$⊢ (φ \land y \in Y) \to 0 \in ℝ$
96	95 9	fmptd	$⊢ φ \to F : Y ⟶ ℝ$
97	85	a1i	$⊢ φ \to ℝ \in V$
98	97 75	elmapd	$⊢ φ \to (F \in (ℝ^{Y}) \leftrightarrow F : Y ⟶ ℝ)$
99	96 98	mpbird	$⊢ φ \to F \in (ℝ^{Y})$
100	99	ad2antrr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to F \in (ℝ^{Y})$
101	94 100	eqeltrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in (ℝ^{Y})$
102	92 101	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in (ℝ^{Y})$
103	102 11	fmptd	$⊢ φ \to J : ℕ ⟶ ℝ^{Y}$
104	103	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to J (j) \in (ℝ^{Y})$
105		elmapi	$⊢ J (j) \in (ℝ^{Y}) \to J (j) : Y ⟶ ℝ$
106	104 105	syl	$⊢ (φ \land j \in ℕ) \to J (j) : Y ⟶ ℝ$
107		iftrue	$⊢ S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
108	107	adantl	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
109	12	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{W})$
110		elmapi	$⊢ D (j) \in (ℝ^{W}) \to D (j) : W ⟶ ℝ$
111	109 110	syl	$⊢ (φ \land j \in ℕ) \to D (j) : W ⟶ ℝ$
112	111 83	fssresd	$⊢ (φ \land j \in ℕ) \to ({D (j) ↾}_{Y}) : Y ⟶ ℝ$
113	86 88	elmapd	$⊢ (φ \land j \in ℕ) \to ({D (j) ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({D (j) ↾}_{Y}) : Y ⟶ ℝ)$
114	112 113	mpbird	$⊢ (φ \land j \in ℕ) \to {D (j) ↾}_{Y} \in (ℝ^{Y})$
115	114	adantr	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to {D (j) ↾}_{Y} \in (ℝ^{Y})$
116	108 115	eqeltrd	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in (ℝ^{Y})$
117		iffalse	$⊢ \neg S \in [C (j) (Z), D (j) (Z)) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = F$
118	117	adantl	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = F$
119	118 100	eqeltrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in (ℝ^{Y})$
120	116 119	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in (ℝ^{Y})$
121	120 13	fmptd	$⊢ φ \to K : ℕ ⟶ ℝ^{Y}$
122	121	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to K (j) \in (ℝ^{Y})$
123		elmapi	$⊢ K (j) \in (ℝ^{Y}) \to K (j) : Y ⟶ ℝ$
124	122 123	syl	$⊢ (φ \land j \in ℕ) \to K (j) : Y ⟶ ℝ$
125	1 76 106 124	hoidmvcl	$⊢ (φ \land j \in ℕ) \to J (j) L (Y) K (j) \in [0, +∞)$
126	63 125	eqeltrd	$⊢ (φ \land j \in ℕ) \to P (j) \in [0, +∞)$
127	53 58 126	vtocl	$⊢ (φ \land 1 \in ℕ) \to P (1) \in [0, +∞)$
128	51 52 127	syl2anc	$⊢ φ \to P (1) \in [0, +∞)$
129	50 128	sselid	$⊢ φ \to P (1) \in ℝ$
130	129	recnd	$⊢ φ \to P (1) \in ℂ$
131	45 46 48 49 130	sumsnd	$⊢ φ \to \sum_{j \in \{1\}} P (j) = P (1)$
132	131	adantr	$⊢ (φ \land Y = \emptyset) \to \sum_{j \in \{1\}} P (j) = P (1)$
133		fveq2	$⊢ j = 1 \to J (j) = J (1)$
134		fveq2	$⊢ j = 1 \to K (j) = K (1)$
135	133 134	oveq12d	$⊢ j = 1 \to J (j) L (Y) K (j) = J (1) L (Y) K (1)$
136		ovex	$⊢ J (1) L (Y) K (1) \in V$
137	135 21 136	fvmpt	$⊢ 1 \in ℕ \to P (1) = J (1) L (Y) K (1)$
138	25 137	ax-mp	$⊢ P (1) = J (1) L (Y) K (1)$
139	138	a1i	$⊢ (φ \land Y = \emptyset) \to P (1) = J (1) L (Y) K (1)$
140	30	oveqd	$⊢ Y = \emptyset \to J (1) L (Y) K (1) = J (1) L (\emptyset) K (1)$
141	140	adantl	$⊢ (φ \land Y = \emptyset) \to J (1) L (Y) K (1) = J (1) L (\emptyset) K (1)$
142	133	feq1d	$⊢ j = 1 \to (J (j) : Y ⟶ ℝ \leftrightarrow J (1) : Y ⟶ ℝ)$
143	55 142	imbi12d	$⊢ j = 1 \to (((φ \land j \in ℕ) \to J (j) : Y ⟶ ℝ) \leftrightarrow ((φ \land 1 \in ℕ) \to J (1) : Y ⟶ ℝ))$
144	84	adantr	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to ({C (j) ↾}_{Y}) : Y ⟶ ℝ$
145	78	feq1d	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow ({C (j) ↾}_{Y}) : Y ⟶ ℝ)$
146	144 145	mpbird	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
147	96	ad2antrr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to F : Y ⟶ ℝ$
148	94	feq1d	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to (if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ \leftrightarrow F : Y ⟶ ℝ)$
149	147 148	mpbird	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
150	146 149	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ$
151		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
152		fvex	$⊢ C (j) \in V$
153	152	resex	$⊢ {C (j) ↾}_{Y} \in V$
154	78 153	eqeltrdi	$⊢ ((φ \land j \in ℕ) \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V$
155	99	elexd	$⊢ φ \to F \in V$
156	155	adantr	$⊢ (φ \land j \in ℕ) \to F \in V$
157	156	adantr	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to F \in V$
158	94 157	eqeltrd	$⊢ ((φ \land j \in ℕ) \land \neg S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V$
159	154 158	pm2.61dan	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V$
160	11	fvmpt2	$⊢ (j \in ℕ \land if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \in V) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
161	151 159 160	syl2anc	$⊢ (φ \land j \in ℕ) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
162	161	feq1d	$⊢ (φ \land j \in ℕ) \to (J (j) : Y ⟶ ℝ \leftrightarrow if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) : Y ⟶ ℝ)$
163	150 162	mpbird	$⊢ (φ \land j \in ℕ) \to J (j) : Y ⟶ ℝ$
164	53 143 163	vtocl	$⊢ (φ \land 1 \in ℕ) \to J (1) : Y ⟶ ℝ$
165	51 52 164	syl2anc	$⊢ φ \to J (1) : Y ⟶ ℝ$
166	165	adantr	$⊢ (φ \land Y = \emptyset) \to J (1) : Y ⟶ ℝ$
167		id	$⊢ Y = \emptyset \to Y = \emptyset$
168	167	eqcomd	$⊢ Y = \emptyset \to \emptyset = Y$
169	168	feq2d	$⊢ Y = \emptyset \to (J (1) : \emptyset ⟶ ℝ \leftrightarrow J (1) : Y ⟶ ℝ)$
170	169	adantl	$⊢ (φ \land Y = \emptyset) \to (J (1) : \emptyset ⟶ ℝ \leftrightarrow J (1) : Y ⟶ ℝ)$
171	166 170	mpbird	$⊢ (φ \land Y = \emptyset) \to J (1) : \emptyset ⟶ ℝ$
172	134	feq1d	$⊢ j = 1 \to (K (j) : Y ⟶ ℝ \leftrightarrow K (1) : Y ⟶ ℝ)$
173	55 172	imbi12d	$⊢ j = 1 \to (((φ \land j \in ℕ) \to K (j) : Y ⟶ ℝ) \leftrightarrow ((φ \land 1 \in ℕ) \to K (1) : Y ⟶ ℝ))$
174	53 173 124	vtocl	$⊢ (φ \land 1 \in ℕ) \to K (1) : Y ⟶ ℝ$
175	51 52 174	syl2anc	$⊢ φ \to K (1) : Y ⟶ ℝ$
176	175	adantr	$⊢ (φ \land Y = \emptyset) \to K (1) : Y ⟶ ℝ$
177	168	feq2d	$⊢ Y = \emptyset \to (K (1) : \emptyset ⟶ ℝ \leftrightarrow K (1) : Y ⟶ ℝ)$
178	177	adantl	$⊢ (φ \land Y = \emptyset) \to (K (1) : \emptyset ⟶ ℝ \leftrightarrow K (1) : Y ⟶ ℝ)$
179	176 178	mpbird	$⊢ (φ \land Y = \emptyset) \to K (1) : \emptyset ⟶ ℝ$
180	1 171 179	hoidmv0val	$⊢ (φ \land Y = \emptyset) \to J (1) L (\emptyset) K (1) = 0$
181	141 180	eqtrd	$⊢ (φ \land Y = \emptyset) \to J (1) L (Y) K (1) = 0$
182	132 139 181	3eqtrd	$⊢ (φ \land Y = \emptyset) \to \sum_{j \in \{1\}} P (j) = 0$
183	182	oveq2d	$⊢ (φ \land Y = \emptyset) \to (1 + E) \sum_{j \in \{1\}} P (j) = (1 + E) \cdot 0$
184	17	rpred	$⊢ φ \to E \in ℝ$
185	49 184	readdcld	$⊢ φ \to 1 + E \in ℝ$
186	185	recnd	$⊢ φ \to 1 + E \in ℂ$
187	186	mul01d	$⊢ φ \to (1 + E) \cdot 0 = 0$
188	187	adantr	$⊢ (φ \land Y = \emptyset) \to (1 + E) \cdot 0 = 0$
189		eqidd	$⊢ (φ \land Y = \emptyset) \to 0 = 0$
190	183 188 189	3eqtrd	$⊢ (φ \land Y = \emptyset) \to (1 + E) \sum_{j \in \{1\}} P (j) = 0$
191	44 190	breq12d	$⊢ (φ \land Y = \emptyset) \to (G \leq (1 + E) \sum_{j \in \{1\}} P (j) \leftrightarrow 0 \leq 0)$
192	28 191	mpbird	$⊢ (φ \land Y = \emptyset) \to G \leq (1 + E) \sum_{j \in \{1\}} P (j)$
193		oveq2	$⊢ m = 1 \to (1 \dots m) = (1 \dots 1)$
194	25	nnzi	$⊢ 1 \in ℤ$
195		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
196	194 195	ax-mp	$⊢ (1 \dots 1) = \{1\}$
197	196	a1i	$⊢ m = 1 \to (1 \dots 1) = \{1\}$
198	193 197	eqtrd	$⊢ m = 1 \to (1 \dots m) = \{1\}$
199	198	sumeq1d	$⊢ m = 1 \to \sum_{j = 1}^{m} P (j) = \sum_{j \in \{1\}} P (j)$
200	199	oveq2d	$⊢ m = 1 \to (1 + E) \sum_{j = 1}^{m} P (j) = (1 + E) \sum_{j \in \{1\}} P (j)$
201	200	breq2d	$⊢ m = 1 \to (G \leq (1 + E) \sum_{j = 1}^{m} P (j) \leftrightarrow G \leq (1 + E) \sum_{j \in \{1\}} P (j))$
202	201	rspcev	$⊢ (1 \in ℕ \land G \leq (1 + E) \sum_{j \in \{1\}} P (j)) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
203	26 192 202	syl2anc	$⊢ (φ \land Y = \emptyset) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
204		simpl	$⊢ (φ \land \neg Y = \emptyset) \to φ$
205		neqne	$⊢ \neg Y = \emptyset \to Y \neq \emptyset$
206	205	adantl	$⊢ (φ \land \neg Y = \emptyset) \to Y \neq \emptyset$
207		nfv	$⊢ Ⅎ j (φ \land Y \neq \emptyset)$
208	194	a1i	$⊢ (φ \land Y \neq \emptyset) \to 1 \in ℤ$
209		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
210	126	adantlr	$⊢ ((φ \land Y \neq \emptyset) \land j \in ℕ) \to P (j) \in [0, +∞)$
211	82	a1i	$⊢ φ \to Y \subseteq W$
212	6 211	fssresd	$⊢ φ \to ({A ↾}_{Y}) : Y ⟶ ℝ$
213	7 211	fssresd	$⊢ φ \to ({B ↾}_{Y}) : Y ⟶ ℝ$
214	1 75 212 213	hoidmvcl	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \in [0, +∞)$
215	50 214	sselid	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \in ℝ$
216	16 215	eqeltrid	$⊢ φ \to G \in ℝ$
217		0red	$⊢ φ \to 0 \in ℝ$
218		1rp	$⊢ 1 \in ℝ^{+}$
219	218	a1i	$⊢ φ \to 1 \in ℝ^{+}$
220	219 17	jca	$⊢ φ \to (1 \in ℝ^{+} \land E \in ℝ^{+})$
221		rpaddcl	$⊢ (1 \in ℝ^{+} \land E \in ℝ^{+}) \to 1 + E \in ℝ^{+}$
222	220 221	syl	$⊢ φ \to 1 + E \in ℝ^{+}$
223		rpgt0	$⊢ 1 + E \in ℝ^{+} \to 0 < 1 + E$
224	222 223	syl	$⊢ φ \to 0 < 1 + E$
225	217 224	gtned	$⊢ φ \to 1 + E \neq 0$
226	216 185 225	redivcld	$⊢ φ \to \frac{G}{1 + E} \in ℝ$
227	226	adantr	$⊢ (φ \land Y \neq \emptyset) \to \frac{G}{1 + E} \in ℝ$
228	226	ltpnfd	$⊢ φ \to \frac{G}{1 + E} < +∞$
229	228	adantr	$⊢ (φ \land sum^((j \in ℕ ⟼ P (j))) = +∞) \to \frac{G}{1 + E} < +∞$
230		id	$⊢ sum^((j \in ℕ ⟼ P (j))) = +∞ \to sum^((j \in ℕ ⟼ P (j))) = +∞$
231	230	eqcomd	$⊢ sum^((j \in ℕ ⟼ P (j))) = +∞ \to +∞ = sum^((j \in ℕ ⟼ P (j)))$
232	231	adantl	$⊢ (φ \land sum^((j \in ℕ ⟼ P (j))) = +∞) \to +∞ = sum^((j \in ℕ ⟼ P (j)))$
233	229 232	breqtrd	$⊢ (φ \land sum^((j \in ℕ ⟼ P (j))) = +∞) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
234	233	adantlr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) = +∞) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
235		simpl	$⊢ ((φ \land Y \neq \emptyset) \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to (φ \land Y \neq \emptyset)$
236		simpr	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to \neg sum^((j \in ℕ ⟼ P (j))) = +∞$
237		nnex	$⊢ ℕ \in V$
238	237	a1i	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to ℕ \in V$
239		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
240	239 126	sselid	$⊢ (φ \land j \in ℕ) \to P (j) \in [0, +∞]$
241		eqid	$⊢ (j \in ℕ ⟼ P (j)) = (j \in ℕ ⟼ P (j))$
242	240 241	fmptd	$⊢ φ \to (j \in ℕ ⟼ P (j)) : ℕ ⟶ [0, +∞]$
243	242	adantr	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to (j \in ℕ ⟼ P (j)) : ℕ ⟶ [0, +∞]$
244	238 243	sge0repnf	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to (sum^((j \in ℕ ⟼ P (j))) \in ℝ \leftrightarrow \neg sum^((j \in ℕ ⟼ P (j))) = +∞)$
245	236 244	mpbird	$⊢ (φ \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to sum^((j \in ℕ ⟼ P (j))) \in ℝ$
246	245	adantlr	$⊢ ((φ \land Y \neq \emptyset) \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to sum^((j \in ℕ ⟼ P (j))) \in ℝ$
247	227	adantr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to \frac{G}{1 + E} \in ℝ$
248	216	adantr	$⊢ (φ \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to G \in ℝ$
249	248	adantlr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to G \in ℝ$
250		simpr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to sum^((j \in ℕ ⟼ P (j))) \in ℝ$
251	49 17	ltaddrpd	$⊢ φ \to 1 < 1 + E$
252	251	adantr	$⊢ (φ \land Y \neq \emptyset) \to 1 < 1 + E$
253	75	adantr	$⊢ (φ \land Y \neq \emptyset) \to Y \in Fin$
254		simpr	$⊢ (φ \land Y \neq \emptyset) \to Y \neq \emptyset$
255	212	adantr	$⊢ (φ \land Y \neq \emptyset) \to ({A ↾}_{Y}) : Y ⟶ ℝ$
256	213	adantr	$⊢ (φ \land Y \neq \emptyset) \to ({B ↾}_{Y}) : Y ⟶ ℝ$
257	1 253 254 255 256	hoidmvn0val	$⊢ (φ \land Y \neq \emptyset) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) = \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)))$
258	16	a1i	$⊢ (φ \land Y \neq \emptyset) \to G = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
259		fvres	$⊢ k \in Y \to ({A ↾}_{Y}) (k) = A (k)$
260		fvres	$⊢ k \in Y \to ({B ↾}_{Y}) (k) = B (k)$
261	259 260	oveq12d	$⊢ k \in Y \to [({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)) = [A (k), B (k))$
262	261	fveq2d	$⊢ k \in Y \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = vol ([A (k), B (k)))$
263	262	adantl	$⊢ (φ \land k \in Y) \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = vol ([A (k), B (k)))$
264	6	adantr	$⊢ (φ \land k \in Y) \to A : W ⟶ ℝ$
265		elun1	$⊢ k \in Y \to k \in (Y \cup \{Z\})$
266	265 5	eleqtrrdi	$⊢ k \in Y \to k \in W$
267	266	adantl	$⊢ (φ \land k \in Y) \to k \in W$
268	264 267	ffvelcdmd	$⊢ (φ \land k \in Y) \to A (k) \in ℝ$
269	7	adantr	$⊢ (φ \land k \in Y) \to B : W ⟶ ℝ$
270	269 267	ffvelcdmd	$⊢ (φ \land k \in Y) \to B (k) \in ℝ$
271		volico	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
272	268 270 271	syl2anc	$⊢ (φ \land k \in Y) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
273	267 8	syldan	$⊢ (φ \land k \in Y) \to A (k) < B (k)$
274	273	iftrued	$⊢ (φ \land k \in Y) \to if (A (k) < B (k), B (k) - A (k), 0) = B (k) - A (k)$
275	263 272 274	3eqtrd	$⊢ (φ \land k \in Y) \to vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = B (k) - A (k)$
276	275	prodeq2dv	$⊢ φ \to \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k))) = \prod_{k \in Y} (B (k) - A (k))$
277	276	eqcomd	$⊢ φ \to \prod_{k \in Y} (B (k) - A (k)) = \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)))$
278	277	adantr	$⊢ (φ \land Y \neq \emptyset) \to \prod_{k \in Y} (B (k) - A (k)) = \prod_{k \in Y} vol ([({A ↾}_{Y}) (k), ({B ↾}_{Y}) (k)))$
279	257 258 278	3eqtr4d	$⊢ (φ \land Y \neq \emptyset) \to G = \prod_{k \in Y} (B (k) - A (k))$
280		difrp	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to (A (k) < B (k) \leftrightarrow B (k) - A (k) \in ℝ^{+})$
281	268 270 280	syl2anc	$⊢ (φ \land k \in Y) \to (A (k) < B (k) \leftrightarrow B (k) - A (k) \in ℝ^{+})$
282	273 281	mpbid	$⊢ (φ \land k \in Y) \to B (k) - A (k) \in ℝ^{+}$
283	75 282	fprodrpcl	$⊢ φ \to \prod_{k \in Y} (B (k) - A (k)) \in ℝ^{+}$
284	283	adantr	$⊢ (φ \land Y \neq \emptyset) \to \prod_{k \in Y} (B (k) - A (k)) \in ℝ^{+}$
285	279 284	eqeltrd	$⊢ (φ \land Y \neq \emptyset) \to G \in ℝ^{+}$
286	222	adantr	$⊢ (φ \land Y \neq \emptyset) \to 1 + E \in ℝ^{+}$
287	285 286	ltdivgt1	$⊢ (φ \land Y \neq \emptyset) \to (1 < 1 + E \leftrightarrow \frac{G}{1 + E} < G)$
288	252 287	mpbid	$⊢ (φ \land Y \neq \emptyset) \to \frac{G}{1 + E} < G$
289	288	adantr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to \frac{G}{1 + E} < G$
290	23	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to \underset{k \in W}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
291		fvexd	$⊢ φ \to x (k) \in V$
292	19	elexd	$⊢ φ \to S \in V$
293	291 292	ifcld	$⊢ φ \to if (k \in Y, x (k), S) \in V$
294	293	ralrimivw	$⊢ φ \to \forall k \in W if (k \in Y, x (k), S) \in V$
295	294	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to \forall k \in W if (k \in Y, x (k), S) \in V$
296		eqid	$⊢ (k \in W ⟼ if (k \in Y, x (k), S)) = (k \in W ⟼ if (k \in Y, x (k), S))$
297	296	fnmpt	$⊢ \forall k \in W if (k \in Y, x (k), S) \in V \to (k \in W ⟼ if (k \in Y, x (k), S)) Fn W$
298	295 297	syl	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (k \in W ⟼ if (k \in Y, x (k), S)) Fn W$
299		simpr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to x \in \underset{k \in Y}{⨉} [A (k), B (k))$
300		mptexg	$⊢ W \in Fin \to (k \in W ⟼ if (k \in Y, x (k), S)) \in V$
301	70 300	syl	$⊢ φ \to (k \in W ⟼ if (k \in Y, x (k), S)) \in V$
302	301	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (k \in W ⟼ if (k \in Y, x (k), S)) \in V$
303	24	fvmpt2	$⊢ (x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land (k \in W ⟼ if (k \in Y, x (k), S)) \in V) \to O (x) = (k \in W ⟼ if (k \in Y, x (k), S))$
304	299 302 303	syl2anc	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) = (k \in W ⟼ if (k \in Y, x (k), S))$
305	304	fneq1d	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (O (x) Fn W \leftrightarrow (k \in W ⟼ if (k \in Y, x (k), S)) Fn W)$
306	298 305	mpbird	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) Fn W$
307		nfv	$⊢ Ⅎ k φ$
308		nfcv	$⊢ \underline{Ⅎ} k x$
309		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in Y}{⨉} [A (k), B (k))$
310	308 309	nfel	$⊢ Ⅎ k x \in \underset{k \in Y}{⨉} [A (k), B (k))$
311	307 310	nfan	$⊢ Ⅎ k (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)))$
312	304	fveq1d	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) (k) = (k \in W ⟼ if (k \in Y, x (k), S)) (k)$
313	312	adantr	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \to O (x) (k) = (k \in W ⟼ if (k \in Y, x (k), S)) (k)$
314		simpr	$⊢ (φ \land k \in W) \to k \in W$
315	293	adantr	$⊢ (φ \land k \in W) \to if (k \in Y, x (k), S) \in V$
316	296	fvmpt2	$⊢ (k \in W \land if (k \in Y, x (k), S) \in V) \to (k \in W ⟼ if (k \in Y, x (k), S)) (k) = if (k \in Y, x (k), S)$
317	314 315 316	syl2anc	$⊢ (φ \land k \in W) \to (k \in W ⟼ if (k \in Y, x (k), S)) (k) = if (k \in Y, x (k), S)$
318	317	adantlr	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \to (k \in W ⟼ if (k \in Y, x (k), S)) (k) = if (k \in Y, x (k), S)$
319	313 318	eqtrd	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \to O (x) (k) = if (k \in Y, x (k), S)$
320		iftrue	$⊢ k \in Y \to if (k \in Y, x (k), S) = x (k)$
321	320	adantl	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \land k \in Y) \to if (k \in Y, x (k), S) = x (k)$
322		vex	$⊢ x \in V$
323	322	elixp	$⊢ x \in \underset{k \in Y}{⨉} [A (k), B (k)) \leftrightarrow (x Fn Y \land \forall k \in Y x (k) \in [A (k), B (k)))$
324	323	simprbi	$⊢ x \in \underset{k \in Y}{⨉} [A (k), B (k)) \to \forall k \in Y x (k) \in [A (k), B (k))$
325	324	adantr	$⊢ (x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to \forall k \in Y x (k) \in [A (k), B (k))$
326		simpr	$⊢ (x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to k \in Y$
327		rspa	$⊢ (\forall k \in Y x (k) \in [A (k), B (k)) \land k \in Y) \to x (k) \in [A (k), B (k))$
328	325 326 327	syl2anc	$⊢ (x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to x (k) \in [A (k), B (k))$
329	328	ad4ant24	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \land k \in Y) \to x (k) \in [A (k), B (k))$
330	321 329	eqeltrd	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \land k \in Y) \to if (k \in Y, x (k), S) \in [A (k), B (k))$
331		snidg	$⊢ Z \in (X ∖ Y) \to Z \in \{Z\}$
332	4 331	syl	$⊢ φ \to Z \in \{Z\}$
333		elun2	$⊢ Z \in \{Z\} \to Z \in (Y \cup \{Z\})$
334	332 333	syl	$⊢ φ \to Z \in (Y \cup \{Z\})$
335	72	a1i	$⊢ φ \to Y \cup \{Z\} = W$
336	334 335	eleqtrd	$⊢ φ \to Z \in W$
337	6 336	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
338	337	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
339	7 336	ffvelcdmd	$⊢ φ \to B (Z) \in ℝ$
340	339	rexrd	$⊢ φ \to B (Z) \in ℝ^{*}$
341		iccssxr	$⊢ [A (Z), B (Z)] \subseteq ℝ^{*}$
342		ssrab2	$⊢ \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} \subseteq [A (Z), B (Z)]$
343	18 342	eqsstri	$⊢ U \subseteq [A (Z), B (Z)]$
344	343 19	sselid	$⊢ φ \to S \in [A (Z), B (Z)]$
345	341 344	sselid	$⊢ φ \to S \in ℝ^{*}$
346		iccgelb	$⊢ (A (Z) \in ℝ^{} \land B (Z) \in ℝ^{} \land S \in [A (Z), B (Z)]) \to A (Z) \leq S$
347	338 340 344 346	syl3anc	$⊢ φ \to A (Z) \leq S$
348	338 340 345 347 20	elicod	$⊢ φ \to S \in [A (Z), B (Z))$
349	348	ad2antrr	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to S \in [A (Z), B (Z))$
350		iffalse	$⊢ \neg k \in Y \to if (k \in Y, x (k), S) = S$
351	350	adantl	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to if (k \in Y, x (k), S) = S$
352	5	eleq2i	$⊢ k \in W \leftrightarrow k \in (Y \cup \{Z\})$
353	352	biimpi	$⊢ k \in W \to k \in (Y \cup \{Z\})$
354	353	adantr	$⊢ (k \in W \land \neg k \in Y) \to k \in (Y \cup \{Z\})$
355		simpr	$⊢ (k \in W \land \neg k \in Y) \to \neg k \in Y$
356		elunnel1	$⊢ (k \in (Y \cup \{Z\}) \land \neg k \in Y) \to k \in \{Z\}$
357	354 355 356	syl2anc	$⊢ (k \in W \land \neg k \in Y) \to k \in \{Z\}$
358		elsni	$⊢ k \in \{Z\} \to k = Z$
359	357 358	syl	$⊢ (k \in W \land \neg k \in Y) \to k = Z$
360		fveq2	$⊢ k = Z \to A (k) = A (Z)$
361		fveq2	$⊢ k = Z \to B (k) = B (Z)$
362	360 361	oveq12d	$⊢ k = Z \to [A (k), B (k)) = [A (Z), B (Z))$
363	359 362	syl	$⊢ (k \in W \land \neg k \in Y) \to [A (k), B (k)) = [A (Z), B (Z))$
364	363	adantll	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to [A (k), B (k)) = [A (Z), B (Z))$
365	351 364	eleq12d	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to (if (k \in Y, x (k), S) \in [A (k), B (k)) \leftrightarrow S \in [A (Z), B (Z)))$
366	349 365	mpbird	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to if (k \in Y, x (k), S) \in [A (k), B (k))$
367	366	adantllr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \land \neg k \in Y) \to if (k \in Y, x (k), S) \in [A (k), B (k))$
368	330 367	pm2.61dan	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \to if (k \in Y, x (k), S) \in [A (k), B (k))$
369	319 368	eqeltrd	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land k \in W) \to O (x) (k) \in [A (k), B (k))$
370	369	ex	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (k \in W \to O (x) (k) \in [A (k), B (k)))$
371	311 370	ralrimi	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to \forall k \in W O (x) (k) \in [A (k), B (k))$
372	306 371	jca	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (O (x) Fn W \land \forall k \in W O (x) (k) \in [A (k), B (k)))$
373		fvex	$⊢ O (x) \in V$
374	373	elixp	$⊢ O (x) \in \underset{k \in W}{⨉} [A (k), B (k)) \leftrightarrow (O (x) Fn W \land \forall k \in W O (x) (k) \in [A (k), B (k)))$
375	372 374	sylibr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) \in \underset{k \in W}{⨉} [A (k), B (k))$
376	290 375	sseldd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) \in ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
377		eliun	$⊢ O (x) \in ⋃_{j \in ℕ} \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \leftrightarrow \exists j \in ℕ O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
378	376 377	sylib	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to \exists j \in ℕ O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
379		ixpfn	$⊢ x \in \underset{k \in Y}{⨉} [A (k), B (k)) \to x Fn Y$
380	379	adantl	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to x Fn Y$
381	380	ad2antrr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to x Fn Y$
382		nfv	$⊢ Ⅎ k j \in ℕ$
383	311 382	nfan	$⊢ Ⅎ k ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ)$
384		nfcv	$⊢ \underline{Ⅎ} k O (x)$
385		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
386	384 385	nfel	$⊢ Ⅎ k O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
387	383 386	nfan	$⊢ Ⅎ k (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)))$
388	312	3adant3	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to O (x) (k) = (k \in W ⟼ if (k \in Y, x (k), S)) (k)$
389	293	adantr	$⊢ (φ \land k \in Y) \to if (k \in Y, x (k), S) \in V$
390	267 389 316	syl2anc	$⊢ (φ \land k \in Y) \to (k \in W ⟼ if (k \in Y, x (k), S)) (k) = if (k \in Y, x (k), S)$
391	390	3adant2	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to (k \in W ⟼ if (k \in Y, x (k), S)) (k) = if (k \in Y, x (k), S)$
392	320	3ad2ant3	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to if (k \in Y, x (k), S) = x (k)$
393	388 391 392	3eqtrrd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to x (k) = O (x) (k)$
394	393	ad5ant125	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to x (k) = O (x) (k)$
395		simpl	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
396	373	elixp	$⊢ O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \leftrightarrow (O (x) Fn W \land \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k)))$
397	395 396	sylib	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to (O (x) Fn W \land \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k)))$
398	397	simprd	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k))$
399	266	adantl	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to k \in W$
400		rspa	$⊢ (\forall k \in W O (x) (k) \in [C (j) (k), D (j) (k)) \land k \in W) \to O (x) (k) \in [C (j) (k), D (j) (k))$
401	398 399 400	syl2anc	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to O (x) (k) \in [C (j) (k), D (j) (k))$
402	401	adantll	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to O (x) (k) \in [C (j) (k), D (j) (k))$
403	394 402	eqeltrd	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to x (k) \in [C (j) (k), D (j) (k))$
404	51	ad3antrrr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to φ$
405	59	ad2antlr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to j \in ℕ$
406	304	fveq1d	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) (Z) = (k \in W ⟼ if (k \in Y, x (k), S)) (Z)$
407		eqidd	$⊢ φ \to (k \in W ⟼ if (k \in Y, x (k), S)) = (k \in W ⟼ if (k \in Y, x (k), S))$
408		eleq1	$⊢ k = Z \to (k \in Y \leftrightarrow Z \in Y)$
409		fveq2	$⊢ k = Z \to x (k) = x (Z)$
410	408 409	ifbieq1d	$⊢ k = Z \to if (k \in Y, x (k), S) = if (Z \in Y, x (Z), S)$
411	410	adantl	$⊢ (φ \land k = Z) \to if (k \in Y, x (k), S) = if (Z \in Y, x (Z), S)$
412		fvexd	$⊢ φ \to x (Z) \in V$
413	412 292	ifcld	$⊢ φ \to if (Z \in Y, x (Z), S) \in V$
414	407 411 336 413	fvmptd	$⊢ φ \to (k \in W ⟼ if (k \in Y, x (k), S)) (Z) = if (Z \in Y, x (Z), S)$
415	414	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (k \in W ⟼ if (k \in Y, x (k), S)) (Z) = if (Z \in Y, x (Z), S)$
416	4	eldifbd	$⊢ φ \to \neg Z \in Y$
417	416	iffalsed	$⊢ φ \to if (Z \in Y, x (Z), S) = S$
418	417	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to if (Z \in Y, x (Z), S) = S$
419	406 415 418	3eqtrrd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to S = O (x) (Z)$
420	419	ad2antrr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to S = O (x) (Z)$
421	404 336	syl	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to Z \in W$
422	396	simprbi	$⊢ O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \to \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k))$
423	422	adantl	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k))$
424		fveq2	$⊢ k = Z \to O (x) (k) = O (x) (Z)$
425		fveq2	$⊢ k = Z \to C (j) (k) = C (j) (Z)$
426		fveq2	$⊢ k = Z \to D (j) (k) = D (j) (Z)$
427	425 426	oveq12d	$⊢ k = Z \to [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z))$
428	424 427	eleq12d	$⊢ k = Z \to (O (x) (k) \in [C (j) (k), D (j) (k)) \leftrightarrow O (x) (Z) \in [C (j) (Z), D (j) (Z)))$
429	428	rspcva	$⊢ (Z \in W \land \forall k \in W O (x) (k) \in [C (j) (k), D (j) (k))) \to O (x) (Z) \in [C (j) (Z), D (j) (Z))$
430	421 423 429	syl2anc	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to O (x) (Z) \in [C (j) (Z), D (j) (Z))$
431	420 430	eqeltrd	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to S \in [C (j) (Z), D (j) (Z))$
432	161	3adant3	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)$
433	77	3ad2ant3	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = {C (j) ↾}_{Y}$
434	432 433	eqtrd	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to J (j) = {C (j) ↾}_{Y}$
435	434	fveq1d	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
436	404 405 431 435	syl3anc	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
437	436	adantr	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
438		fvres	$⊢ k \in Y \to ({C (j) ↾}_{Y}) (k) = C (j) (k)$
439	438	adantl	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to ({C (j) ↾}_{Y}) (k) = C (j) (k)$
440	437 439	eqtrd	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to J (j) (k) = C (j) (k)$
441	120	elexd	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V$
442	13	fvmpt2	$⊢ (j \in ℕ \land if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
443	151 441 442	syl2anc	$⊢ (φ \land j \in ℕ) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
444	443	3adant3	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
445	107	3ad2ant3	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = {D (j) ↾}_{Y}$
446	444 445	eqtrd	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to K (j) = {D (j) ↾}_{Y}$
447	446	fveq1d	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
448	404 405 431 447	syl3anc	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
449	448	adantr	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
450		fvres	$⊢ k \in Y \to ({D (j) ↾}_{Y}) (k) = D (j) (k)$
451	450	adantl	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to ({D (j) ↾}_{Y}) (k) = D (j) (k)$
452	449 451	eqtrd	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to K (j) (k) = D (j) (k)$
453	440 452	oveq12d	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to [J (j) (k), K (j) (k)) = [C (j) (k), D (j) (k))$
454	453	eqcomd	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to [C (j) (k), D (j) (k)) = [J (j) (k), K (j) (k))$
455	403 454	eleqtrd	$⊢ ((((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \land k \in Y) \to x (k) \in [J (j) (k), K (j) (k))$
456	455	ex	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to (k \in Y \to x (k) \in [J (j) (k), K (j) (k)))$
457	387 456	ralrimi	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to \forall k \in Y x (k) \in [J (j) (k), K (j) (k))$
458	381 457	jca	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to (x Fn Y \land \forall k \in Y x (k) \in [J (j) (k), K (j) (k)))$
459	322	elixp	$⊢ x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \leftrightarrow (x Fn Y \land \forall k \in Y x (k) \in [J (j) (k), K (j) (k)))$
460	458 459	sylibr	$⊢ (((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \land O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))) \to x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
461	460	ex	$⊢ ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ) \to (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \to x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)))$
462	461	reximdva	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to (\exists j \in ℕ O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \to \exists j \in ℕ x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)))$
463	378 462	mpd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to \exists j \in ℕ x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
464		eliun	$⊢ x \in ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \leftrightarrow \exists j \in ℕ x \in \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
465	463 464	sylibr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to x \in ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
466	465	ralrimiva	$⊢ φ \to \forall x \in \underset{k \in Y}{⨉} [A (k), B (k)) x \in ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
467		dfss3	$⊢ \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \leftrightarrow \forall x \in \underset{k \in Y}{⨉} [A (k), B (k)) x \in ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
468	466 467	sylibr	$⊢ φ \to \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
469		ovexd	$⊢ φ \to ℝ^{Y} \in V$
470	237	a1i	$⊢ φ \to ℕ \in V$
471	469 470	elmapd	$⊢ φ \to (K \in ({(ℝ^{Y})}^{ℕ}) \leftrightarrow K : ℕ ⟶ ℝ^{Y})$
472	121 471	mpbird	$⊢ φ \to K \in ({(ℝ^{Y})}^{ℕ})$
473	469 470	elmapd	$⊢ φ \to (J \in ({(ℝ^{Y})}^{ℕ}) \leftrightarrow J : ℕ ⟶ ℝ^{Y})$
474	103 473	mpbird	$⊢ φ \to J \in ({(ℝ^{Y})}^{ℕ})$
475	97 87	elmapd	$⊢ φ \to ({B ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({B ↾}_{Y}) : Y ⟶ ℝ)$
476	213 475	mpbird	$⊢ φ \to {B ↾}_{Y} \in (ℝ^{Y})$
477	97 87	elmapd	$⊢ φ \to ({A ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({A ↾}_{Y}) : Y ⟶ ℝ)$
478	212 477	mpbird	$⊢ φ \to {A ↾}_{Y} \in (ℝ^{Y})$
479		fveq1	$⊢ e = {A ↾}_{Y} \to e (k) = ({A ↾}_{Y}) (k)$
480	479	adantr	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to e (k) = ({A ↾}_{Y}) (k)$
481	259	adantl	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to ({A ↾}_{Y}) (k) = A (k)$
482	480 481	eqtrd	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to e (k) = A (k)$
483	482	oveq1d	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to [e (k), f (k)) = [A (k), f (k))$
484	483	ixpeq2dva	$⊢ e = {A ↾}_{Y} \to \underset{k \in Y}{⨉} [e (k), f (k)) = \underset{k \in Y}{⨉} [A (k), f (k))$
485	484	sseq1d	$⊢ e = {A ↾}_{Y} \to (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \leftrightarrow \underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)))$
486		oveq1	$⊢ e = {A ↾}_{Y} \to e L (Y) f = ({A ↾}_{Y}) L (Y) f$
487	486	breq1d	$⊢ e = {A ↾}_{Y} \to (e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))) \leftrightarrow ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
488	485 487	imbi12d	$⊢ e = {A ↾}_{Y} \to ((\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
489	488	ralbidv	$⊢ e = {A ↾}_{Y} \to (\forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
490	489	ralbidv	$⊢ e = {A ↾}_{Y} \to (\forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
491	490	ralbidv	$⊢ e = {A ↾}_{Y} \to (\forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
492	491	rspcva	$⊢ ({A ↾}_{Y} \in (ℝ^{Y}) \land \forall e \in (ℝ^{Y}) \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [e (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to e L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))) \to \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
493	478 22 492	syl2anc	$⊢ φ \to \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
494		fveq1	$⊢ f = {B ↾}_{Y} \to f (k) = ({B ↾}_{Y}) (k)$
495	494	adantr	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to f (k) = ({B ↾}_{Y}) (k)$
496	260	adantl	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to ({B ↾}_{Y}) (k) = B (k)$
497	495 496	eqtrd	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to f (k) = B (k)$
498	497	oveq2d	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to [A (k), f (k)) = [A (k), B (k))$
499	498	ixpeq2dva	$⊢ f = {B ↾}_{Y} \to \underset{k \in Y}{⨉} [A (k), f (k)) = \underset{k \in Y}{⨉} [A (k), B (k))$
500	499	sseq1d	$⊢ f = {B ↾}_{Y} \to (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \leftrightarrow \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)))$
501		oveq2	$⊢ f = {B ↾}_{Y} \to ({A ↾}_{Y}) L (Y) f = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
502	501	breq1d	$⊢ f = {B ↾}_{Y} \to (({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))) \leftrightarrow ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
503	500 502	imbi12d	$⊢ f = {B ↾}_{Y} \to ((\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
504	503	ralbidv	$⊢ f = {B ↾}_{Y} \to (\forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
505	504	ralbidv	$⊢ f = {B ↾}_{Y} \to (\forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))))$
506	505	rspcva	$⊢ ({B ↾}_{Y} \in (ℝ^{Y}) \land \forall f \in (ℝ^{Y}) \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), f (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) f \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))) \to \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
507	476 493 506	syl2anc	$⊢ φ \to \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))$
508		fveq1	$⊢ g = J \to g (j) = J (j)$
509	508	fveq1d	$⊢ g = J \to g (j) (k) = J (j) (k)$
510	509	oveq1d	$⊢ g = J \to [g (j) (k), h (j) (k)) = [J (j) (k), h (j) (k))$
511	510	ixpeq2dv	$⊢ g = J \to \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) = \underset{k \in Y}{⨉} [J (j) (k), h (j) (k))$
512	511	iuneq2d	$⊢ g = J \to ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) = ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k))$
513	512	sseq2d	$⊢ g = J \to (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \leftrightarrow \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)))$
514	508	oveq1d	$⊢ g = J \to g (j) L (Y) h (j) = J (j) L (Y) h (j)$
515	514	mpteq2dv	$⊢ g = J \to (j \in ℕ ⟼ g (j) L (Y) h (j)) = (j \in ℕ ⟼ J (j) L (Y) h (j))$
516	515	fveq2d	$⊢ g = J \to sum^((j \in ℕ ⟼ g (j) L (Y) h (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) h (j)))$
517	516	breq2d	$⊢ g = J \to (({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))) \leftrightarrow ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j))))$
518	513 517	imbi12d	$⊢ g = J \to ((\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j)))))$
519	518	ralbidv	$⊢ g = J \to (\forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j)))) \leftrightarrow \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j)))))$
520	519	rspcva	$⊢ (J \in ({(ℝ^{Y})}^{ℕ}) \land \forall g \in ({(ℝ^{Y})}^{ℕ}) \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ g (j) L (Y) h (j))))) \to \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j))))$
521	474 507 520	syl2anc	$⊢ φ \to \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j))))$
522		fveq1	$⊢ h = K \to h (j) = K (j)$
523	522	fveq1d	$⊢ h = K \to h (j) (k) = K (j) (k)$
524	523	oveq2d	$⊢ h = K \to [J (j) (k), h (j) (k)) = [J (j) (k), K (j) (k))$
525	524	ixpeq2dv	$⊢ h = K \to \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) = \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
526	525	iuneq2d	$⊢ h = K \to ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) = ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
527	526	sseq2d	$⊢ h = K \to (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \leftrightarrow \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)))$
528	522	oveq2d	$⊢ h = K \to J (j) L (Y) h (j) = J (j) L (Y) K (j)$
529	528	mpteq2dv	$⊢ h = K \to (j \in ℕ ⟼ J (j) L (Y) h (j)) = (j \in ℕ ⟼ J (j) L (Y) K (j))$
530	529	fveq2d	$⊢ h = K \to sum^((j \in ℕ ⟼ J (j) L (Y) h (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
531	530	breq2d	$⊢ h = K \to (({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j))) \leftrightarrow ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))))$
532	527 531	imbi12d	$⊢ h = K \to ((\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j)))) \leftrightarrow (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))))$
533	532	rspcva	$⊢ (K \in ({(ℝ^{Y})}^{ℕ}) \land \forall h \in ({(ℝ^{Y})}^{ℕ}) (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) h (j))))) \to (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))))$
534	472 521 533	syl2anc	$⊢ φ \to (\underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k)) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))))$
535	468 534	mpd	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
536		idd	$⊢ φ \to (({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))))$
537	535 536	mpd	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
538	537	adantr	$⊢ (φ \land Y \neq \emptyset) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
539	62	adantl	$⊢ ((φ \land Y \neq \emptyset) \land j \in ℕ) \to P (j) = J (j) L (Y) K (j)$
540	539	mpteq2dva	$⊢ (φ \land Y \neq \emptyset) \to (j \in ℕ ⟼ P (j)) = (j \in ℕ ⟼ J (j) L (Y) K (j))$
541	540	fveq2d	$⊢ (φ \land Y \neq \emptyset) \to sum^((j \in ℕ ⟼ P (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
542	258 541	breq12d	$⊢ (φ \land Y \neq \emptyset) \to (G \leq sum^((j \in ℕ ⟼ P (j))) \leftrightarrow ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j))))$
543	538 542	mpbird	$⊢ (φ \land Y \neq \emptyset) \to G \leq sum^((j \in ℕ ⟼ P (j)))$
544	543	adantr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to G \leq sum^((j \in ℕ ⟼ P (j)))$
545	247 249 250 289 544	ltletrd	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
546	235 246 545	syl2anc	$⊢ ((φ \land Y \neq \emptyset) \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
547	234 546	pm2.61dan	$⊢ (φ \land Y \neq \emptyset) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
548	207 208 209 210 227 547	sge0uzfsumgt	$⊢ (φ \land Y \neq \emptyset) \to \exists m \in ℕ \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)$
549	226	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} \in ℝ$
550		fzfid	$⊢ φ \to (1 \dots m) \in Fin$
551		simpl	$⊢ (φ \land j \in (1 \dots m)) \to φ$
552		elfznn	$⊢ j \in (1 \dots m) \to j \in ℕ$
553	552	adantl	$⊢ (φ \land j \in (1 \dots m)) \to j \in ℕ$
554	50 126	sselid	$⊢ (φ \land j \in ℕ) \to P (j) \in ℝ$
555	551 553 554	syl2anc	$⊢ (φ \land j \in (1 \dots m)) \to P (j) \in ℝ$
556	550 555	fsumrecl	$⊢ φ \to \sum_{j = 1}^{m} P (j) \in ℝ$
557	556	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \sum_{j = 1}^{m} P (j) \in ℝ$
558		simpr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)$
559	549 557 558	ltled	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} \leq \sum_{j = 1}^{m} P (j)$
560	216	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to G \in ℝ$
561	222	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to 1 + E \in ℝ^{+}$
562	560 557 561	ledivmuld	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to (\frac{G}{1 + E} \leq \sum_{j = 1}^{m} P (j) \leftrightarrow G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
563	559 562	mpbid	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
564	563	ex	$⊢ φ \to (\frac{G}{1 + E} < \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
565	564	adantr	$⊢ (φ \land m \in ℕ) \to (\frac{G}{1 + E} < \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
566	565	adantlr	$⊢ ((φ \land Y \neq \emptyset) \land m \in ℕ) \to (\frac{G}{1 + E} < \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
567	566	reximdva	$⊢ (φ \land Y \neq \emptyset) \to (\exists m \in ℕ \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
568	548 567	mpd	$⊢ (φ \land Y \neq \emptyset) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
569	204 206 568	syl2anc	$⊢ (φ \land \neg Y = \emptyset) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
570	203 569	pm2.61dan	$⊢ φ \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
571	2	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to X \in Fin$
572	3	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to Y \subseteq X$
573	4	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to Z \in (X ∖ Y)$
574	6	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to A : W ⟶ ℝ$
575	7	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to B : W ⟶ ℝ$
576	10	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to C : ℕ ⟶ ℝ^{W}$
577		eqid	$⊢ (y \in Y ⟼ 0) = (y \in Y ⟼ 0)$
578		eqid	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
579	12	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to D : ℕ ⟶ ℝ^{W}$
580		eqid	$⊢ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)))$
581		fveq2	$⊢ i = j \to C (i) = C (j)$
582		fveq2	$⊢ i = j \to D (i) = D (j)$
583	581 582	oveq12d	$⊢ i = j \to C (i) L (W) D (i) = C (j) L (W) D (j)$
584	583	cbvmptv	$⊢ (i \in ℕ ⟼ C (i) L (W) D (i)) = (j \in ℕ ⟼ C (j) L (W) D (j))$
585	584	fveq2i	$⊢ sum^((i \in ℕ ⟼ C (i) L (W) D (i))) = sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
586	585 14	eqeltrid	$⊢ φ \to sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
587	586	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
588		eleq1w	$⊢ j = i \to (j \in Y \leftrightarrow i \in Y)$
589		fveq2	$⊢ j = i \to c (j) = c (i)$
590	589	breq1d	$⊢ j = i \to (c (j) \leq x \leftrightarrow c (i) \leq x)$
591	590 589	ifbieq1d	$⊢ j = i \to if (c (j) \leq x, c (j), x) = if (c (i) \leq x, c (i), x)$
592	588 589 591	ifbieq12d	$⊢ j = i \to if (j \in Y, c (j), if (c (j) \leq x, c (j), x)) = if (i \in Y, c (i), if (c (i) \leq x, c (i), x))$
593	592	cbvmptv	$⊢ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))) = (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x)))$
594	593	mpteq2i	$⊢ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))) = (c \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x))))$
595	594	mpteq2i	$⊢ (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (j \in W ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x))))) = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x)))))$
596	15 595	eqtri	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x)))))$
597	17	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to E \in ℝ^{+}$
598		fveq2	$⊢ j = i \to C (j) = C (i)$
599		fveq2	$⊢ j = i \to D (j) = D (i)$
600	599	fveq2d	$⊢ j = i \to H (z) (D (j)) = H (z) (D (i))$
601	598 600	oveq12d	$⊢ j = i \to C (j) L (W) H (z) (D (j)) = C (i) L (W) H (z) (D (i))$
602	601	cbvmptv	$⊢ (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (i \in ℕ ⟼ C (i) L (W) H (z) (D (i)))$
603	602	fveq2i	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))$
604	603	oveq2i	$⊢ (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = (1 + E) sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))$
605	604	breq2i	$⊢ G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) \leftrightarrow G (z - A (Z)) \leq (1 + E) sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))$
606	605	rabbii	$⊢ \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j))))\} = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))\}$
607	18 606	eqtri	$⊢ U = \{z \in [A (Z), B (Z)] \| G (z - A (Z)) \leq (1 + E) sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))\}$
608	19	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to S \in U$
609	20	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to S < B (Z)$
610		eqid	$⊢ (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) = (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i))$
611		simp2	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to m \in ℕ$
612		id	$⊢ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
613		fveq2	$⊢ j = i \to P (j) = P (i)$
614	613	cbvsumv	$⊢ \sum_{j = 1}^{m} P (j) = \sum_{i = 1}^{m} P (i)$
615	614	oveq2i	$⊢ (1 + E) \sum_{j = 1}^{m} P (j) = (1 + E) \sum_{i = 1}^{m} P (i)$
616	615	a1i	$⊢ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to (1 + E) \sum_{j = 1}^{m} P (j) = (1 + E) \sum_{i = 1}^{m} P (i)$
617	612 616	breqtrd	$⊢ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{i = 1}^{m} P (i)$
618	617	3ad2ant3	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to G \leq (1 + E) \sum_{i = 1}^{m} P (i)$
619		simpl	$⊢ (φ \land i \in (1 \dots m)) \to φ$
620		elfznn	$⊢ i \in (1 \dots m) \to i \in ℕ$
621	620	adantl	$⊢ (φ \land i \in (1 \dots m)) \to i \in ℕ$
622		eleq1w	$⊢ j = i \to (j \in ℕ \leftrightarrow i \in ℕ)$
623		fveq2	$⊢ j = i \to J (j) = J (i)$
624		fveq2	$⊢ j = i \to K (j) = K (i)$
625	623 624	oveq12d	$⊢ j = i \to J (j) L (Y) K (j) = J (i) L (Y) K (i)$
626	613 625	eqeq12d	$⊢ j = i \to (P (j) = J (j) L (Y) K (j) \leftrightarrow P (i) = J (i) L (Y) K (i))$
627	622 626	imbi12d	$⊢ j = i \to ((j \in ℕ \to P (j) = J (j) L (Y) K (j)) \leftrightarrow (i \in ℕ \to P (i) = J (i) L (Y) K (i)))$
628	627 62	chvarvv	$⊢ i \in ℕ \to P (i) = J (i) L (Y) K (i)$
629	628	adantl	$⊢ (φ \land i \in ℕ) \to P (i) = J (i) L (Y) K (i)$
630	622	anbi2d	$⊢ j = i \to ((φ \land j \in ℕ) \leftrightarrow (φ \land i \in ℕ))$
631	598	fveq1d	$⊢ j = i \to C (j) (Z) = C (i) (Z)$
632	599	fveq1d	$⊢ j = i \to D (j) (Z) = D (i) (Z)$
633	631 632	oveq12d	$⊢ j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))$
634	633	eleq2d	$⊢ j = i \to (S \in [C (j) (Z), D (j) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z)))$
635	598	reseq1d	$⊢ j = i \to {C (j) ↾}_{Y} = {C (i) ↾}_{Y}$
636	634 635	ifbieq1d	$⊢ j = i \to if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
637	623 636	eqeq12d	$⊢ j = i \to (J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F) \leftrightarrow J (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F))$
638	630 637	imbi12d	$⊢ j = i \to (((φ \land j \in ℕ) \to J (j) = if (S \in [C (j) (Z), D (j) (Z)), {C (j) ↾}_{Y}, F)) \leftrightarrow ((φ \land i \in ℕ) \to J (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)))$
639	638 161	chvarvv	$⊢ (φ \land i \in ℕ) \to J (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
640	599	reseq1d	$⊢ j = i \to {D (j) ↾}_{Y} = {D (i) ↾}_{Y}$
641	634 640	ifbieq1d	$⊢ j = i \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
642	624 641	eqeq12d	$⊢ j = i \to (K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \leftrightarrow K (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F))$
643	630 642	imbi12d	$⊢ j = i \to (((φ \land j \in ℕ) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)) \leftrightarrow ((φ \land i \in ℕ) \to K (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)))$
644	643 443	chvarvv	$⊢ (φ \land i \in ℕ) \to K (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
645	639 644	oveq12d	$⊢ (φ \land i \in ℕ) \to J (i) L (Y) K (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F) L (Y) if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
646	629 645	eqtrd	$⊢ (φ \land i \in ℕ) \to P (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F) L (Y) if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
647		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
648		ovexd	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) \in V$
649	610	fvmpt2	$⊢ (i \in ℕ \land (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) \in V) \to (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)$
650	647 648 649	syl2anc	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i) = (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)$
651		fvex	$⊢ C (i) \in V$
652	651	resex	$⊢ {C (i) ↾}_{Y} \in V$
653	652	a1i	$⊢ φ \to {C (i) ↾}_{Y} \in V$
654	9 155	eqeltrrid	$⊢ φ \to (y \in Y ⟼ 0) \in V$
655	653 654	ifcld	$⊢ φ \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
656	655	adantr	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
657	578	fvmpt2	$⊢ (i \in ℕ \land if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))$
658	647 656 657	syl2anc	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))$
659	9	eqcomi	$⊢ (y \in Y ⟼ 0) = F$
660		ifeq2	$⊢ (y \in Y ⟼ 0) = F \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
661	659 660	ax-mp	$⊢ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
662	661	a1i	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
663	658 662	eqtrd	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
664		fvex	$⊢ D (i) \in V$
665	664	resex	$⊢ {D (i) ↾}_{Y} \in V$
666	665	a1i	$⊢ φ \to {D (i) ↾}_{Y} \in V$
667	666 654	ifcld	$⊢ φ \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
668	667	adantr	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
669	580	fvmpt2	$⊢ (i \in ℕ \land if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))$
670	647 668 669	syl2anc	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))$
671		biid	$⊢ S \in [C (i) (Z), D (i) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z))$
672	671 659	ifbieq2i	$⊢ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
673	672	a1i	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
674	670 673	eqtrd	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
675	663 674	oveq12d	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F) L (Y) if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
676	650 675	eqtrd	$⊢ (φ \land i \in ℕ) \to (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F) L (Y) if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
677	646 676	eqtr4d	$⊢ (φ \land i \in ℕ) \to P (i) = (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
678	619 621 677	syl2anc	$⊢ (φ \land i \in (1 \dots m)) \to P (i) = (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
679	678	3ad2antl1	$⊢ ((φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \land i \in (1 \dots m)) \to P (i) = (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
680	679	sumeq2dv	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to \sum_{i = 1}^{m} P (i) = \sum_{i = 1}^{m} (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
681	680	oveq2d	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to (1 + E) \sum_{i = 1}^{m} P (i) = (1 + E) \sum_{i = 1}^{m} (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
682	618 681	breqtrd	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to G \leq (1 + E) \sum_{i = 1}^{m} (i \in ℕ ⟼ (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i) L (Y) (i \in ℕ ⟼ if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0))) (i)) (i)$
683		fveq2	$⊢ j = h \to D (j) = D (h)$
684	683	fveq1d	$⊢ j = h \to D (j) (Z) = D (h) (Z)$
685	684	cbvmptv	$⊢ (j \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (j) (Z)) = (h \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (h) (Z))$
686	685	rneqi	$⊢ ran (j \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (j) (Z)) = ran (h \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (h) (Z))$
687		fveq2	$⊢ h = i \to C (h) = C (i)$
688	687	fveq1d	$⊢ h = i \to C (h) (Z) = C (i) (Z)$
689		fveq2	$⊢ h = i \to D (h) = D (i)$
690	689	fveq1d	$⊢ h = i \to D (h) (Z) = D (i) (Z)$
691	688 690	oveq12d	$⊢ h = i \to [C (h) (Z), D (h) (Z)) = [C (i) (Z), D (i) (Z))$
692	691	eleq2d	$⊢ h = i \to (S \in [C (h) (Z), D (h) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z)))$
693	692	cbvrabv	$⊢ \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} = \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\}$
694	693	mpteq1i	$⊢ (j \in \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} ⟼ D (j) (Z)) = (j \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (j) (Z))$
695	694	rneqi	$⊢ ran (j \in \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} ⟼ D (j) (Z)) = ran (j \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (j) (Z))$
696	695	uneq2i	$⊢ \{B (Z)\} \cup ran (j \in \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} ⟼ D (j) (Z)) = \{B (Z)\} \cup ran (j \in \{i \in (1 \dots m) \| S \in [C (i) (Z), D (i) (Z))\} ⟼ D (j) (Z))$
697		eqid	$⊢ inf (\{B (Z)\} \cup ran (j \in \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} ⟼ D (j) (Z)) ℝ <) = inf (\{B (Z)\} \cup ran (j \in \{h \in (1 \dots m) \| S \in [C (h) (Z), D (h) (Z))\} ⟼ D (j) (Z)) ℝ <)$
698	1 571 572 573 5 574 575 576 577 578 579 580 587 596 16 597 607 608 609 610 611 682 686 696 697	hoidmvlelem2	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to \exists u \in U S < u$
699	698	3exp	$⊢ φ \to (m \in ℕ \to (G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to \exists u \in U S < u))$
700	699	rexlimdv	$⊢ φ \to (\exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to \exists u \in U S < u)$
701	570 700	mpd	$⊢ φ \to \exists u \in U S < u$

Metamath Proof Explorer

Theorem hoidmvlelem3

Proof