stoweidlem59

Description: This lemma proves that there exists a function x as in the proof in BrosowskiDeutsh p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - \epsilon / n on B_j. Here D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem59.1	$⊢ \underline{Ⅎ} t F$
	stoweidlem59.2	$⊢ Ⅎ t φ$
	stoweidlem59.3	$⊢ K = topGen (ran (.))$
	stoweidlem59.4	$⊢ T = ⋃ J$
	stoweidlem59.5	$⊢ C = J Cn K$
	stoweidlem59.6	$⊢ D = (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
	stoweidlem59.7	$⊢ B = (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
	stoweidlem59.8	$⊢ Y = \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
	stoweidlem59.9	$⊢ H = (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
	stoweidlem59.10	$⊢ φ \to J \in Comp$
	stoweidlem59.11	$⊢ φ \to A \subseteq C$
	stoweidlem59.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem59.13	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem59.14	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
	stoweidlem59.15	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem59.16	$⊢ φ \to F \in C$
	stoweidlem59.17	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem59.18	$⊢ φ \to E < \frac{1}{3}$
	stoweidlem59.19	$⊢ φ \to N \in ℕ$
Assertion	stoweidlem59	$⊢ φ \to \exists x (x : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem59.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem59.2	$⊢ Ⅎ t φ$
3		stoweidlem59.3	$⊢ K = topGen (ran (.))$
4		stoweidlem59.4	$⊢ T = ⋃ J$
5		stoweidlem59.5	$⊢ C = J Cn K$
6		stoweidlem59.6	$⊢ D = (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
7		stoweidlem59.7	$⊢ B = (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
8		stoweidlem59.8	$⊢ Y = \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
9		stoweidlem59.9	$⊢ H = (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
10		stoweidlem59.10	$⊢ φ \to J \in Comp$
11		stoweidlem59.11	$⊢ φ \to A \subseteq C$
12		stoweidlem59.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
13		stoweidlem59.13	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
14		stoweidlem59.14	$⊢ (φ \land y \in ℝ) \to (t \in T ⟼ y) \in A$
15		stoweidlem59.15	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
16		stoweidlem59.16	$⊢ φ \to F \in C$
17		stoweidlem59.17	$⊢ φ \to E \in ℝ^{+}$
18		stoweidlem59.18	$⊢ φ \to E < \frac{1}{3}$
19		stoweidlem59.19	$⊢ φ \to N \in ℕ$
20		nfrab1	$⊢ \underline{Ⅎ} y \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
21	8 20	nfcxfr	$⊢ \underline{Ⅎ} y Y$
22		nfcv	$⊢ \underline{Ⅎ} z Y$
23		nfv	$⊢ Ⅎ z (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))$
24		nfv	$⊢ Ⅎ y (\forall t \in D (j) z (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < z (t))$
25		fveq1	$⊢ y = z \to y (t) = z (t)$
26	25	breq1d	$⊢ y = z \to (y (t) < \frac{E}{N} \leftrightarrow z (t) < \frac{E}{N})$
27	26	ralbidv	$⊢ y = z \to (\forall t \in D (j) y (t) < \frac{E}{N} \leftrightarrow \forall t \in D (j) z (t) < \frac{E}{N})$
28	25	breq2d	$⊢ y = z \to (1 - (\frac{E}{N}) < y (t) \leftrightarrow 1 - (\frac{E}{N}) < z (t))$
29	28	ralbidv	$⊢ y = z \to (\forall t \in B (j) 1 - (\frac{E}{N}) < y (t) \leftrightarrow \forall t \in B (j) 1 - (\frac{E}{N}) < z (t))$
30	27 29	anbi12d	$⊢ y = z \to ((\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)) \leftrightarrow (\forall t \in D (j) z (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < z (t)))$
31	21 22 23 24 30	cbvrabw	$⊢ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} = \{z \in Y \| (\forall t \in D (j) z (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < z (t))\}$
32		ovexd	$⊢ φ \to J Cn K \in V$
33	11 5	sseqtrdi	$⊢ φ \to A \subseteq J Cn K$
34	32 33	ssexd	$⊢ φ \to A \in V$
35	8 34	rabexd	$⊢ φ \to Y \in V$
36	31 35	rabexd	$⊢ φ \to \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \in V$
37	36	ralrimivw	$⊢ φ \to \forall j \in (0 \dots N) \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \in V$
38	9	fnmpt	$⊢ \forall j \in (0 \dots N) \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \in V \to H Fn (0 \dots N)$
39	37 38	syl	$⊢ φ \to H Fn (0 \dots N)$
40		fzfi	$⊢ (0 \dots N) \in Fin$
41		fnfi	$⊢ (H Fn (0 \dots N) \land (0 \dots N) \in Fin) \to H \in Fin$
42	39 40 41	sylancl	$⊢ φ \to H \in Fin$
43		rnfi	$⊢ H \in Fin \to ran H \in Fin$
44	42 43	syl	$⊢ φ \to ran H \in Fin$
45		fnchoice	$⊢ ran H \in Fin \to \exists h (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))$
46	44 45	syl	$⊢ φ \to \exists h (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))$
47		simprl	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to h Fn ran H$
48		ovex	$⊢ (0 \dots N) \in V$
49	48	mptex	$⊢ (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}) \in V$
50	9 49	eqeltri	$⊢ H \in V$
51	50	rnex	$⊢ ran H \in V$
52		fnex	$⊢ (h Fn ran H \land ran H \in V) \to h \in V$
53	47 51 52	sylancl	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to h \in V$
54		coexg	$⊢ (h \in V \land H \in V) \to h \circ H \in V$
55	53 50 54	sylancl	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to h \circ H \in V$
56		dffn3	$⊢ h Fn ran H \leftrightarrow h : ran H ⟶ ran h$
57	47 56	sylib	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to h : ran H ⟶ ran h$
58		nfv	$⊢ Ⅎ w φ$
59		nfv	$⊢ Ⅎ w h Fn ran H$
60		nfra1	$⊢ Ⅎ w \forall w \in ran H (w \neq \emptyset \to h (w) \in w)$
61	59 60	nfan	$⊢ Ⅎ w (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))$
62	58 61	nfan	$⊢ Ⅎ w (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w)))$
63		simplrr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land w \in ran H) \to \forall w \in ran H (w \neq \emptyset \to h (w) \in w)$
64		simpr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land w \in ran H) \to w \in ran H$
65		fvelrnb	$⊢ H Fn (0 \dots N) \to (w \in ran H \leftrightarrow \exists a \in (0 \dots N) H (a) = w)$
66		nfv	$⊢ Ⅎ a H (j) = w$
67		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
68	9 67	nfcxfr	$⊢ \underline{Ⅎ} j H$
69		nfcv	$⊢ \underline{Ⅎ} j a$
70	68 69	nffv	$⊢ \underline{Ⅎ} j H (a)$
71		nfcv	$⊢ \underline{Ⅎ} j w$
72	70 71	nfeq	$⊢ Ⅎ j H (a) = w$
73		fveq2	$⊢ j = a \to H (j) = H (a)$
74	73	eqeq1d	$⊢ j = a \to (H (j) = w \leftrightarrow H (a) = w)$
75	66 72 74	cbvrexw	$⊢ \exists j \in (0 \dots N) H (j) = w \leftrightarrow \exists a \in (0 \dots N) H (a) = w$
76	65 75	bitr4di	$⊢ H Fn (0 \dots N) \to (w \in ran H \leftrightarrow \exists j \in (0 \dots N) H (j) = w)$
77	39 76	syl	$⊢ φ \to (w \in ran H \leftrightarrow \exists j \in (0 \dots N) H (j) = w)$
78	77	biimpa	$⊢ (φ \land w \in ran H) \to \exists j \in (0 \dots N) H (j) = w$
79		simp3	$⊢ (φ \land j \in (0 \dots N) \land H (j) = w) \to H (j) = w$
80		simpr	$⊢ (φ \land j \in (0 \dots N)) \to j \in (0 \dots N)$
81	36	adantr	$⊢ (φ \land j \in (0 \dots N)) \to \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \in V$
82	9	fvmpt2	$⊢ (j \in (0 \dots N) \land \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \in V) \to H (j) = \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
83	80 81 82	syl2anc	$⊢ (φ \land j \in (0 \dots N)) \to H (j) = \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
84		nfcv	$⊢ \underline{Ⅎ} t (0 \dots N)$
85		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
86	84 85	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\})$
87	6 86	nfcxfr	$⊢ \underline{Ⅎ} t D$
88		nfcv	$⊢ \underline{Ⅎ} t j$
89	87 88	nffv	$⊢ \underline{Ⅎ} t D (j)$
90		nfcv	$⊢ \underline{Ⅎ} t T$
91		nfrab1	$⊢ \underline{Ⅎ} t \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
92	84 91	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
93	7 92	nfcxfr	$⊢ \underline{Ⅎ} t B$
94	93 88	nffv	$⊢ \underline{Ⅎ} t B (j)$
95	90 94	nfdif	$⊢ \underline{Ⅎ} t (T ∖ B (j))$
96		nfv	$⊢ Ⅎ t j \in (0 \dots N)$
97	2 96	nfan	$⊢ Ⅎ t (φ \land j \in (0 \dots N))$
98	10	adantr	$⊢ (φ \land j \in (0 \dots N)) \to J \in Comp$
99	11	adantr	$⊢ (φ \land j \in (0 \dots N)) \to A \subseteq C$
100	12	3adant1r	$⊢ ((φ \land j \in (0 \dots N)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
101	13	3adant1r	$⊢ ((φ \land j \in (0 \dots N)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
102	14	adantlr	$⊢ ((φ \land j \in (0 \dots N)) \land y \in ℝ) \to (t \in T ⟼ y) \in A$
103	15	adantlr	$⊢ ((φ \land j \in (0 \dots N)) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
104	10	uniexd	$⊢ φ \to ⋃ J \in V$
105	4 104	eqeltrid	$⊢ φ \to T \in V$
106	105	adantr	$⊢ (φ \land j \in (0 \dots N)) \to T \in V$
107		rabexg	$⊢ T \in V \to \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \in V$
108	106 107	syl	$⊢ (φ \land j \in (0 \dots N)) \to \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \in V$
109	7	fvmpt2	$⊢ (j \in (0 \dots N) \land \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \in V) \to B (j) = \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
110	80 108 109	syl2anc	$⊢ (φ \land j \in (0 \dots N)) \to B (j) = \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
111		eqid	$⊢ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} = \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
112		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
113	112	zred	$⊢ j \in (0 \dots N) \to j \in ℝ$
114		3re	$⊢ 3 \in ℝ$
115		3ne0	$⊢ 3 \neq 0$
116	114 115	rereccli	$⊢ \frac{1}{3} \in ℝ$
117		readdcl	$⊢ (j \in ℝ \land \frac{1}{3} \in ℝ) \to j + (\frac{1}{3}) \in ℝ$
118	113 116 117	sylancl	$⊢ j \in (0 \dots N) \to j + (\frac{1}{3}) \in ℝ$
119	118	adantl	$⊢ (φ \land j \in (0 \dots N)) \to j + (\frac{1}{3}) \in ℝ$
120	17	rpred	$⊢ φ \to E \in ℝ$
121	120	adantr	$⊢ (φ \land j \in (0 \dots N)) \to E \in ℝ$
122	119 121	remulcld	$⊢ (φ \land j \in (0 \dots N)) \to (j + (\frac{1}{3})) E \in ℝ$
123	16 5	eleqtrdi	$⊢ φ \to F \in (J Cn K)$
124	123	adantr	$⊢ (φ \land j \in (0 \dots N)) \to F \in (J Cn K)$
125	1 3 4 111 122 124	rfcnpre3	$⊢ (φ \land j \in (0 \dots N)) \to \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \in Clsd (J)$
126	110 125	eqeltrd	$⊢ (φ \land j \in (0 \dots N)) \to B (j) \in Clsd (J)$
127		rabexg	$⊢ T \in V \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in V$
128	106 127	syl	$⊢ (φ \land j \in (0 \dots N)) \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in V$
129	6	fvmpt2	$⊢ (j \in (0 \dots N) \land \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in V) \to D (j) = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
130	80 128 129	syl2anc	$⊢ (φ \land j \in (0 \dots N)) \to D (j) = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
131		eqid	$⊢ \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
132		resubcl	$⊢ (j \in ℝ \land \frac{1}{3} \in ℝ) \to j - (\frac{1}{3}) \in ℝ$
133	113 116 132	sylancl	$⊢ j \in (0 \dots N) \to j - (\frac{1}{3}) \in ℝ$
134	133	adantl	$⊢ (φ \land j \in (0 \dots N)) \to j - (\frac{1}{3}) \in ℝ$
135	134 121	remulcld	$⊢ (φ \land j \in (0 \dots N)) \to (j - (\frac{1}{3})) E \in ℝ$
136	1 3 4 131 135 124	rfcnpre4	$⊢ (φ \land j \in (0 \dots N)) \to \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \in Clsd (J)$
137	130 136	eqeltrd	$⊢ (φ \land j \in (0 \dots N)) \to D (j) \in Clsd (J)$
138	135	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (j - (\frac{1}{3})) E \in ℝ$
139	122	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (j + (\frac{1}{3})) E \in ℝ$
140	3 4 5 16	fcnre	$⊢ φ \to F : T ⟶ ℝ$
141	140	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to F : T ⟶ ℝ$
142		ssrab2	$⊢ \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \subseteq T$
143	110 142	eqsstrdi	$⊢ (φ \land j \in (0 \dots N)) \to B (j) \subseteq T$
144	143	sselda	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to t \in T$
145	141 144	ffvelcdmd	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to F (t) \in ℝ$
146	116 132	mpan2	$⊢ j \in ℝ \to j - (\frac{1}{3}) \in ℝ$
147		id	$⊢ j \in ℝ \to j \in ℝ$
148	116 117	mpan2	$⊢ j \in ℝ \to j + (\frac{1}{3}) \in ℝ$
149		3pos	$⊢ 0 < 3$
150	114 149	recgt0ii	$⊢ 0 < \frac{1}{3}$
151	116 150	elrpii	$⊢ \frac{1}{3} \in ℝ^{+}$
152		ltsubrp	$⊢ (j \in ℝ \land \frac{1}{3} \in ℝ^{+}) \to j - (\frac{1}{3}) < j$
153	151 152	mpan2	$⊢ j \in ℝ \to j - (\frac{1}{3}) < j$
154		ltaddrp	$⊢ (j \in ℝ \land \frac{1}{3} \in ℝ^{+}) \to j < j + (\frac{1}{3})$
155	151 154	mpan2	$⊢ j \in ℝ \to j < j + (\frac{1}{3})$
156	146 147 148 153 155	lttrd	$⊢ j \in ℝ \to j - (\frac{1}{3}) < j + (\frac{1}{3})$
157	113 156	syl	$⊢ j \in (0 \dots N) \to j - (\frac{1}{3}) < j + (\frac{1}{3})$
158	157	adantl	$⊢ (φ \land j \in (0 \dots N)) \to j - (\frac{1}{3}) < j + (\frac{1}{3})$
159	17	rpregt0d	$⊢ φ \to (E \in ℝ \land 0 < E)$
160	159	adantr	$⊢ (φ \land j \in (0 \dots N)) \to (E \in ℝ \land 0 < E)$
161		ltmul1	$⊢ (j - (\frac{1}{3}) \in ℝ \land j + (\frac{1}{3}) \in ℝ \land (E \in ℝ \land 0 < E)) \to (j - (\frac{1}{3}) < j + (\frac{1}{3}) \leftrightarrow (j - (\frac{1}{3})) E < (j + (\frac{1}{3})) E)$
162	134 119 160 161	syl3anc	$⊢ (φ \land j \in (0 \dots N)) \to (j - (\frac{1}{3}) < j + (\frac{1}{3}) \leftrightarrow (j - (\frac{1}{3})) E < (j + (\frac{1}{3})) E)$
163	158 162	mpbid	$⊢ (φ \land j \in (0 \dots N)) \to (j - (\frac{1}{3})) E < (j + (\frac{1}{3})) E$
164	163	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (j - (\frac{1}{3})) E < (j + (\frac{1}{3})) E$
165	110	eleq2d	$⊢ (φ \land j \in (0 \dots N)) \to (t \in B (j) \leftrightarrow t \in \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\})$
166	165	biimpa	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to t \in \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\}$
167		rabid	$⊢ t \in \{t \in T \| (j + (\frac{1}{3})) E \leq F (t)\} \leftrightarrow (t \in T \land (j + (\frac{1}{3})) E \leq F (t))$
168	166 167	sylib	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (t \in T \land (j + (\frac{1}{3})) E \leq F (t))$
169	168	simprd	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (j + (\frac{1}{3})) E \leq F (t)$
170	138 139 145 164 169	ltletrd	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to (j - (\frac{1}{3})) E < F (t)$
171	138 145	ltnled	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to ((j - (\frac{1}{3})) E < F (t) \leftrightarrow \neg F (t) \leq (j - (\frac{1}{3})) E)$
172	170 171	mpbid	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to \neg F (t) \leq (j - (\frac{1}{3})) E$
173	172	intnand	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to \neg (t \in T \land F (t) \leq (j - (\frac{1}{3})) E)$
174		rabid	$⊢ t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\} \leftrightarrow (t \in T \land F (t) \leq (j - (\frac{1}{3})) E)$
175	173 174	sylnibr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to \neg t \in \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
176	130	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to D (j) = \{t \in T \| F (t) \leq (j - (\frac{1}{3})) E\}$
177	175 176	neleqtrrd	$⊢ ((φ \land j \in (0 \dots N)) \land t \in B (j)) \to \neg t \in D (j)$
178	177	ex	$⊢ (φ \land j \in (0 \dots N)) \to (t \in B (j) \to \neg t \in D (j))$
179	97 178	ralrimi	$⊢ (φ \land j \in (0 \dots N)) \to \forall t \in B (j) \neg t \in D (j)$
180		disj	$⊢ B (j) \cap D (j) = \emptyset \leftrightarrow \forall a \in B (j) \neg a \in D (j)$
181		nfcv	$⊢ \underline{Ⅎ} a B (j)$
182	89	nfcri	$⊢ Ⅎ t a \in D (j)$
183	182	nfn	$⊢ Ⅎ t \neg a \in D (j)$
184		nfv	$⊢ Ⅎ a \neg t \in D (j)$
185		eleq1	$⊢ a = t \to (a \in D (j) \leftrightarrow t \in D (j))$
186	185	notbid	$⊢ a = t \to (\neg a \in D (j) \leftrightarrow \neg t \in D (j))$
187	181 94 183 184 186	cbvralfw	$⊢ \forall a \in B (j) \neg a \in D (j) \leftrightarrow \forall t \in B (j) \neg t \in D (j)$
188	180 187	bitri	$⊢ B (j) \cap D (j) = \emptyset \leftrightarrow \forall t \in B (j) \neg t \in D (j)$
189	179 188	sylibr	$⊢ (φ \land j \in (0 \dots N)) \to B (j) \cap D (j) = \emptyset$
190		eqid	$⊢ T ∖ B (j) = T ∖ B (j)$
191	19	nnrpd	$⊢ φ \to N \in ℝ^{+}$
192	17 191	rpdivcld	$⊢ φ \to \frac{E}{N} \in ℝ^{+}$
193	192	adantr	$⊢ (φ \land j \in (0 \dots N)) \to \frac{E}{N} \in ℝ^{+}$
194	120 19	nndivred	$⊢ φ \to \frac{E}{N} \in ℝ$
195	116	a1i	$⊢ φ \to \frac{1}{3} \in ℝ$
196	19	nnge1d	$⊢ φ \to 1 \leq N$
197		1re	$⊢ 1 \in ℝ$
198		0lt1	$⊢ 0 < 1$
199	197 198	pm3.2i	$⊢ (1 \in ℝ \land 0 < 1)$
200	199	a1i	$⊢ φ \to (1 \in ℝ \land 0 < 1)$
201	19	nnred	$⊢ φ \to N \in ℝ$
202	19	nngt0d	$⊢ φ \to 0 < N$
203		lediv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (N \in ℝ \land 0 < N) \land (E \in ℝ \land 0 < E)) \to (1 \leq N \leftrightarrow \frac{E}{N} \leq \frac{E}{1})$
204	200 201 202 159 203	syl121anc	$⊢ φ \to (1 \leq N \leftrightarrow \frac{E}{N} \leq \frac{E}{1})$
205	196 204	mpbid	$⊢ φ \to \frac{E}{N} \leq \frac{E}{1}$
206	17	rpcnd	$⊢ φ \to E \in ℂ$
207	206	div1d	$⊢ φ \to \frac{E}{1} = E$
208	205 207	breqtrd	$⊢ φ \to \frac{E}{N} \leq E$
209	194 120 195 208 18	lelttrd	$⊢ φ \to \frac{E}{N} < \frac{1}{3}$
210	209	adantr	$⊢ (φ \land j \in (0 \dots N)) \to \frac{E}{N} < \frac{1}{3}$
211	89 95 97 3 4 5 98 99 100 101 102 103 126 137 189 190 193 210	stoweidlem58	$⊢ (φ \land j \in (0 \dots N)) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))$
212		df-rex	$⊢ \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)) \leftrightarrow \exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))$
213	211 212	sylib	$⊢ (φ \land j \in (0 \dots N)) \to \exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))$
214		simprl	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to x \in A$
215		simprr1	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to \forall t \in T (0 \leq x (t) \land x (t) \leq 1)$
216		fveq1	$⊢ y = x \to y (t) = x (t)$
217	216	breq2d	$⊢ y = x \to (0 \leq y (t) \leftrightarrow 0 \leq x (t))$
218	216	breq1d	$⊢ y = x \to (y (t) \leq 1 \leftrightarrow x (t) \leq 1)$
219	217 218	anbi12d	$⊢ y = x \to ((0 \leq y (t) \land y (t) \leq 1) \leftrightarrow (0 \leq x (t) \land x (t) \leq 1))$
220	219	ralbidv	$⊢ y = x \to (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq x (t) \land x (t) \leq 1))$
221	220 8	elrab2	$⊢ x \in Y \leftrightarrow (x \in A \land \forall t \in T (0 \leq x (t) \land x (t) \leq 1))$
222	214 215 221	sylanbrc	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to x \in Y$
223		simprr2	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to \forall t \in D (j) x (t) < \frac{E}{N}$
224		simprr3	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)$
225	223 224	jca	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to (\forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))$
226		nfcv	$⊢ \underline{Ⅎ} y x$
227		nfv	$⊢ Ⅎ y (\forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))$
228	216	breq1d	$⊢ y = x \to (y (t) < \frac{E}{N} \leftrightarrow x (t) < \frac{E}{N})$
229	228	ralbidv	$⊢ y = x \to (\forall t \in D (j) y (t) < \frac{E}{N} \leftrightarrow \forall t \in D (j) x (t) < \frac{E}{N})$
230	216	breq2d	$⊢ y = x \to (1 - (\frac{E}{N}) < y (t) \leftrightarrow 1 - (\frac{E}{N}) < x (t))$
231	230	ralbidv	$⊢ y = x \to (\forall t \in B (j) 1 - (\frac{E}{N}) < y (t) \leftrightarrow \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))$
232	229 231	anbi12d	$⊢ y = x \to ((\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)) \leftrightarrow (\forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))$
233	226 21 227 232	elrabf	$⊢ x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \leftrightarrow (x \in Y \land (\forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))$
234	222 225 233	sylanbrc	$⊢ ((φ \land j \in (0 \dots N)) \land (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t)))) \to x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
235	234	ex	$⊢ (φ \land j \in (0 \dots N)) \to ((x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))) \to x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
236	235	eximdv	$⊢ (φ \land j \in (0 \dots N)) \to (\exists x (x \in A \land (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D (j) x (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (t))) \to \exists x x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
237	213 236	mpd	$⊢ (φ \land j \in (0 \dots N)) \to \exists x x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
238		ne0i	$⊢ x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \to \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \neq \emptyset$
239	238	exlimiv	$⊢ \exists x x \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \to \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \neq \emptyset$
240	237 239	syl	$⊢ (φ \land j \in (0 \dots N)) \to \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \neq \emptyset$
241	83 240	eqnetrd	$⊢ (φ \land j \in (0 \dots N)) \to H (j) \neq \emptyset$
242	241	3adant3	$⊢ (φ \land j \in (0 \dots N) \land H (j) = w) \to H (j) \neq \emptyset$
243	79 242	eqnetrrd	$⊢ (φ \land j \in (0 \dots N) \land H (j) = w) \to w \neq \emptyset$
244	243	3exp	$⊢ φ \to (j \in (0 \dots N) \to (H (j) = w \to w \neq \emptyset))$
245	244	rexlimdv	$⊢ φ \to (\exists j \in (0 \dots N) H (j) = w \to w \neq \emptyset)$
246	245	adantr	$⊢ (φ \land w \in ran H) \to (\exists j \in (0 \dots N) H (j) = w \to w \neq \emptyset)$
247	78 246	mpd	$⊢ (φ \land w \in ran H) \to w \neq \emptyset$
248	247	adantlr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land w \in ran H) \to w \neq \emptyset$
249		rsp	$⊢ \forall w \in ran H (w \neq \emptyset \to h (w) \in w) \to (w \in ran H \to (w \neq \emptyset \to h (w) \in w))$
250	63 64 248 249	syl3c	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land w \in ran H) \to h (w) \in w$
251	250	ex	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to (w \in ran H \to h (w) \in w)$
252	62 251	ralrimi	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to \forall w \in ran H h (w) \in w$
253		chfnrn	$⊢ (h Fn ran H \land \forall w \in ran H h (w) \in w) \to ran h \subseteq ⋃ ran H$
254	47 252 253	syl2anc	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to ran h \subseteq ⋃ ran H$
255		nfv	$⊢ Ⅎ y φ$
256		nfcv	$⊢ \underline{Ⅎ} y h$
257		nfcv	$⊢ \underline{Ⅎ} y (0 \dots N)$
258		nfrab1	$⊢ \underline{Ⅎ} y \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
259	257 258	nfmpt	$⊢ \underline{Ⅎ} y (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
260	9 259	nfcxfr	$⊢ \underline{Ⅎ} y H$
261	260	nfrn	$⊢ \underline{Ⅎ} y ran H$
262	256 261	nffn	$⊢ Ⅎ y h Fn ran H$
263		nfv	$⊢ Ⅎ y (w \neq \emptyset \to h (w) \in w)$
264	261 263	nfralw	$⊢ Ⅎ y \forall w \in ran H (w \neq \emptyset \to h (w) \in w)$
265	262 264	nfan	$⊢ Ⅎ y (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))$
266	255 265	nfan	$⊢ Ⅎ y (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w)))$
267	261	nfuni	$⊢ \underline{Ⅎ} y ⋃ ran H$
268		fnunirn	$⊢ H Fn (0 \dots N) \to (y \in ⋃ ran H \leftrightarrow \exists z \in (0 \dots N) y \in H (z))$
269		nfcv	$⊢ \underline{Ⅎ} j z$
270	68 269	nffv	$⊢ \underline{Ⅎ} j H (z)$
271	270	nfcri	$⊢ Ⅎ j y \in H (z)$
272		nfv	$⊢ Ⅎ z y \in H (j)$
273		fveq2	$⊢ z = j \to H (z) = H (j)$
274	273	eleq2d	$⊢ z = j \to (y \in H (z) \leftrightarrow y \in H (j))$
275	271 272 274	cbvrexw	$⊢ \exists z \in (0 \dots N) y \in H (z) \leftrightarrow \exists j \in (0 \dots N) y \in H (j)$
276	268 275	bitrdi	$⊢ H Fn (0 \dots N) \to (y \in ⋃ ran H \leftrightarrow \exists j \in (0 \dots N) y \in H (j))$
277	39 276	syl	$⊢ φ \to (y \in ⋃ ran H \leftrightarrow \exists j \in (0 \dots N) y \in H (j))$
278	277	biimpa	$⊢ (φ \land y \in ⋃ ran H) \to \exists j \in (0 \dots N) y \in H (j)$
279		nfv	$⊢ Ⅎ j φ$
280	68	nfrn	$⊢ \underline{Ⅎ} j ran H$
281	280	nfuni	$⊢ \underline{Ⅎ} j ⋃ ran H$
282	281	nfcri	$⊢ Ⅎ j y \in ⋃ ran H$
283	279 282	nfan	$⊢ Ⅎ j (φ \land y \in ⋃ ran H)$
284		nfv	$⊢ Ⅎ j y \in Y$
285		simp1l	$⊢ ((φ \land y \in ⋃ ran H) \land j \in (0 \dots N) \land y \in H (j)) \to φ$
286		simp2	$⊢ ((φ \land y \in ⋃ ran H) \land j \in (0 \dots N) \land y \in H (j)) \to j \in (0 \dots N)$
287		simp3	$⊢ ((φ \land y \in ⋃ ran H) \land j \in (0 \dots N) \land y \in H (j)) \to y \in H (j)$
288	83	eleq2d	$⊢ (φ \land j \in (0 \dots N)) \to (y \in H (j) \leftrightarrow y \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
289	288	biimpa	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to y \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
290		rabid	$⊢ y \in \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\} \leftrightarrow (y \in Y \land (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)))$
291	289 290	sylib	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to (y \in Y \land (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)))$
292	291	simpld	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to y \in Y$
293	285 286 287 292	syl21anc	$⊢ ((φ \land y \in ⋃ ran H) \land j \in (0 \dots N) \land y \in H (j)) \to y \in Y$
294	293	3exp	$⊢ (φ \land y \in ⋃ ran H) \to (j \in (0 \dots N) \to (y \in H (j) \to y \in Y))$
295	283 284 294	rexlimd	$⊢ (φ \land y \in ⋃ ran H) \to (\exists j \in (0 \dots N) y \in H (j) \to y \in Y)$
296	278 295	mpd	$⊢ (φ \land y \in ⋃ ran H) \to y \in Y$
297	296	adantlr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land y \in ⋃ ran H) \to y \in Y$
298	297	ex	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to (y \in ⋃ ran H \to y \in Y)$
299	266 267 21 298	ssrd	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to ⋃ ran H \subseteq Y$
300		ssrab2	$⊢ \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\} \subseteq A$
301	8 300	eqsstri	$⊢ Y \subseteq A$
302	299 301	sstrdi	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to ⋃ ran H \subseteq A$
303	254 302	sstrd	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to ran h \subseteq A$
304	57 303	fssd	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to h : ran H ⟶ A$
305		dffn3	$⊢ H Fn (0 \dots N) \leftrightarrow H : (0 \dots N) ⟶ ran H$
306	39 305	sylib	$⊢ φ \to H : (0 \dots N) ⟶ ran H$
307	306	adantr	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to H : (0 \dots N) ⟶ ran H$
308		fco	$⊢ (h : ran H ⟶ A \land H : (0 \dots N) ⟶ ran H) \to (h \circ H) : (0 \dots N) ⟶ A$
309	304 307 308	syl2anc	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to (h \circ H) : (0 \dots N) ⟶ A$
310		nfcv	$⊢ \underline{Ⅎ} j h$
311	310 280	nffn	$⊢ Ⅎ j h Fn ran H$
312		nfv	$⊢ Ⅎ j (w \neq \emptyset \to h (w) \in w)$
313	280 312	nfralw	$⊢ Ⅎ j \forall w \in ran H (w \neq \emptyset \to h (w) \in w)$
314	311 313	nfan	$⊢ Ⅎ j (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))$
315	279 314	nfan	$⊢ Ⅎ j (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w)))$
316		simpll	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to φ$
317		simpr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to j \in (0 \dots N)$
318	39	ad2antrr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to H Fn (0 \dots N)$
319		fvco2	$⊢ (H Fn (0 \dots N) \land j \in (0 \dots N)) \to (h \circ H) (j) = h (H (j))$
320	318 319	sylancom	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to (h \circ H) (j) = h (H (j))$
321		simplrr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to \forall w \in ran H (w \neq \emptyset \to h (w) \in w)$
322		fnfun	$⊢ H Fn (0 \dots N) \to Fun H$
323	39 322	syl	$⊢ φ \to Fun H$
324	323	ad2antrr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to Fun H$
325	39	fndmd	$⊢ φ \to dom H = (0 \dots N)$
326	325	adantr	$⊢ (φ \land j \in (0 \dots N)) \to dom H = (0 \dots N)$
327	80 326	eleqtrrd	$⊢ (φ \land j \in (0 \dots N)) \to j \in dom H$
328	327	adantlr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to j \in dom H$
329		fvelrn	$⊢ (Fun H \land j \in dom H) \to H (j) \in ran H$
330	324 328 329	syl2anc	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to H (j) \in ran H$
331	321 330	jca	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to (\forall w \in ran H (w \neq \emptyset \to h (w) \in w) \land H (j) \in ran H)$
332	241	adantlr	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to H (j) \neq \emptyset$
333		neeq1	$⊢ w = H (j) \to (w \neq \emptyset \leftrightarrow H (j) \neq \emptyset)$
334		fveq2	$⊢ w = H (j) \to h (w) = h (H (j))$
335		id	$⊢ w = H (j) \to w = H (j)$
336	334 335	eleq12d	$⊢ w = H (j) \to (h (w) \in w \leftrightarrow h (H (j)) \in H (j))$
337	333 336	imbi12d	$⊢ w = H (j) \to ((w \neq \emptyset \to h (w) \in w) \leftrightarrow (H (j) \neq \emptyset \to h (H (j)) \in H (j)))$
338	337	rspccva	$⊢ (\forall w \in ran H (w \neq \emptyset \to h (w) \in w) \land H (j) \in ran H) \to (H (j) \neq \emptyset \to h (H (j)) \in H (j))$
339	331 332 338	sylc	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to h (H (j)) \in H (j)$
340	320 339	eqeltrd	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to (h \circ H) (j) \in H (j)$
341	256 260	nfco	$⊢ \underline{Ⅎ} y (h \circ H)$
342		nfcv	$⊢ \underline{Ⅎ} y j$
343	341 342	nffv	$⊢ \underline{Ⅎ} y (h \circ H) (j)$
344		nfv	$⊢ Ⅎ y (φ \land j \in (0 \dots N))$
345	260 342	nffv	$⊢ \underline{Ⅎ} y H (j)$
346	343 345	nfel	$⊢ Ⅎ y (h \circ H) (j) \in H (j)$
347	344 346	nfan	$⊢ Ⅎ y ((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j))$
348	343 21	nfel	$⊢ Ⅎ y (h \circ H) (j) \in Y$
349	347 348	nfim	$⊢ Ⅎ y (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to (h \circ H) (j) \in Y)$
350		eleq1	$⊢ y = (h \circ H) (j) \to (y \in H (j) \leftrightarrow (h \circ H) (j) \in H (j))$
351	350	anbi2d	$⊢ y = (h \circ H) (j) \to (((φ \land j \in (0 \dots N)) \land y \in H (j)) \leftrightarrow ((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)))$
352		eleq1	$⊢ y = (h \circ H) (j) \to (y \in Y \leftrightarrow (h \circ H) (j) \in Y)$
353	351 352	imbi12d	$⊢ y = (h \circ H) (j) \to ((((φ \land j \in (0 \dots N)) \land y \in H (j)) \to y \in Y) \leftrightarrow (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to (h \circ H) (j) \in Y))$
354	343 349 353 292	vtoclgf	$⊢ (h \circ H) (j) \in H (j) \to (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to (h \circ H) (j) \in Y)$
355	354	anabsi7	$⊢ ((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to (h \circ H) (j) \in Y$
356	316 317 340 355	syl21anc	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to (h \circ H) (j) \in Y$
357	8	eleq2i	$⊢ (h \circ H) (j) \in Y \leftrightarrow (h \circ H) (j) \in \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
358		nfcv	$⊢ \underline{Ⅎ} y A$
359		nfcv	$⊢ \underline{Ⅎ} y T$
360		nfcv	$⊢ \underline{Ⅎ} y 0$
361		nfcv	$⊢ \underline{Ⅎ} y \leq$
362		nfcv	$⊢ \underline{Ⅎ} y t$
363	343 362	nffv	$⊢ \underline{Ⅎ} y (h \circ H) (j) (t)$
364	360 361 363	nfbr	$⊢ Ⅎ y 0 \leq (h \circ H) (j) (t)$
365		nfcv	$⊢ \underline{Ⅎ} y 1$
366	363 361 365	nfbr	$⊢ Ⅎ y (h \circ H) (j) (t) \leq 1$
367	364 366	nfan	$⊢ Ⅎ y (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1)$
368	359 367	nfralw	$⊢ Ⅎ y \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1)$
369		nfcv	$⊢ \underline{Ⅎ} t y$
370		nfcv	$⊢ \underline{Ⅎ} t h$
371		nfra1	$⊢ Ⅎ t \forall t \in D (j) y (t) < \frac{E}{N}$
372		nfra1	$⊢ Ⅎ t \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)$
373	371 372	nfan	$⊢ Ⅎ t (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))$
374		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq y (t) \land y (t) \leq 1)$
375		nfcv	$⊢ \underline{Ⅎ} t A$
376	374 375	nfrabw	$⊢ \underline{Ⅎ} t \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\}$
377	8 376	nfcxfr	$⊢ \underline{Ⅎ} t Y$
378	373 377	nfrabw	$⊢ \underline{Ⅎ} t \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\}$
379	84 378	nfmpt	$⊢ \underline{Ⅎ} t (j \in (0 \dots N) ⟼ \{y \in Y \| (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))\})$
380	9 379	nfcxfr	$⊢ \underline{Ⅎ} t H$
381	370 380	nfco	$⊢ \underline{Ⅎ} t (h \circ H)$
382	381 88	nffv	$⊢ \underline{Ⅎ} t (h \circ H) (j)$
383	369 382	nfeq	$⊢ Ⅎ t y = (h \circ H) (j)$
384		fveq1	$⊢ y = (h \circ H) (j) \to y (t) = (h \circ H) (j) (t)$
385	384	breq2d	$⊢ y = (h \circ H) (j) \to (0 \leq y (t) \leftrightarrow 0 \leq (h \circ H) (j) (t))$
386	384	breq1d	$⊢ y = (h \circ H) (j) \to (y (t) \leq 1 \leftrightarrow (h \circ H) (j) (t) \leq 1)$
387	385 386	anbi12d	$⊢ y = (h \circ H) (j) \to ((0 \leq y (t) \land y (t) \leq 1) \leftrightarrow (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
388	383 387	ralbid	$⊢ y = (h \circ H) (j) \to (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
389	343 358 368 388	elrabf	$⊢ (h \circ H) (j) \in \{y \in A \| \forall t \in T (0 \leq y (t) \land y (t) \leq 1)\} \leftrightarrow ((h \circ H) (j) \in A \land \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
390	357 389	bitri	$⊢ (h \circ H) (j) \in Y \leftrightarrow ((h \circ H) (j) \in A \land \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
391	356 390	sylib	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to ((h \circ H) (j) \in A \land \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
392	391	simprd	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1)$
393		nfcv	$⊢ \underline{Ⅎ} y D (j)$
394		nfcv	$⊢ \underline{Ⅎ} y <$
395		nfcv	$⊢ \underline{Ⅎ} y (\frac{E}{N})$
396	363 394 395	nfbr	$⊢ Ⅎ y (h \circ H) (j) (t) < \frac{E}{N}$
397	393 396	nfralw	$⊢ Ⅎ y \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N}$
398	347 397	nfim	$⊢ Ⅎ y (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N})$
399	384	breq1d	$⊢ y = (h \circ H) (j) \to (y (t) < \frac{E}{N} \leftrightarrow (h \circ H) (j) (t) < \frac{E}{N})$
400	383 399	ralbid	$⊢ y = (h \circ H) (j) \to (\forall t \in D (j) y (t) < \frac{E}{N} \leftrightarrow \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N})$
401	351 400	imbi12d	$⊢ y = (h \circ H) (j) \to ((((φ \land j \in (0 \dots N)) \land y \in H (j)) \to \forall t \in D (j) y (t) < \frac{E}{N}) \leftrightarrow (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N}))$
402	291	simprd	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to (\forall t \in D (j) y (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < y (t))$
403	402	simpld	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to \forall t \in D (j) y (t) < \frac{E}{N}$
404	343 398 401 403	vtoclgf	$⊢ (h \circ H) (j) \in H (j) \to (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N})$
405	404	anabsi7	$⊢ ((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N}$
406	316 317 340 405	syl21anc	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N}$
407		nfcv	$⊢ \underline{Ⅎ} y B (j)$
408		nfcv	$⊢ \underline{Ⅎ} y (1 - (\frac{E}{N}))$
409	408 394 363	nfbr	$⊢ Ⅎ y 1 - (\frac{E}{N}) < (h \circ H) (j) (t)$
410	407 409	nfralw	$⊢ Ⅎ y \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)$
411	347 410	nfim	$⊢ Ⅎ y (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
412	384	breq2d	$⊢ y = (h \circ H) (j) \to (1 - (\frac{E}{N}) < y (t) \leftrightarrow 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
413	383 412	ralbid	$⊢ y = (h \circ H) (j) \to (\forall t \in B (j) 1 - (\frac{E}{N}) < y (t) \leftrightarrow \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
414	351 413	imbi12d	$⊢ y = (h \circ H) (j) \to ((((φ \land j \in (0 \dots N)) \land y \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)) \leftrightarrow (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)))$
415	402	simprd	$⊢ ((φ \land j \in (0 \dots N)) \land y \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < y (t)$
416	343 411 414 415	vtoclgf	$⊢ (h \circ H) (j) \in H (j) \to (((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
417	416	anabsi7	$⊢ ((φ \land j \in (0 \dots N)) \land (h \circ H) (j) \in H (j)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)$
418	316 317 340 417	syl21anc	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)$
419	392 406 418	3jca	$⊢ ((φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \land j \in (0 \dots N)) \to (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
420	419	ex	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to (j \in (0 \dots N) \to (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)))$
421	315 420	ralrimi	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to \forall j \in (0 \dots N) (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
422	309 421	jca	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to ((h \circ H) : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)))$
423		feq1	$⊢ x = h \circ H \to (x : (0 \dots N) ⟶ A \leftrightarrow (h \circ H) : (0 \dots N) ⟶ A)$
424		nfcv	$⊢ \underline{Ⅎ} j x$
425	310 68	nfco	$⊢ \underline{Ⅎ} j (h \circ H)$
426	424 425	nfeq	$⊢ Ⅎ j x = h \circ H$
427		nfcv	$⊢ \underline{Ⅎ} t x$
428	427 381	nfeq	$⊢ Ⅎ t x = h \circ H$
429		fveq1	$⊢ x = h \circ H \to x (j) = (h \circ H) (j)$
430	429	fveq1d	$⊢ x = h \circ H \to x (j) (t) = (h \circ H) (j) (t)$
431	430	breq2d	$⊢ x = h \circ H \to (0 \leq x (j) (t) \leftrightarrow 0 \leq (h \circ H) (j) (t))$
432	430	breq1d	$⊢ x = h \circ H \to (x (j) (t) \leq 1 \leftrightarrow (h \circ H) (j) (t) \leq 1)$
433	431 432	anbi12d	$⊢ x = h \circ H \to ((0 \leq x (j) (t) \land x (j) (t) \leq 1) \leftrightarrow (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
434	428 433	ralbid	$⊢ x = h \circ H \to (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1))$
435	430	breq1d	$⊢ x = h \circ H \to (x (j) (t) < \frac{E}{N} \leftrightarrow (h \circ H) (j) (t) < \frac{E}{N})$
436	428 435	ralbid	$⊢ x = h \circ H \to (\forall t \in D (j) x (j) (t) < \frac{E}{N} \leftrightarrow \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N})$
437	430	breq2d	$⊢ x = h \circ H \to (1 - (\frac{E}{N}) < x (j) (t) \leftrightarrow 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
438	428 437	ralbid	$⊢ x = h \circ H \to (\forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t) \leftrightarrow \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))$
439	434 436 438	3anbi123d	$⊢ x = h \circ H \to ((\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t)) \leftrightarrow (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)))$
440	426 439	ralbid	$⊢ x = h \circ H \to (\forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t)) \leftrightarrow \forall j \in (0 \dots N) (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t)))$
441	423 440	anbi12d	$⊢ x = h \circ H \to ((x : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t))) \leftrightarrow ((h \circ H) : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))))$
442	441	spcegv	$⊢ h \circ H \in V \to (((h \circ H) : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq (h \circ H) (j) (t) \land (h \circ H) (j) (t) \leq 1) \land \forall t \in D (j) (h \circ H) (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < (h \circ H) (j) (t))) \to \exists x (x : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t))))$
443	55 422 442	sylc	$⊢ (φ \land (h Fn ran H \land \forall w \in ran H (w \neq \emptyset \to h (w) \in w))) \to \exists x (x : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t)))$
444	46 443	exlimddv	$⊢ φ \to \exists x (x : (0 \dots N) ⟶ A \land \forall j \in (0 \dots N) (\forall t \in T (0 \leq x (j) (t) \land x (j) (t) \leq 1) \land \forall t \in D (j) x (j) (t) < \frac{E}{N} \land \forall t \in B (j) 1 - (\frac{E}{N}) < x (j) (t)))$

Metamath Proof Explorer

Theorem stoweidlem59

Proof