stoweidlem57

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem57.1	$⊢ \underline{Ⅎ} t D$
	stoweidlem57.2	$⊢ \underline{Ⅎ} t U$
	stoweidlem57.3	$⊢ Ⅎ t φ$
	stoweidlem57.4	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
	stoweidlem57.5	$⊢ V = \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
	stoweidlem57.6	$⊢ K = topGen (ran (.))$
	stoweidlem57.7	$⊢ T = ⋃ J$
	stoweidlem57.8	$⊢ C = J Cn K$
	stoweidlem57.9	$⊢ U = T ∖ B$
	stoweidlem57.10	$⊢ φ \to J \in Comp$
	stoweidlem57.11	$⊢ φ \to A \subseteq C$
	stoweidlem57.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem57.13	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem57.14	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
	stoweidlem57.15	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem57.16	$⊢ φ \to B \in Clsd (J)$
	stoweidlem57.17	$⊢ φ \to D \in Clsd (J)$
	stoweidlem57.18	$⊢ φ \to B \cap D = \emptyset$
	stoweidlem57.19	$⊢ φ \to D \neq \emptyset$
	stoweidlem57.20	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem57.21	$⊢ φ \to E < \frac{1}{3}$
Assertion	stoweidlem57	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem57.1	$⊢ \underline{Ⅎ} t D$
2		stoweidlem57.2	$⊢ \underline{Ⅎ} t U$
3		stoweidlem57.3	$⊢ Ⅎ t φ$
4		stoweidlem57.4	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
5		stoweidlem57.5	$⊢ V = \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
6		stoweidlem57.6	$⊢ K = topGen (ran (.))$
7		stoweidlem57.7	$⊢ T = ⋃ J$
8		stoweidlem57.8	$⊢ C = J Cn K$
9		stoweidlem57.9	$⊢ U = T ∖ B$
10		stoweidlem57.10	$⊢ φ \to J \in Comp$
11		stoweidlem57.11	$⊢ φ \to A \subseteq C$
12		stoweidlem57.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
13		stoweidlem57.13	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
14		stoweidlem57.14	$⊢ (φ \land a \in ℝ) \to (t \in T ⟼ a) \in A$
15		stoweidlem57.15	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
16		stoweidlem57.16	$⊢ φ \to B \in Clsd (J)$
17		stoweidlem57.17	$⊢ φ \to D \in Clsd (J)$
18		stoweidlem57.18	$⊢ φ \to B \cap D = \emptyset$
19		stoweidlem57.19	$⊢ φ \to D \neq \emptyset$
20		stoweidlem57.20	$⊢ φ \to E \in ℝ^{+}$
21		stoweidlem57.21	$⊢ φ \to E < \frac{1}{3}$
22	1	nfcri	$⊢ Ⅎ t s \in D$
23	3 22	nfan	$⊢ Ⅎ t (φ \land s \in D)$
24	10	adantr	$⊢ (φ \land s \in D) \to J \in Comp$
25	11	adantr	$⊢ (φ \land s \in D) \to A \subseteq C$
26	12	3adant1r	$⊢ ((φ \land s \in D) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
27	13	3adant1r	$⊢ ((φ \land s \in D) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
28	14	adantlr	$⊢ ((φ \land s \in D) \land a \in ℝ) \to (t \in T ⟼ a) \in A$
29	15	adantlr	$⊢ ((φ \land s \in D) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
30		cmptop	$⊢ J \in Comp \to J \in Top$
31	7	iscld	$⊢ J \in Top \to (B \in Clsd (J) \leftrightarrow (B \subseteq T \land T ∖ B \in J))$
32	10 30 31	3syl	$⊢ φ \to (B \in Clsd (J) \leftrightarrow (B \subseteq T \land T ∖ B \in J))$
33	16 32	mpbid	$⊢ φ \to (B \subseteq T \land T ∖ B \in J)$
34	33	simprd	$⊢ φ \to T ∖ B \in J$
35	9 34	eqeltrid	$⊢ φ \to U \in J$
36	35	adantr	$⊢ (φ \land s \in D) \to U \in J$
37	7	cldss	$⊢ D \in Clsd (J) \to D \subseteq T$
38	17 37	syl	$⊢ φ \to D \subseteq T$
39	38	sselda	$⊢ (φ \land s \in D) \to s \in T$
40		disjr	$⊢ B \cap D = \emptyset \leftrightarrow \forall s \in D \neg s \in B$
41	18 40	sylib	$⊢ φ \to \forall s \in D \neg s \in B$
42	41	r19.21bi	$⊢ (φ \land s \in D) \to \neg s \in B$
43	39 42	eldifd	$⊢ (φ \land s \in D) \to s \in (T ∖ B)$
44	43 9	eleqtrrdi	$⊢ (φ \land s \in D) \to s \in U$
45	2 23 6 24 7 8 25 26 27 28 29 36 44	stoweidlem56	$⊢ (φ \land s \in D) \to \exists w \in J ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))$
46		simpl	$⊢ (w \in J \land ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))) \to w \in J$
47		simprll	$⊢ (w \in J \land ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))) \to s \in w$
48		simprr	$⊢ (w \in J \land ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))) \to \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
49	5	reqabi	$⊢ w \in V \leftrightarrow (w \in J \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))$
50	46 48 49	sylanbrc	$⊢ (w \in J \land ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))) \to w \in V$
51	46 47 50	jca32	$⊢ (w \in J \land ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t)))) \to (w \in J \land (s \in w \land w \in V))$
52	51	reximi2	$⊢ \exists w \in J ((s \in w \land w \subseteq U) \land \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))) \to \exists w \in J (s \in w \land w \in V)$
53		rexex	$⊢ \exists w \in J (s \in w \land w \in V) \to \exists w (s \in w \land w \in V)$
54	45 52 53	3syl	$⊢ (φ \land s \in D) \to \exists w (s \in w \land w \in V)$
55		nfcv	$⊢ \underline{Ⅎ} w s$
56		nfrab1	$⊢ \underline{Ⅎ} w \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
57	5 56	nfcxfr	$⊢ \underline{Ⅎ} w V$
58	55 57	elunif	$⊢ s \in ⋃ V \leftrightarrow \exists w (s \in w \land w \in V)$
59	54 58	sylibr	$⊢ (φ \land s \in D) \to s \in ⋃ V$
60	59	ex	$⊢ φ \to (s \in D \to s \in ⋃ V)$
61	60	ssrdv	$⊢ φ \to D \subseteq ⋃ V$
62		cmpcld	$⊢ (J \in Comp \land D \in Clsd (J)) \to J ↾_{𝑡} D \in Comp$
63	10 17 62	syl2anc	$⊢ φ \to J ↾_{𝑡} D \in Comp$
64	10 30	syl	$⊢ φ \to J \in Top$
65	7	cmpsub	$⊢ (J \in Top \land D \subseteq T) \to (J ↾_{𝑡} D \in Comp \leftrightarrow \forall k \in 𝒫 J (D \subseteq ⋃ k \to \exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u))$
66	64 38 65	syl2anc	$⊢ φ \to (J ↾_{𝑡} D \in Comp \leftrightarrow \forall k \in 𝒫 J (D \subseteq ⋃ k \to \exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u))$
67	63 66	mpbid	$⊢ φ \to \forall k \in 𝒫 J (D \subseteq ⋃ k \to \exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u)$
68		ssrab2	$⊢ \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\} \subseteq J$
69	5 68	eqsstri	$⊢ V \subseteq J$
70	5 10	rabexd	$⊢ φ \to V \in V$
71		elpwg	$⊢ V \in V \to (V \in 𝒫 J \leftrightarrow V \subseteq J)$
72	70 71	syl	$⊢ φ \to (V \in 𝒫 J \leftrightarrow V \subseteq J)$
73	69 72	mpbiri	$⊢ φ \to V \in 𝒫 J$
74		unieq	$⊢ k = V \to ⋃ k = ⋃ V$
75	74	sseq2d	$⊢ k = V \to (D \subseteq ⋃ k \leftrightarrow D \subseteq ⋃ V)$
76		pweq	$⊢ k = V \to 𝒫 k = 𝒫 V$
77	76	ineq1d	$⊢ k = V \to 𝒫 k \cap Fin = 𝒫 V \cap Fin$
78	77	rexeqdv	$⊢ k = V \to (\exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u \leftrightarrow \exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u)$
79	75 78	imbi12d	$⊢ k = V \to ((D \subseteq ⋃ k \to \exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u) \leftrightarrow (D \subseteq ⋃ V \to \exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u))$
80	79	rspccva	$⊢ (\forall k \in 𝒫 J (D \subseteq ⋃ k \to \exists u \in (𝒫 k \cap Fin) D \subseteq ⋃ u) \land V \in 𝒫 J) \to (D \subseteq ⋃ V \to \exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u)$
81	67 73 80	syl2anc	$⊢ φ \to (D \subseteq ⋃ V \to \exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u)$
82	61 81	mpd	$⊢ φ \to \exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u$
83		elinel1	$⊢ u \in (𝒫 V \cap Fin) \to u \in 𝒫 V$
84		elpwi	$⊢ u \in 𝒫 V \to u \subseteq V$
85	84	ssdifssd	$⊢ u \in 𝒫 V \to u ∖ \{\emptyset\} \subseteq V$
86		vex	$⊢ u \in V$
87		difexg	$⊢ u \in V \to u ∖ \{\emptyset\} \in V$
88	86 87	ax-mp	$⊢ u ∖ \{\emptyset\} \in V$
89	88	elpw	$⊢ u ∖ \{\emptyset\} \in 𝒫 V \leftrightarrow u ∖ \{\emptyset\} \subseteq V$
90	85 89	sylibr	$⊢ u \in 𝒫 V \to u ∖ \{\emptyset\} \in 𝒫 V$
91	83 90	syl	$⊢ u \in (𝒫 V \cap Fin) \to u ∖ \{\emptyset\} \in 𝒫 V$
92		elinel2	$⊢ u \in (𝒫 V \cap Fin) \to u \in Fin$
93		diffi	$⊢ u \in Fin \to u ∖ \{\emptyset\} \in Fin$
94	92 93	syl	$⊢ u \in (𝒫 V \cap Fin) \to u ∖ \{\emptyset\} \in Fin$
95	91 94	elind	$⊢ u \in (𝒫 V \cap Fin) \to u ∖ \{\emptyset\} \in (𝒫 V \cap Fin)$
96	95	3ad2ant2	$⊢ (φ \land u \in (𝒫 V \cap Fin) \land D \subseteq ⋃ u) \to u ∖ \{\emptyset\} \in (𝒫 V \cap Fin)$
97		unidif0	$⊢ ⋃ (u ∖ \{\emptyset\}) = ⋃ u$
98	97	sseq2i	$⊢ D \subseteq ⋃ (u ∖ \{\emptyset\}) \leftrightarrow D \subseteq ⋃ u$
99	98	biimpri	$⊢ D \subseteq ⋃ u \to D \subseteq ⋃ (u ∖ \{\emptyset\})$
100	99	3ad2ant3	$⊢ (φ \land u \in (𝒫 V \cap Fin) \land D \subseteq ⋃ u) \to D \subseteq ⋃ (u ∖ \{\emptyset\})$
101		eldifsni	$⊢ w \in (u ∖ \{\emptyset\}) \to w \neq \emptyset$
102	101	rgen	$⊢ \forall w \in (u ∖ \{\emptyset\}) w \neq \emptyset$
103	102	a1i	$⊢ (φ \land u \in (𝒫 V \cap Fin) \land D \subseteq ⋃ u) \to \forall w \in (u ∖ \{\emptyset\}) w \neq \emptyset$
104		unieq	$⊢ r = u ∖ \{\emptyset\} \to ⋃ r = ⋃ (u ∖ \{\emptyset\})$
105	104	sseq2d	$⊢ r = u ∖ \{\emptyset\} \to (D \subseteq ⋃ r \leftrightarrow D \subseteq ⋃ (u ∖ \{\emptyset\}))$
106		raleq	$⊢ r = u ∖ \{\emptyset\} \to (\forall w \in r w \neq \emptyset \leftrightarrow \forall w \in (u ∖ \{\emptyset\}) w \neq \emptyset)$
107	105 106	anbi12d	$⊢ r = u ∖ \{\emptyset\} \to ((D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset) \leftrightarrow (D \subseteq ⋃ (u ∖ \{\emptyset\}) \land \forall w \in (u ∖ \{\emptyset\}) w \neq \emptyset))$
108	107	rspcev	$⊢ (u ∖ \{\emptyset\} \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ (u ∖ \{\emptyset\}) \land \forall w \in (u ∖ \{\emptyset\}) w \neq \emptyset)) \to \exists r \in (𝒫 V \cap Fin) (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
109	96 100 103 108	syl12anc	$⊢ (φ \land u \in (𝒫 V \cap Fin) \land D \subseteq ⋃ u) \to \exists r \in (𝒫 V \cap Fin) (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
110	109	rexlimdv3a	$⊢ φ \to (\exists u \in (𝒫 V \cap Fin) D \subseteq ⋃ u \to \exists r \in (𝒫 V \cap Fin) (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset))$
111	82 110	mpd	$⊢ φ \to \exists r \in (𝒫 V \cap Fin) (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
112		nfv	$⊢ Ⅎ h φ$
113		nfcv	$⊢ \underline{Ⅎ} h ℝ^{+}$
114		nfre1	$⊢ Ⅎ h \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
115	113 114	nfralw	$⊢ Ⅎ h \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
116		nfcv	$⊢ \underline{Ⅎ} h J$
117	115 116	nfrabw	$⊢ \underline{Ⅎ} h \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
118	5 117	nfcxfr	$⊢ \underline{Ⅎ} h V$
119	118	nfpw	$⊢ \underline{Ⅎ} h 𝒫 V$
120		nfcv	$⊢ \underline{Ⅎ} h Fin$
121	119 120	nfin	$⊢ \underline{Ⅎ} h (𝒫 V \cap Fin)$
122	121	nfcri	$⊢ Ⅎ h r \in (𝒫 V \cap Fin)$
123		nfv	$⊢ Ⅎ h (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
124	112 122 123	nf3an	$⊢ Ⅎ h (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset))$
125		nfcv	$⊢ \underline{Ⅎ} t ℝ^{+}$
126		nfcv	$⊢ \underline{Ⅎ} t A$
127		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq h (t) \land h (t) \leq 1)$
128		nfra1	$⊢ Ⅎ t \forall t \in w h (t) < e$
129		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) 1 - e < h (t)$
130	127 128 129	nf3an	$⊢ Ⅎ t (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
131	126 130	nfrexw	$⊢ Ⅎ t \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
132	125 131	nfralw	$⊢ Ⅎ t \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))$
133		nfcv	$⊢ \underline{Ⅎ} t J$
134	132 133	nfrabw	$⊢ \underline{Ⅎ} t \{w \in J \| \forall e \in ℝ^{+} \exists h \in A (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \land \forall t \in w h (t) < e \land \forall t \in (T ∖ U) 1 - e < h (t))\}$
135	5 134	nfcxfr	$⊢ \underline{Ⅎ} t V$
136	135	nfpw	$⊢ \underline{Ⅎ} t 𝒫 V$
137		nfcv	$⊢ \underline{Ⅎ} t Fin$
138	136 137	nfin	$⊢ \underline{Ⅎ} t (𝒫 V \cap Fin)$
139	138	nfcri	$⊢ Ⅎ t r \in (𝒫 V \cap Fin)$
140		nfcv	$⊢ \underline{Ⅎ} t ⋃ r$
141	1 140	nfss	$⊢ Ⅎ t D \subseteq ⋃ r$
142		nfv	$⊢ Ⅎ t \forall w \in r w \neq \emptyset$
143	141 142	nfan	$⊢ Ⅎ t (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
144	3 139 143	nf3an	$⊢ Ⅎ t (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset))$
145		nfv	$⊢ Ⅎ w φ$
146	57	nfpw	$⊢ \underline{Ⅎ} w 𝒫 V$
147		nfcv	$⊢ \underline{Ⅎ} w Fin$
148	146 147	nfin	$⊢ \underline{Ⅎ} w (𝒫 V \cap Fin)$
149	148	nfcri	$⊢ Ⅎ w r \in (𝒫 V \cap Fin)$
150		nfv	$⊢ Ⅎ w D \subseteq ⋃ r$
151		nfra1	$⊢ Ⅎ w \forall w \in r w \neq \emptyset$
152	150 151	nfan	$⊢ Ⅎ w (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)$
153	145 149 152	nf3an	$⊢ Ⅎ w (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset))$
154		simp2	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to r \in (𝒫 V \cap Fin)$
155		simp3l	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to D \subseteq ⋃ r$
156	19	3ad2ant1	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to D \neq \emptyset$
157	20	3ad2ant1	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to E \in ℝ^{+}$
158	33	simpld	$⊢ φ \to B \subseteq T$
159	158	3ad2ant1	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to B \subseteq T$
160	70	3ad2ant1	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to V \in V$
161		retop	$⊢ topGen (ran (.)) \in Top$
162	6 161	eqeltri	$⊢ K \in Top$
163		cnfex	$⊢ (J \in Top \land K \in Top) \to J Cn K \in V$
164	64 162 163	sylancl	$⊢ φ \to J Cn K \in V$
165	11 8	sseqtrdi	$⊢ φ \to A \subseteq J Cn K$
166	164 165	ssexd	$⊢ φ \to A \in V$
167	166	3ad2ant1	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to A \in V$
168	124 144 153 9 4 5 154 155 156 157 159 160 167	stoweidlem39	$⊢ (φ \land r \in (𝒫 V \cap Fin) \land (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset)) \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
169	168	rexlimdv3a	$⊢ φ \to (\exists r \in (𝒫 V \cap Fin) (D \subseteq ⋃ r \land \forall w \in r w \neq \emptyset) \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))))$
170	111 169	mpd	$⊢ φ \to \exists m \in ℕ \exists v (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
171		nfv	$⊢ Ⅎ i (φ \land m \in ℕ)$
172		nfv	$⊢ Ⅎ i v : (1 \dots m) ⟶ V$
173		nfv	$⊢ Ⅎ i D \subseteq ⋃ ran v$
174		nfv	$⊢ Ⅎ i y : (1 \dots m) ⟶ Y$
175		nfra1	$⊢ Ⅎ i \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))$
176	174 175	nfan	$⊢ Ⅎ i (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
177	176	nfex	$⊢ Ⅎ i \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
178	172 173 177	nf3an	$⊢ Ⅎ i (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
179	171 178	nfan	$⊢ Ⅎ i ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))))$
180		nfv	$⊢ Ⅎ t m \in ℕ$
181	3 180	nfan	$⊢ Ⅎ t (φ \land m \in ℕ)$
182		nfcv	$⊢ \underline{Ⅎ} t v$
183		nfcv	$⊢ \underline{Ⅎ} t (1 \dots m)$
184	182 183 135	nff	$⊢ Ⅎ t v : (1 \dots m) ⟶ V$
185		nfcv	$⊢ \underline{Ⅎ} t ⋃ ran v$
186	1 185	nfss	$⊢ Ⅎ t D \subseteq ⋃ ran v$
187		nfcv	$⊢ \underline{Ⅎ} t y$
188	127 126	nfrabw	$⊢ \underline{Ⅎ} t \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
189	4 188	nfcxfr	$⊢ \underline{Ⅎ} t Y$
190	187 183 189	nff	$⊢ Ⅎ t y : (1 \dots m) ⟶ Y$
191		nfra1	$⊢ Ⅎ t \forall t \in v (i) y (i) (t) < \frac{E}{m}$
192		nfra1	$⊢ Ⅎ t \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)$
193	191 192	nfan	$⊢ Ⅎ t (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))$
194	183 193	nfralw	$⊢ Ⅎ t \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))$
195	190 194	nfan	$⊢ Ⅎ t (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
196	195	nfex	$⊢ Ⅎ t \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
197	184 186 196	nf3an	$⊢ Ⅎ t (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
198	181 197	nfan	$⊢ Ⅎ t ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))))$
199		nfv	$⊢ Ⅎ y (φ \land m \in ℕ)$
200		nfv	$⊢ Ⅎ y v : (1 \dots m) ⟶ V$
201		nfv	$⊢ Ⅎ y D \subseteq ⋃ ran v$
202		nfe1	$⊢ Ⅎ y \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
203	200 201 202	nf3an	$⊢ Ⅎ y (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
204	199 203	nfan	$⊢ Ⅎ y ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))))$
205		nfv	$⊢ Ⅎ w (φ \land m \in ℕ)$
206		nfcv	$⊢ \underline{Ⅎ} w v$
207		nfcv	$⊢ \underline{Ⅎ} w (1 \dots m)$
208	206 207 57	nff	$⊢ Ⅎ w v : (1 \dots m) ⟶ V$
209		nfv	$⊢ Ⅎ w D \subseteq ⋃ ran v$
210		nfv	$⊢ Ⅎ w \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
211	208 209 210	nf3an	$⊢ Ⅎ w (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))$
212	205 211	nfan	$⊢ Ⅎ w ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))))$
213		eqid	$⊢ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
214		eqid	$⊢ (f \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}, g \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} ⟼ (t \in T ⟼ f (t) g (t))) = (f \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}, g \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} ⟼ (t \in T ⟼ f (t) g (t)))$
215		eqid	$⊢ (t \in T ⟼ (i \in (1 \dots m) ⟼ y (i) (t))) = (t \in T ⟼ (i \in (1 \dots m) ⟼ y (i) (t)))$
216		eqid	$⊢ (t \in T ⟼ seq 1 (\times (t \in T ⟼ (i \in (1 \dots m) ⟼ y (i) (t))) (t)) (m)) = (t \in T ⟼ seq 1 (\times (t \in T ⟼ (i \in (1 \dots m) ⟼ y (i) (t))) (t)) (m))$
217		simp1ll	$⊢ (((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \land f \in A \land g \in A) \to φ$
218	217 13	syld3an1	$⊢ (((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
219	11	sselda	$⊢ (φ \land f \in A) \to f \in C$
220	6 7 8 219	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
221	220	ad4ant14	$⊢ (((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \land f \in A) \to f : T ⟶ ℝ$
222		simplr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to m \in ℕ$
223		simpr1	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to v : (1 \dots m) ⟶ V$
224	7	cldss	$⊢ B \in Clsd (J) \to B \subseteq T$
225	16 224	syl	$⊢ φ \to B \subseteq T$
226	225	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to B \subseteq T$
227		simpr2	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to D \subseteq ⋃ ran v$
228	38	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to D \subseteq T$
229		feq3	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \to (y : (1 \dots m) ⟶ Y \leftrightarrow y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\})$
230	4 229	ax-mp	$⊢ y : (1 \dots m) ⟶ Y \leftrightarrow y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
231	230	biimpi	$⊢ y : (1 \dots m) ⟶ Y \to y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
232	231	anim1i	$⊢ (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))) \to (y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
233	232	eximi	$⊢ \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))) \to \exists y (y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
234	233	3ad2ant3	$⊢ (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))) \to \exists y (y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
235	234	adantl	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to \exists y (y : (1 \dots m) ⟶ \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))$
236	10	uniexd	$⊢ φ \to ⋃ J \in V$
237	7 236	eqeltrid	$⊢ φ \to T \in V$
238	237	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to T \in V$
239	20	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to E \in ℝ^{+}$
240	21	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to E < \frac{1}{3}$
241	179 198 204 212 7 213 214 215 216 5 218 221 222 223 226 227 228 235 238 239 240	stoweidlem54	$⊢ ((φ \land m \in ℕ) \land (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t))))) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$
242	241	ex	$⊢ (φ \land m \in ℕ) \to ((v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)))$
243	242	exlimdv	$⊢ (φ \land m \in ℕ) \to (\exists v (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)))$
244	243	rexlimdva	$⊢ φ \to (\exists m \in ℕ \exists v (v : (1 \dots m) ⟶ V \land D \subseteq ⋃ ran v \land \exists y (y : (1 \dots m) ⟶ Y \land \forall i \in (1 \dots m) (\forall t \in v (i) y (i) (t) < \frac{E}{m} \land \forall t \in B 1 - (\frac{E}{m}) < y (i) (t)))) \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t)))$
245	170 244	mpd	$⊢ φ \to \exists x \in A (\forall t \in T (0 \leq x (t) \land x (t) \leq 1) \land \forall t \in D x (t) < E \land \forall t \in B 1 - E < x (t))$

Metamath Proof Explorer

Theorem stoweidlem57

Proof