icccmplem3

	Ref	Expression
Hypotheses	icccmp.1	$⊢ J = topGen (ran (.))$
	icccmp.2	$⊢ T = J ↾_{𝑡} [A, B]$
	icccmp.3	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
	icccmp.4	$⊢ S = \{x \in [A, B] \| \exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z\}$
	icccmp.5	$⊢ φ \to A \in ℝ$
	icccmp.6	$⊢ φ \to B \in ℝ$
	icccmp.7	$⊢ φ \to A \leq B$
	icccmp.8	$⊢ φ \to U \subseteq J$
	icccmp.9	$⊢ φ \to [A, B] \subseteq ⋃ U$
Assertion	icccmplem3	$⊢ φ \to B \in S$

Proof

Step	Hyp	Ref	Expression
1		icccmp.1	$⊢ J = topGen (ran (.))$
2		icccmp.2	$⊢ T = J ↾_{𝑡} [A, B]$
3		icccmp.3	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
4		icccmp.4	$⊢ S = \{x \in [A, B] \| \exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z\}$
5		icccmp.5	$⊢ φ \to A \in ℝ$
6		icccmp.6	$⊢ φ \to B \in ℝ$
7		icccmp.7	$⊢ φ \to A \leq B$
8		icccmp.8	$⊢ φ \to U \subseteq J$
9		icccmp.9	$⊢ φ \to [A, B] \subseteq ⋃ U$
10	4	ssrab3	$⊢ S \subseteq [A, B]$
11		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
12	5 6 11	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
13	10 12	sstrid	$⊢ φ \to S \subseteq ℝ$
14	1 2 3 4 5 6 7 8 9	icccmplem1	$⊢ φ \to (A \in S \land \forall y \in S y \leq B)$
15	14	simpld	$⊢ φ \to A \in S$
16	15	ne0d	$⊢ φ \to S \neq \emptyset$
17	14	simprd	$⊢ φ \to \forall y \in S y \leq B$
18		brralrspcev	$⊢ (B \in ℝ \land \forall y \in S y \leq B) \to \exists v \in ℝ \forall y \in S y \leq v$
19	6 17 18	syl2anc	$⊢ φ \to \exists v \in ℝ \forall y \in S y \leq v$
20	13 16 19	suprcld	$⊢ φ \to sup (S ℝ <) \in ℝ$
21	13 16 19 15	suprubd	$⊢ φ \to A \leq sup (S ℝ <)$
22		suprleub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists v \in ℝ \forall y \in S y \leq v) \land B \in ℝ) \to (sup (S ℝ <) \leq B \leftrightarrow \forall y \in S y \leq B)$
23	13 16 19 6 22	syl31anc	$⊢ φ \to (sup (S ℝ <) \leq B \leftrightarrow \forall y \in S y \leq B)$
24	17 23	mpbird	$⊢ φ \to sup (S ℝ <) \leq B$
25		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (sup (S ℝ <) \in [A, B] \leftrightarrow (sup (S ℝ <) \in ℝ \land A \leq sup (S ℝ <) \land sup (S ℝ <) \leq B))$
26	5 6 25	syl2anc	$⊢ φ \to (sup (S ℝ <) \in [A, B] \leftrightarrow (sup (S ℝ <) \in ℝ \land A \leq sup (S ℝ <) \land sup (S ℝ <) \leq B))$
27	20 21 24 26	mpbir3and	$⊢ φ \to sup (S ℝ <) \in [A, B]$
28	9 27	sseldd	$⊢ φ \to sup (S ℝ <) \in ⋃ U$
29		eluni2	$⊢ sup (S ℝ <) \in ⋃ U \leftrightarrow \exists u \in U sup (S ℝ <) \in u$
30	28 29	sylib	$⊢ φ \to \exists u \in U sup (S ℝ <) \in u$
31	8	sselda	$⊢ (φ \land u \in U) \to u \in J$
32	3	rexmet	$⊢ D \in ∞Met (ℝ)$
33		eqid	$⊢ MetOpen (D) = MetOpen (D)$
34	3 33	tgioo	$⊢ topGen (ran (.)) = MetOpen (D)$
35	1 34	eqtri	$⊢ J = MetOpen (D)$
36	35	mopni2	$⊢ (D \in ∞Met (ℝ) \land u \in J \land sup (S ℝ <) \in u) \to \exists w \in ℝ^{+} sup (S ℝ <) ball (D) w \subseteq u$
37	32 36	mp3an1	$⊢ (u \in J \land sup (S ℝ <) \in u) \to \exists w \in ℝ^{+} sup (S ℝ <) ball (D) w \subseteq u$
38	37	ex	$⊢ u \in J \to (sup (S ℝ <) \in u \to \exists w \in ℝ^{+} sup (S ℝ <) ball (D) w \subseteq u)$
39	31 38	syl	$⊢ (φ \land u \in U) \to (sup (S ℝ <) \in u \to \exists w \in ℝ^{+} sup (S ℝ <) ball (D) w \subseteq u)$
40	5	ad2antrr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to A \in ℝ$
41	6	ad2antrr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to B \in ℝ$
42	7	ad2antrr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to A \leq B$
43	8	ad2antrr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to U \subseteq J$
44	9	ad2antrr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to [A, B] \subseteq ⋃ U$
45		simplr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to u \in U$
46		simprl	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to w \in ℝ^{+}$
47		simprr	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to sup (S ℝ <) ball (D) w \subseteq u$
48		eqid	$⊢ sup (S ℝ <) = sup (S ℝ <)$
49		eqid	$⊢ if (sup (S ℝ <) + (\frac{w}{2}) \leq B, sup (S ℝ <) + (\frac{w}{2}), B) = if (sup (S ℝ <) + (\frac{w}{2}) \leq B, sup (S ℝ <) + (\frac{w}{2}), B)$
50	1 2 3 4 40 41 42 43 44 45 46 47 48 49	icccmplem2	$⊢ ((φ \land u \in U) \land (w \in ℝ^{+} \land sup (S ℝ <) ball (D) w \subseteq u)) \to B \in S$
51	50	rexlimdvaa	$⊢ (φ \land u \in U) \to (\exists w \in ℝ^{+} sup (S ℝ <) ball (D) w \subseteq u \to B \in S)$
52	39 51	syld	$⊢ (φ \land u \in U) \to (sup (S ℝ <) \in u \to B \in S)$
53	52	rexlimdva	$⊢ φ \to (\exists u \in U sup (S ℝ <) \in u \to B \in S)$
54	30 53	mpd	$⊢ φ \to B \in S$

Metamath Proof Explorer

Theorem icccmplem3

Proof