stoweidlem28

Description: There exists a δ as in Lemma 1 BrosowskiDeutsh p. 90: 0 < delta < 1 and p >= delta on T \ U . Here d is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem28.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem28.2	$⊢ Ⅎ t φ$
	stoweidlem28.3	$⊢ K = topGen (ran (.))$
	stoweidlem28.4	$⊢ T = ⋃ J$
	stoweidlem28.5	$⊢ φ \to J \in Comp$
	stoweidlem28.6	$⊢ φ \to P \in (J Cn K)$
	stoweidlem28.7	$⊢ φ \to \forall t \in (T ∖ U) 0 < P (t)$
	stoweidlem28.8	$⊢ φ \to U \in J$
Assertion	stoweidlem28	$⊢ φ \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem28.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem28.2	$⊢ Ⅎ t φ$
3		stoweidlem28.3	$⊢ K = topGen (ran (.))$
4		stoweidlem28.4	$⊢ T = ⋃ J$
5		stoweidlem28.5	$⊢ φ \to J \in Comp$
6		stoweidlem28.6	$⊢ φ \to P \in (J Cn K)$
7		stoweidlem28.7	$⊢ φ \to \forall t \in (T ∖ U) 0 < P (t)$
8		stoweidlem28.8	$⊢ φ \to U \in J$
9		halfre	$⊢ \frac{1}{2} \in ℝ$
10		halfgt0	$⊢ 0 < \frac{1}{2}$
11	9 10	elrpii	$⊢ \frac{1}{2} \in ℝ^{+}$
12	11	a1i	$⊢ (φ \land T ∖ U = \emptyset) \to \frac{1}{2} \in ℝ^{+}$
13		halflt1	$⊢ \frac{1}{2} < 1$
14	13	a1i	$⊢ (φ \land T ∖ U = \emptyset) \to \frac{1}{2} < 1$
15		nfcv	$⊢ \underline{Ⅎ} t T$
16	15 1	nfdif	$⊢ \underline{Ⅎ} t (T ∖ U)$
17	16	nfeq1	$⊢ Ⅎ t T ∖ U = \emptyset$
18	17	rzalf	$⊢ T ∖ U = \emptyset \to \forall t \in (T ∖ U) \frac{1}{2} \leq P (t)$
19	18	adantl	$⊢ (φ \land T ∖ U = \emptyset) \to \forall t \in (T ∖ U) \frac{1}{2} \leq P (t)$
20		ovex	$⊢ \frac{1}{2} \in V$
21		eleq1	$⊢ d = \frac{1}{2} \to (d \in ℝ^{+} \leftrightarrow \frac{1}{2} \in ℝ^{+})$
22		breq1	$⊢ d = \frac{1}{2} \to (d < 1 \leftrightarrow \frac{1}{2} < 1)$
23		breq1	$⊢ d = \frac{1}{2} \to (d \leq P (t) \leftrightarrow \frac{1}{2} \leq P (t))$
24	23	ralbidv	$⊢ d = \frac{1}{2} \to (\forall t \in (T ∖ U) d \leq P (t) \leftrightarrow \forall t \in (T ∖ U) \frac{1}{2} \leq P (t))$
25	21 22 24	3anbi123d	$⊢ d = \frac{1}{2} \to ((d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t)) \leftrightarrow (\frac{1}{2} \in ℝ^{+} \land \frac{1}{2} < 1 \land \forall t \in (T ∖ U) \frac{1}{2} \leq P (t)))$
26	20 25	spcev	$⊢ (\frac{1}{2} \in ℝ^{+} \land \frac{1}{2} < 1 \land \forall t \in (T ∖ U) \frac{1}{2} \leq P (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
27	12 14 19 26	syl3anc	$⊢ (φ \land T ∖ U = \emptyset) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
28		simplll	$⊢ (((φ \land \neg T ∖ U = \emptyset) \land x \in (T ∖ U)) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to φ$
29		simplr	$⊢ (((φ \land \neg T ∖ U = \emptyset) \land x \in (T ∖ U)) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to x \in (T ∖ U)$
30		simpr	$⊢ (((φ \land \neg T ∖ U = \emptyset) \land x \in (T ∖ U)) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
31		eqid	$⊢ J Cn K = J Cn K$
32	3 4 31 6	fcnre	$⊢ φ \to P : T ⟶ ℝ$
33	32	adantr	$⊢ (φ \land x \in (T ∖ U)) \to P : T ⟶ ℝ$
34		eldifi	$⊢ x \in (T ∖ U) \to x \in T$
35	34	adantl	$⊢ (φ \land x \in (T ∖ U)) \to x \in T$
36	33 35	ffvelcdmd	$⊢ (φ \land x \in (T ∖ U)) \to P (x) \in ℝ$
37		nfcv	$⊢ \underline{Ⅎ} x (T ∖ U)$
38		nfv	$⊢ Ⅎ x 0 < P (t)$
39		nfv	$⊢ Ⅎ t 0 < P (x)$
40		fveq2	$⊢ t = x \to P (t) = P (x)$
41	40	breq2d	$⊢ t = x \to (0 < P (t) \leftrightarrow 0 < P (x))$
42	16 37 38 39 41	cbvralfw	$⊢ \forall t \in (T ∖ U) 0 < P (t) \leftrightarrow \forall x \in (T ∖ U) 0 < P (x)$
43	42	biimpi	$⊢ \forall t \in (T ∖ U) 0 < P (t) \to \forall x \in (T ∖ U) 0 < P (x)$
44	43	r19.21bi	$⊢ (\forall t \in (T ∖ U) 0 < P (t) \land x \in (T ∖ U)) \to 0 < P (x)$
45	7 44	sylan	$⊢ (φ \land x \in (T ∖ U)) \to 0 < P (x)$
46	36 45	elrpd	$⊢ (φ \land x \in (T ∖ U)) \to P (x) \in ℝ^{+}$
47	46	3adant3	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to P (x) \in ℝ^{+}$
48	16	nfcri	$⊢ Ⅎ t x \in (T ∖ U)$
49		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
50	2 48 49	nf3an	$⊢ Ⅎ t (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
51		rspa	$⊢ (\forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t) \land t \in (T ∖ U)) \to ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
52	51	3ad2antl3	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land t \in (T ∖ U)) \to ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
53		simpl2	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land t \in (T ∖ U)) \to x \in (T ∖ U)$
54		fvres	$⊢ x \in (T ∖ U) \to ({P ↾}_{(T ∖ U)}) (x) = P (x)$
55	53 54	syl	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land t \in (T ∖ U)) \to ({P ↾}_{(T ∖ U)}) (x) = P (x)$
56		fvres	$⊢ t \in (T ∖ U) \to ({P ↾}_{(T ∖ U)}) (t) = P (t)$
57	56	adantl	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land t \in (T ∖ U)) \to ({P ↾}_{(T ∖ U)}) (t) = P (t)$
58	52 55 57	3brtr3d	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land t \in (T ∖ U)) \to P (x) \leq P (t)$
59	58	ex	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to (t \in (T ∖ U) \to P (x) \leq P (t))$
60	50 59	ralrimi	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to \forall t \in (T ∖ U) P (x) \leq P (t)$
61		eleq1	$⊢ c = P (x) \to (c \in ℝ^{+} \leftrightarrow P (x) \in ℝ^{+})$
62		breq1	$⊢ c = P (x) \to (c \leq P (t) \leftrightarrow P (x) \leq P (t))$
63	62	ralbidv	$⊢ c = P (x) \to (\forall t \in (T ∖ U) c \leq P (t) \leftrightarrow \forall t \in (T ∖ U) P (x) \leq P (t))$
64	61 63	anbi12d	$⊢ c = P (x) \to ((c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \leftrightarrow (P (x) \in ℝ^{+} \land \forall t \in (T ∖ U) P (x) \leq P (t)))$
65	64	spcegv	$⊢ P (x) \in ℝ^{+} \to ((P (x) \in ℝ^{+} \land \forall t \in (T ∖ U) P (x) \leq P (t)) \to \exists c (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)))$
66	47 65	syl	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to ((P (x) \in ℝ^{+} \land \forall t \in (T ∖ U) P (x) \leq P (t)) \to \exists c (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)))$
67	47 60 66	mp2and	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to \exists c (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))$
68		simpl1	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))) \to φ$
69		simprl	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))) \to c \in ℝ^{+}$
70		simprr	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))) \to \forall t \in (T ∖ U) c \leq P (t)$
71		nfv	$⊢ Ⅎ t c \in ℝ^{+}$
72		nfra1	$⊢ Ⅎ t \forall t \in (T ∖ U) c \leq P (t)$
73	2 71 72	nf3an	$⊢ Ⅎ t (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))$
74		eqid	$⊢ if (c \leq \frac{1}{2}, c, \frac{1}{2}) = if (c \leq \frac{1}{2}, c, \frac{1}{2})$
75	32	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \to P : T ⟶ ℝ$
76		difssd	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \to T ∖ U \subseteq T$
77		simp2	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \to c \in ℝ^{+}$
78		simp3	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \to \forall t \in (T ∖ U) c \leq P (t)$
79	73 74 75 76 77 78	stoweidlem5	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
80	68 69 70 79	syl3anc	$⊢ ((φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \land (c \in ℝ^{+} \land \forall t \in (T ∖ U) c \leq P (t))) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
81	67 80	exlimddv	$⊢ (φ \land x \in (T ∖ U) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
82	28 29 30 81	syl3anc	$⊢ (((φ \land \neg T ∖ U = \emptyset) \land x \in (T ∖ U)) \land \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
83		eqid	$⊢ ⋃ (J ↾_{𝑡} (T ∖ U)) = ⋃ (J ↾_{𝑡} (T ∖ U))$
84		cmptop	$⊢ J \in Comp \to J \in Top$
85	5 84	syl	$⊢ φ \to J \in Top$
86		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
87	8 86	syl	$⊢ φ \to U \subseteq ⋃ J$
88	87 4	sseqtrrdi	$⊢ φ \to U \subseteq T$
89	4	isopn2	$⊢ (J \in Top \land U \subseteq T) \to (U \in J \leftrightarrow T ∖ U \in Clsd (J))$
90	85 88 89	syl2anc	$⊢ φ \to (U \in J \leftrightarrow T ∖ U \in Clsd (J))$
91	8 90	mpbid	$⊢ φ \to T ∖ U \in Clsd (J)$
92		cmpcld	$⊢ (J \in Comp \land T ∖ U \in Clsd (J)) \to J ↾_{𝑡} (T ∖ U) \in Comp$
93	5 91 92	syl2anc	$⊢ φ \to J ↾_{𝑡} (T ∖ U) \in Comp$
94	93	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to J ↾_{𝑡} (T ∖ U) \in Comp$
95	6	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to P \in (J Cn K)$
96		difssd	$⊢ (φ \land \neg T ∖ U = \emptyset) \to T ∖ U \subseteq T$
97	4	cnrest	$⊢ (P \in (J Cn K) \land T ∖ U \subseteq T) \to {P ↾}_{(T ∖ U)} \in ((J ↾_{𝑡} (T ∖ U)) Cn K)$
98	95 96 97	syl2anc	$⊢ (φ \land \neg T ∖ U = \emptyset) \to {P ↾}_{(T ∖ U)} \in ((J ↾_{𝑡} (T ∖ U)) Cn K)$
99		difssd	$⊢ φ \to T ∖ U \subseteq T$
100	4	restuni	$⊢ (J \in Top \land T ∖ U \subseteq T) \to T ∖ U = ⋃ (J ↾_{𝑡} (T ∖ U))$
101	85 99 100	syl2anc	$⊢ φ \to T ∖ U = ⋃ (J ↾_{𝑡} (T ∖ U))$
102	101	neeq1d	$⊢ φ \to (T ∖ U \neq \emptyset \leftrightarrow ⋃ (J ↾_{𝑡} (T ∖ U)) \neq \emptyset)$
103		df-ne	$⊢ T ∖ U \neq \emptyset \leftrightarrow \neg T ∖ U = \emptyset$
104	102 103	bitr3di	$⊢ φ \to (⋃ (J ↾_{𝑡} (T ∖ U)) \neq \emptyset \leftrightarrow \neg T ∖ U = \emptyset)$
105	104	biimpar	$⊢ (φ \land \neg T ∖ U = \emptyset) \to ⋃ (J ↾_{𝑡} (T ∖ U)) \neq \emptyset$
106	83 3 94 98 105	evth2	$⊢ (φ \land \neg T ∖ U = \emptyset) \to \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall s \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (s)$
107		nfcv	$⊢ \underline{Ⅎ} s ⋃ (J ↾_{𝑡} (T ∖ U))$
108		nfcv	$⊢ \underline{Ⅎ} t J$
109		nfcv	$⊢ \underline{Ⅎ} t ↾_{𝑡}$
110	108 109 16	nfov	$⊢ \underline{Ⅎ} t (J ↾_{𝑡} (T ∖ U))$
111	110	nfuni	$⊢ \underline{Ⅎ} t ⋃ (J ↾_{𝑡} (T ∖ U))$
112		nfcv	$⊢ \underline{Ⅎ} t P$
113	112 16	nfres	$⊢ \underline{Ⅎ} t ({P ↾}_{(T ∖ U)})$
114		nfcv	$⊢ \underline{Ⅎ} t x$
115	113 114	nffv	$⊢ \underline{Ⅎ} t ({P ↾}_{(T ∖ U)}) (x)$
116		nfcv	$⊢ \underline{Ⅎ} t \leq$
117		nfcv	$⊢ \underline{Ⅎ} t s$
118	113 117	nffv	$⊢ \underline{Ⅎ} t ({P ↾}_{(T ∖ U)}) (s)$
119	115 116 118	nfbr	$⊢ Ⅎ t ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (s)$
120		nfv	$⊢ Ⅎ s ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
121		fveq2	$⊢ s = t \to ({P ↾}_{(T ∖ U)}) (s) = ({P ↾}_{(T ∖ U)}) (t)$
122	121	breq2d	$⊢ s = t \to (({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (s) \leftrightarrow ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
123	107 111 119 120 122	cbvralfw	$⊢ \forall s \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (s) \leftrightarrow \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
124	123	rexbii	$⊢ \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall s \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (s) \leftrightarrow \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
125	106 124	sylib	$⊢ (φ \land \neg T ∖ U = \emptyset) \to \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
126	16 111	raleqf	$⊢ T ∖ U = ⋃ (J ↾_{𝑡} (T ∖ U)) \to (\forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t) \leftrightarrow \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
127	126	rexeqbi1dv	$⊢ T ∖ U = ⋃ (J ↾_{𝑡} (T ∖ U)) \to (\exists x \in (T ∖ U) \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t) \leftrightarrow \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
128	101 127	syl	$⊢ φ \to (\exists x \in (T ∖ U) \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t) \leftrightarrow \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
129	128	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to (\exists x \in (T ∖ U) \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t) \leftrightarrow \exists x \in ⋃ (J ↾_{𝑡} (T ∖ U)) \forall t \in ⋃ (J ↾_{𝑡} (T ∖ U)) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t))$
130	125 129	mpbird	$⊢ (φ \land \neg T ∖ U = \emptyset) \to \exists x \in (T ∖ U) \forall t \in (T ∖ U) ({P ↾}_{(T ∖ U)}) (x) \leq ({P ↾}_{(T ∖ U)}) (t)$
131	82 130	r19.29a	$⊢ (φ \land \neg T ∖ U = \emptyset) \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$
132	27 131	pm2.61dan	$⊢ φ \to \exists d (d \in ℝ^{+} \land d < 1 \land \forall t \in (T ∖ U) d \leq P (t))$

Metamath Proof Explorer

Theorem stoweidlem28

Proof