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	birani	$⊢ (k \in W \land \neg k \in Y) \to k \in (Y \cup \{Z\})$
354		simpr	$⊢ (k \in W \land \neg k \in Y) \to \neg k \in Y$
355		elunnel1	$⊢ (k \in (Y \cup \{Z\}) \land \neg k \in Y) \to k \in \{Z\}$
356	353 354 355	syl2anc	$⊢ (k \in W \land \neg k \in Y) \to k \in \{Z\}$
357		elsni	$⊢ k \in \{Z\} \to k = Z$
358	356 357	syl	$⊢ (k \in W \land \neg k \in Y) \to k = Z$
359		fveq2	$⊢ k = Z \to A (k) = A (Z)$
360		fveq2	$⊢ k = Z \to B (k) = B (Z)$
361	359 360	oveq12d	$⊢ k = Z \to [A (k), B (k)) = [A (Z), B (Z))$
362	358 361	syl	$⊢ (k \in W \land \neg k \in Y) \to [A (k), B (k)) = [A (Z), B (Z))$
363	362	adantll	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to [A (k), B (k)) = [A (Z), B (Z))$
364	351 363	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)))$
365	349 364	mpbird	$⊢ ((φ \land k \in W) \land \neg k \in Y) \to if (k \in Y, x (k), S) \in [A (k), B (k))$
366	365	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))$
367	330 366	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))$
368	319 367	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))$
369	368	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)))$
370	311 369	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))$
371	306 370	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)))$
372		fvex	$⊢ O (x) \in V$
373	372	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)))$
374	371 373	sylibr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to O (x) \in \underset{k \in W}{⨉} [A (k), B (k))$
375	290 374	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))$
376		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))$
377	375 376	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))$
378		ixpfn	$⊢ x \in \underset{k \in Y}{⨉} [A (k), B (k)) \to x Fn Y$
379	378	adantl	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to x Fn Y$
380	379	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$
381		nfv	$⊢ Ⅎ k j \in ℕ$
382	311 381	nfan	$⊢ Ⅎ k ((φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \land j \in ℕ)$
383		nfcv	$⊢ \underline{Ⅎ} k O (x)$
384		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
385	383 384	nfel	$⊢ Ⅎ k O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k))$
386	382 385	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)))$
387	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)$
388	293	adantr	$⊢ (φ \land k \in Y) \to if (k \in Y, x (k), S) \in V$
389	267 388 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)$
390	389	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)$
391	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)$
392	387 390 391	3eqtrrd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k)) \land k \in Y) \to x (k) = O (x) (k)$
393	392	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)$
394	372	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)))$
395	394	birani	$⊢ (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)))$
396	395	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))$
397	266	adantl	$⊢ (O (x) \in \underset{k \in W}{⨉} [C (j) (k), D (j) (k)) \land k \in Y) \to k \in W$
398		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))$
399	396 397 398	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))$
400	399	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))$
401	393 400	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))$
402	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 φ$
403	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 ℕ$
404	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)$
405		eqidd	$⊢ φ \to (k \in W ⟼ if (k \in Y, x (k), S)) = (k \in W ⟼ if (k \in Y, x (k), S))$
406		eleq1	$⊢ k = Z \to (k \in Y \leftrightarrow Z \in Y)$
407		fveq2	$⊢ k = Z \to x (k) = x (Z)$
408	406 407	ifbieq1d	$⊢ k = Z \to if (k \in Y, x (k), S) = if (Z \in Y, x (Z), S)$
409	408	adantl	$⊢ (φ \land k = Z) \to if (k \in Y, x (k), S) = if (Z \in Y, x (Z), S)$
410		fvexd	$⊢ φ \to x (Z) \in V$
411	410 292	ifcld	$⊢ φ \to if (Z \in Y, x (Z), S) \in V$
412	405 409 336 411	fvmptd	$⊢ φ \to (k \in W ⟼ if (k \in Y, x (k), S)) (Z) = if (Z \in Y, x (Z), S)$
413	412	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)$
414	4	eldifbd	$⊢ φ \to \neg Z \in Y$
415	414	iffalsed	$⊢ φ \to if (Z \in Y, x (Z), S) = S$
416	415	adantr	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to if (Z \in Y, x (Z), S) = S$
417	404 413 416	3eqtrrd	$⊢ (φ \land x \in \underset{k \in Y}{⨉} [A (k), B (k))) \to S = O (x) (Z)$
418	417	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)$
419	402 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$
420	394	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))$
421	420	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))$
422		fveq2	$⊢ k = Z \to O (x) (k) = O (x) (Z)$
423		fveq2	$⊢ k = Z \to C (j) (k) = C (j) (Z)$
424		fveq2	$⊢ k = Z \to D (j) (k) = D (j) (Z)$
425	423 424	oveq12d	$⊢ k = Z \to [C (j) (k), D (j) (k)) = [C (j) (Z), D (j) (Z))$
426	422 425	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)))$
427	426	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))$
428	419 421 427	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))$
429	418 428	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))$
430	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)$
431	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}$
432	430 431	eqtrd	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to J (j) = {C (j) ↾}_{Y}$
433	432	fveq1d	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to J (j) (k) = ({C (j) ↾}_{Y}) (k)$
434	402 403 429 433	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)$
435	434	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)$
436		fvres	$⊢ k \in Y \to ({C (j) ↾}_{Y}) (k) = C (j) (k)$
437	436	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)$
438	435 437	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)$
439	120	elexd	$⊢ (φ \land j \in ℕ) \to if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F) \in V$
440	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)$
441	151 439 440	syl2anc	$⊢ (φ \land j \in ℕ) \to K (j) = if (S \in [C (j) (Z), D (j) (Z)), {D (j) ↾}_{Y}, F)$
442	441	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)$
443	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}$
444	442 443	eqtrd	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to K (j) = {D (j) ↾}_{Y}$
445	444	fveq1d	$⊢ (φ \land j \in ℕ \land S \in [C (j) (Z), D (j) (Z))) \to K (j) (k) = ({D (j) ↾}_{Y}) (k)$
446	402 403 429 445	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)$
447	446	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)$
448		fvres	$⊢ k \in Y \to ({D (j) ↾}_{Y}) (k) = D (j) (k)$
449	448	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)$
450	447 449	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)$
451	438 450	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))$
452	451	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))$
453	401 452	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))$
454	453	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)))$
455	386 454	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))$
456	380 455	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)))$
457	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)))$
458	456 457	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))$
459	458	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)))$
460	459	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)))$
461	377 460	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))$
462		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))$
463	461 462	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))$
464	463	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))$
465		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))$
466	464 465	sylibr	$⊢ φ \to \underset{k \in Y}{⨉} [A (k), B (k)) \subseteq ⋃_{j \in ℕ} \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
467		ovexd	$⊢ φ \to ℝ^{Y} \in V$
468	237	a1i	$⊢ φ \to ℕ \in V$
469	467 468	elmapd	$⊢ φ \to (K \in ({(ℝ^{Y})}^{ℕ}) \leftrightarrow K : ℕ ⟶ ℝ^{Y})$
470	121 469	mpbird	$⊢ φ \to K \in ({(ℝ^{Y})}^{ℕ})$
471	467 468	elmapd	$⊢ φ \to (J \in ({(ℝ^{Y})}^{ℕ}) \leftrightarrow J : ℕ ⟶ ℝ^{Y})$
472	103 471	mpbird	$⊢ φ \to J \in ({(ℝ^{Y})}^{ℕ})$
473	97 87	elmapd	$⊢ φ \to ({B ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({B ↾}_{Y}) : Y ⟶ ℝ)$
474	213 473	mpbird	$⊢ φ \to {B ↾}_{Y} \in (ℝ^{Y})$
475	97 87	elmapd	$⊢ φ \to ({A ↾}_{Y} \in (ℝ^{Y}) \leftrightarrow ({A ↾}_{Y}) : Y ⟶ ℝ)$
476	212 475	mpbird	$⊢ φ \to {A ↾}_{Y} \in (ℝ^{Y})$
477		fveq1	$⊢ e = {A ↾}_{Y} \to e (k) = ({A ↾}_{Y}) (k)$
478	477	adantr	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to e (k) = ({A ↾}_{Y}) (k)$
479	259	adantl	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to ({A ↾}_{Y}) (k) = A (k)$
480	478 479	eqtrd	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to e (k) = A (k)$
481	480	oveq1d	$⊢ (e = {A ↾}_{Y} \land k \in Y) \to [e (k), f (k)) = [A (k), f (k))$
482	481	ixpeq2dva	$⊢ e = {A ↾}_{Y} \to \underset{k \in Y}{⨉} [e (k), f (k)) = \underset{k \in Y}{⨉} [A (k), f (k))$
483	482	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)))$
484		oveq1	$⊢ e = {A ↾}_{Y} \to e L (Y) f = ({A ↾}_{Y}) L (Y) f$
485	484	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))))$
486	483 485	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)))))$
487	486	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)))))$
488	487	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)))))$
489	488	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)))))$
490	489	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))))$
491	476 22 490	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))))$
492		fveq1	$⊢ f = {B ↾}_{Y} \to f (k) = ({B ↾}_{Y}) (k)$
493	492	adantr	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to f (k) = ({B ↾}_{Y}) (k)$
494	260	adantl	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to ({B ↾}_{Y}) (k) = B (k)$
495	493 494	eqtrd	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to f (k) = B (k)$
496	495	oveq2d	$⊢ (f = {B ↾}_{Y} \land k \in Y) \to [A (k), f (k)) = [A (k), B (k))$
497	496	ixpeq2dva	$⊢ f = {B ↾}_{Y} \to \underset{k \in Y}{⨉} [A (k), f (k)) = \underset{k \in Y}{⨉} [A (k), B (k))$
498	497	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)))$
499		oveq2	$⊢ f = {B ↾}_{Y} \to ({A ↾}_{Y}) L (Y) f = ({A ↾}_{Y}) L (Y) ({B ↾}_{Y})$
500	499	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))))$
501	498 500	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)))))$
502	501	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)))))$
503	502	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)))))$
504	503	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))))$
505	474 491 504	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))))$
506		fveq1	$⊢ g = J \to g (j) = J (j)$
507	506	fveq1d	$⊢ g = J \to g (j) (k) = J (j) (k)$
508	507	oveq1d	$⊢ g = J \to [g (j) (k), h (j) (k)) = [J (j) (k), h (j) (k))$
509	508	ixpeq2dv	$⊢ g = J \to \underset{k \in Y}{⨉} [g (j) (k), h (j) (k)) = \underset{k \in Y}{⨉} [J (j) (k), h (j) (k))$
510	509	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))$
511	510	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)))$
512	506	oveq1d	$⊢ g = J \to g (j) L (Y) h (j) = J (j) L (Y) h (j)$
513	512	mpteq2dv	$⊢ g = J \to (j \in ℕ ⟼ g (j) L (Y) h (j)) = (j \in ℕ ⟼ J (j) L (Y) h (j))$
514	513	fveq2d	$⊢ g = J \to sum^((j \in ℕ ⟼ g (j) L (Y) h (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) h (j)))$
515	514	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))))$
516	511 515	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)))))$
517	516	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)))))$
518	517	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))))$
519	472 505 518	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))))$
520		fveq1	$⊢ h = K \to h (j) = K (j)$
521	520	fveq1d	$⊢ h = K \to h (j) (k) = K (j) (k)$
522	521	oveq2d	$⊢ h = K \to [J (j) (k), h (j) (k)) = [J (j) (k), K (j) (k))$
523	522	ixpeq2dv	$⊢ h = K \to \underset{k \in Y}{⨉} [J (j) (k), h (j) (k)) = \underset{k \in Y}{⨉} [J (j) (k), K (j) (k))$
524	523	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))$
525	524	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)))$
526	520	oveq2d	$⊢ h = K \to J (j) L (Y) h (j) = J (j) L (Y) K (j)$
527	526	mpteq2dv	$⊢ h = K \to (j \in ℕ ⟼ J (j) L (Y) h (j)) = (j \in ℕ ⟼ J (j) L (Y) K (j))$
528	527	fveq2d	$⊢ h = K \to sum^((j \in ℕ ⟼ J (j) L (Y) h (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
529	528	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))))$
530	525 529	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)))))$
531	530	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))))$
532	470 519 531	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))))$
533	466 532	mpd	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
534		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))))$
535	533 534	mpd	$⊢ φ \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
536	535	adantr	$⊢ (φ \land Y \neq \emptyset) \to ({A ↾}_{Y}) L (Y) ({B ↾}_{Y}) \leq sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
537	62	adantl	$⊢ ((φ \land Y \neq \emptyset) \land j \in ℕ) \to P (j) = J (j) L (Y) K (j)$
538	537	mpteq2dva	$⊢ (φ \land Y \neq \emptyset) \to (j \in ℕ ⟼ P (j)) = (j \in ℕ ⟼ J (j) L (Y) K (j))$
539	538	fveq2d	$⊢ (φ \land Y \neq \emptyset) \to sum^((j \in ℕ ⟼ P (j))) = sum^((j \in ℕ ⟼ J (j) L (Y) K (j)))$
540	258 539	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))))$
541	536 540	mpbird	$⊢ (φ \land Y \neq \emptyset) \to G \leq sum^((j \in ℕ ⟼ P (j)))$
542	541	adantr	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to G \leq sum^((j \in ℕ ⟼ P (j)))$
543	247 249 250 289 542	ltletrd	$⊢ ((φ \land Y \neq \emptyset) \land sum^((j \in ℕ ⟼ P (j))) \in ℝ) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
544	235 246 543	syl2anc	$⊢ ((φ \land Y \neq \emptyset) \land \neg sum^((j \in ℕ ⟼ P (j))) = +∞) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
545	234 544	pm2.61dan	$⊢ (φ \land Y \neq \emptyset) \to \frac{G}{1 + E} < sum^((j \in ℕ ⟼ P (j)))$
546	207 208 209 210 227 545	sge0uzfsumgt	$⊢ (φ \land Y \neq \emptyset) \to \exists m \in ℕ \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)$
547	226	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} \in ℝ$
548		fzfid	$⊢ φ \to (1 \dots m) \in Fin$
549		simpl	$⊢ (φ \land j \in (1 \dots m)) \to φ$
550		elfznn	$⊢ j \in (1 \dots m) \to j \in ℕ$
551	550	adantl	$⊢ (φ \land j \in (1 \dots m)) \to j \in ℕ$
552	50 126	sselid	$⊢ (φ \land j \in ℕ) \to P (j) \in ℝ$
553	549 551 552	syl2anc	$⊢ (φ \land j \in (1 \dots m)) \to P (j) \in ℝ$
554	548 553	fsumrecl	$⊢ φ \to \sum_{j = 1}^{m} P (j) \in ℝ$
555	554	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \sum_{j = 1}^{m} P (j) \in ℝ$
556		simpr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)$
557	547 555 556	ltled	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to \frac{G}{1 + E} \leq \sum_{j = 1}^{m} P (j)$
558	216	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to G \in ℝ$
559	222	adantr	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to 1 + E \in ℝ^{+}$
560	558 555 559	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))$
561	557 560	mpbid	$⊢ (φ \land \frac{G}{1 + E} < \sum_{j = 1}^{m} P (j)) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
562	561	ex	$⊢ φ \to (\frac{G}{1 + E} < \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j))$
563	562	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))$
564	563	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))$
565	564	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))$
566	546 565	mpd	$⊢ (φ \land Y \neq \emptyset) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
567	204 206 566	syl2anc	$⊢ (φ \land \neg Y = \emptyset) \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
568	203 567	pm2.61dan	$⊢ φ \to \exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
569	2	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to X \in Fin$
570	3	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to Y \subseteq X$
571	4	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to Z \in (X ∖ Y)$
572	6	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to A : W ⟶ ℝ$
573	7	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to B : W ⟶ ℝ$
574	10	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to C : ℕ ⟶ ℝ^{W}$
575		eqid	$⊢ (y \in Y ⟼ 0) = (y \in Y ⟼ 0)$
576		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)))$
577	12	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to D : ℕ ⟶ ℝ^{W}$
578		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)))$
579		fveq2	$⊢ i = j \to C (i) = C (j)$
580		fveq2	$⊢ i = j \to D (i) = D (j)$
581	579 580	oveq12d	$⊢ i = j \to C (i) L (W) D (i) = C (j) L (W) D (j)$
582	581	cbvmptv	$⊢ (i \in ℕ ⟼ C (i) L (W) D (i)) = (j \in ℕ ⟼ C (j) L (W) D (j))$
583	582	fveq2i	$⊢ sum^((i \in ℕ ⟼ C (i) L (W) D (i))) = sum^((j \in ℕ ⟼ C (j) L (W) D (j)))$
584	583 14	eqeltrid	$⊢ φ \to sum^((i \in ℕ ⟼ C (i) L (W) D (i))) \in ℝ$
585	584	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 ℝ$
586		eleq1w	$⊢ j = i \to (j \in Y \leftrightarrow i \in Y)$
587		fveq2	$⊢ j = i \to c (j) = c (i)$
588	587	breq1d	$⊢ j = i \to (c (j) \leq x \leftrightarrow c (i) \leq x)$
589	588 587	ifbieq1d	$⊢ j = i \to if (c (j) \leq x, c (j), x) = if (c (i) \leq x, c (i), x)$
590	586 587 589	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))$
591	590	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)))$
592	591	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))))$
593	592	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)))))$
594	15 593	eqtri	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{W}) ⟼ (i \in W ⟼ if (i \in Y, c (i), if (c (i) \leq x, c (i), x)))))$
595	17	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to E \in ℝ^{+}$
596		fveq2	$⊢ j = i \to C (j) = C (i)$
597		fveq2	$⊢ j = i \to D (j) = D (i)$
598	597	fveq2d	$⊢ j = i \to H (z) (D (j)) = H (z) (D (i))$
599	596 598	oveq12d	$⊢ j = i \to C (j) L (W) H (z) (D (j)) = C (i) L (W) H (z) (D (i))$
600	599	cbvmptv	$⊢ (j \in ℕ ⟼ C (j) L (W) H (z) (D (j))) = (i \in ℕ ⟼ C (i) L (W) H (z) (D (i)))$
601	600	fveq2i	$⊢ sum^((j \in ℕ ⟼ C (j) L (W) H (z) (D (j)))) = sum^((i \in ℕ ⟼ C (i) L (W) H (z) (D (i))))$
602	601	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))))$
603	602	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))))$
604	603	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))))\}$
605	18 604	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))))\}$
606	19	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to S \in U$
607	20	3ad2ant1	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to S < B (Z)$
608		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))$
609		simp2	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to m \in ℕ$
610		id	$⊢ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{j = 1}^{m} P (j)$
611		fveq2	$⊢ j = i \to P (j) = P (i)$
612	611	cbvsumv	$⊢ \sum_{j = 1}^{m} P (j) = \sum_{i = 1}^{m} P (i)$
613	612	oveq2i	$⊢ (1 + E) \sum_{j = 1}^{m} P (j) = (1 + E) \sum_{i = 1}^{m} P (i)$
614	613	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)$
615	610 614	breqtrd	$⊢ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to G \leq (1 + E) \sum_{i = 1}^{m} P (i)$
616	615	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)$
617		simpl	$⊢ (φ \land i \in (1 \dots m)) \to φ$
618		elfznn	$⊢ i \in (1 \dots m) \to i \in ℕ$
619	618	adantl	$⊢ (φ \land i \in (1 \dots m)) \to i \in ℕ$
620		eleq1w	$⊢ j = i \to (j \in ℕ \leftrightarrow i \in ℕ)$
621		fveq2	$⊢ j = i \to J (j) = J (i)$
622		fveq2	$⊢ j = i \to K (j) = K (i)$
623	621 622	oveq12d	$⊢ j = i \to J (j) L (Y) K (j) = J (i) L (Y) K (i)$
624	611 623	eqeq12d	$⊢ j = i \to (P (j) = J (j) L (Y) K (j) \leftrightarrow P (i) = J (i) L (Y) K (i))$
625	620 624	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)))$
626	625 62	chvarvv	$⊢ i \in ℕ \to P (i) = J (i) L (Y) K (i)$
627	626	adantl	$⊢ (φ \land i \in ℕ) \to P (i) = J (i) L (Y) K (i)$
628	620	anbi2d	$⊢ j = i \to ((φ \land j \in ℕ) \leftrightarrow (φ \land i \in ℕ))$
629	596	fveq1d	$⊢ j = i \to C (j) (Z) = C (i) (Z)$
630	597	fveq1d	$⊢ j = i \to D (j) (Z) = D (i) (Z)$
631	629 630	oveq12d	$⊢ j = i \to [C (j) (Z), D (j) (Z)) = [C (i) (Z), D (i) (Z))$
632	631	eleq2d	$⊢ j = i \to (S \in [C (j) (Z), D (j) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z)))$
633	596	reseq1d	$⊢ j = i \to {C (j) ↾}_{Y} = {C (i) ↾}_{Y}$
634	632 633	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)$
635	621 634	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))$
636	628 635	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)))$
637	636 161	chvarvv	$⊢ (φ \land i \in ℕ) \to J (i) = if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, F)$
638	597	reseq1d	$⊢ j = i \to {D (j) ↾}_{Y} = {D (i) ↾}_{Y}$
639	632 638	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)$
640	622 639	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))$
641	628 640	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)))$
642	641 441	chvarvv	$⊢ (φ \land i \in ℕ) \to K (i) = if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, F)$
643	637 642	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)$
644	627 643	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)$
645		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
646		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$
647	608	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)$
648	645 646 647	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)$
649		fvex	$⊢ C (i) \in V$
650	649	resex	$⊢ {C (i) ↾}_{Y} \in V$
651	650	a1i	$⊢ φ \to {C (i) ↾}_{Y} \in V$
652	9 155	eqeltrrid	$⊢ φ \to (y \in Y ⟼ 0) \in V$
653	651 652	ifcld	$⊢ φ \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
654	653	adantr	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {C (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
655	576	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))$
656	645 654 655	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))$
657	9	eqcomi	$⊢ (y \in Y ⟼ 0) = F$
658		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)$
659	657 658	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)$
660	659	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)$
661	656 660	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)$
662		fvex	$⊢ D (i) \in V$
663	662	resex	$⊢ {D (i) ↾}_{Y} \in V$
664	663	a1i	$⊢ φ \to {D (i) ↾}_{Y} \in V$
665	664 652	ifcld	$⊢ φ \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
666	665	adantr	$⊢ (φ \land i \in ℕ) \to if (S \in [C (i) (Z), D (i) (Z)), {D (i) ↾}_{Y}, (y \in Y ⟼ 0)) \in V$
667	578	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))$
668	645 666 667	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))$
669		biid	$⊢ S \in [C (i) (Z), D (i) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z))$
670	669 657	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)$
671	670	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)$
672	668 671	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)$
673	661 672	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)$
674	648 673	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)$
675	644 674	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)$
676	617 619 675	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)$
677	676	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)$
678	677	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)$
679	678	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)$
680	616 679	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)$
681		fveq2	$⊢ j = h \to D (j) = D (h)$
682	681	fveq1d	$⊢ j = h \to D (j) (Z) = D (h) (Z)$
683	682	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))$
684	683	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))$
685		fveq2	$⊢ h = i \to C (h) = C (i)$
686	685	fveq1d	$⊢ h = i \to C (h) (Z) = C (i) (Z)$
687		fveq2	$⊢ h = i \to D (h) = D (i)$
688	687	fveq1d	$⊢ h = i \to D (h) (Z) = D (i) (Z)$
689	686 688	oveq12d	$⊢ h = i \to [C (h) (Z), D (h) (Z)) = [C (i) (Z), D (i) (Z))$
690	689	eleq2d	$⊢ h = i \to (S \in [C (h) (Z), D (h) (Z)) \leftrightarrow S \in [C (i) (Z), D (i) (Z)))$
691	690	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))\}$
692	691	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))$
693	692	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))$
694	693	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))$
695		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)) ℝ <)$
696	1 569 570 571 5 572 573 574 575 576 577 578 585 594 16 595 605 606 607 608 609 680 684 694 695	hoidmvlelem2	$⊢ (φ \land m \in ℕ \land G \leq (1 + E) \sum_{j = 1}^{m} P (j)) \to \exists u \in U S < u$
697	696	3exp	$⊢ φ \to (m \in ℕ \to (G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to \exists u \in U S < u))$
698	697	rexlimdv	$⊢ φ \to (\exists m \in ℕ G \leq (1 + E) \sum_{j = 1}^{m} P (j) \to \exists u \in U S < u)$
699	568 698	mpd	$⊢ φ \to \exists u \in U S < u$

Metamath Proof Explorer

Theorem hoidmvlelem3

Proof