icccmplem2

	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$
	icccmp.10	$⊢ φ \to V \in U$
	icccmp.11	$⊢ φ \to C \in ℝ^{+}$
	icccmp.12	$⊢ φ \to G ball (D) C \subseteq V$
	icccmp.13	$⊢ G = sup (S ℝ <)$
	icccmp.14	$⊢ R = if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B)$
Assertion	icccmplem2	$⊢ φ \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		icccmp.10	$⊢ φ \to V \in U$
11		icccmp.11	$⊢ φ \to C \in ℝ^{+}$
12		icccmp.12	$⊢ φ \to G ball (D) C \subseteq V$
13		icccmp.13	$⊢ G = sup (S ℝ <)$
14		icccmp.14	$⊢ R = if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B)$
15	4	ssrab3	$⊢ S \subseteq [A, B]$
16		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
17	5 6 16	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
18	15 17	sstrid	$⊢ φ \to S \subseteq ℝ$
19	1 2 3 4 5 6 7 8 9	icccmplem1	$⊢ φ \to (A \in S \land \forall y \in S y \leq B)$
20	19	simpld	$⊢ φ \to A \in S$
21	20	ne0d	$⊢ φ \to S \neq \emptyset$
22	19	simprd	$⊢ φ \to \forall y \in S y \leq B$
23		brralrspcev	$⊢ (B \in ℝ \land \forall y \in S y \leq B) \to \exists n \in ℝ \forall y \in S y \leq n$
24	6 22 23	syl2anc	$⊢ φ \to \exists n \in ℝ \forall y \in S y \leq n$
25	18 21 24	suprcld	$⊢ φ \to sup (S ℝ <) \in ℝ$
26	13 25	eqeltrid	$⊢ φ \to G \in ℝ$
27	11	rphalfcld	$⊢ φ \to \frac{C}{2} \in ℝ^{+}$
28	26 27	ltaddrpd	$⊢ φ \to G < G + (\frac{C}{2})$
29	27	rpred	$⊢ φ \to \frac{C}{2} \in ℝ$
30	26 29	readdcld	$⊢ φ \to G + (\frac{C}{2}) \in ℝ$
31	26 30	ltnled	$⊢ φ \to (G < G + (\frac{C}{2}) \leftrightarrow \neg G + (\frac{C}{2}) \leq G)$
32	28 31	mpbid	$⊢ φ \to \neg G + (\frac{C}{2}) \leq G$
33	30 6	ifcld	$⊢ φ \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \in ℝ$
34	14 33	eqeltrid	$⊢ φ \to R \in ℝ$
35	18 21 24 20	suprubd	$⊢ φ \to A \leq sup (S ℝ <)$
36	35 13	breqtrrdi	$⊢ φ \to A \leq G$
37	26 30 28	ltled	$⊢ φ \to G \leq G + (\frac{C}{2})$
38	5 26 30 36 37	letrd	$⊢ φ \to A \leq G + (\frac{C}{2})$
39		breq2	$⊢ G + (\frac{C}{2}) = if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \to (A \leq G + (\frac{C}{2}) \leftrightarrow A \leq if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B))$
40		breq2	$⊢ B = if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \to (A \leq B \leftrightarrow A \leq if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B))$
41	39 40	ifboth	$⊢ (A \leq G + (\frac{C}{2}) \land A \leq B) \to A \leq if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B)$
42	38 7 41	syl2anc	$⊢ φ \to A \leq if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B)$
43	42 14	breqtrrdi	$⊢ φ \to A \leq R$
44		min2	$⊢ (G + (\frac{C}{2}) \in ℝ \land B \in ℝ) \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \leq B$
45	30 6 44	syl2anc	$⊢ φ \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \leq B$
46	14 45	eqbrtrid	$⊢ φ \to R \leq B$
47		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (R \in [A, B] \leftrightarrow (R \in ℝ \land A \leq R \land R \leq B))$
48	5 6 47	syl2anc	$⊢ φ \to (R \in [A, B] \leftrightarrow (R \in ℝ \land A \leq R \land R \leq B))$
49	34 43 46 48	mpbir3and	$⊢ φ \to R \in [A, B]$
50	26 11	ltsubrpd	$⊢ φ \to G - C < G$
51	50 13	breqtrdi	$⊢ φ \to G - C < sup (S ℝ <)$
52	11	rpred	$⊢ φ \to C \in ℝ$
53	26 52	resubcld	$⊢ φ \to G - C \in ℝ$
54		suprlub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists n \in ℝ \forall y \in S y \leq n) \land G - C \in ℝ) \to (G - C < sup (S ℝ <) \leftrightarrow \exists v \in S G - C < v)$
55	18 21 24 53 54	syl31anc	$⊢ φ \to (G - C < sup (S ℝ <) \leftrightarrow \exists v \in S G - C < v)$
56	51 55	mpbid	$⊢ φ \to \exists v \in S G - C < v$
57		oveq2	$⊢ x = v \to [A, x] = [A, v]$
58	57	sseq1d	$⊢ x = v \to ([A, x] \subseteq ⋃ z \leftrightarrow [A, v] \subseteq ⋃ z)$
59	58	rexbidv	$⊢ x = v \to (\exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z \leftrightarrow \exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z)$
60	59 4	elrab2	$⊢ v \in S \leftrightarrow (v \in [A, B] \land \exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z)$
61		unieq	$⊢ z = w \to ⋃ z = ⋃ w$
62	61	sseq2d	$⊢ z = w \to ([A, v] \subseteq ⋃ z \leftrightarrow [A, v] \subseteq ⋃ w)$
63	62	cbvrexvw	$⊢ \exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z \leftrightarrow \exists w \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ w$
64		simpr1	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \in (𝒫 U \cap Fin)$
65		elin	$⊢ w \in (𝒫 U \cap Fin) \leftrightarrow (w \in 𝒫 U \land w \in Fin)$
66	64 65	sylib	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to (w \in 𝒫 U \land w \in Fin)$
67	66	simpld	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \in 𝒫 U$
68	67	elpwid	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \subseteq U$
69		simpll	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to φ$
70	69 10	syl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to V \in U$
71	70	snssd	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to \{V\} \subseteq U$
72	68 71	unssd	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \cup \{V\} \subseteq U$
73		vex	$⊢ w \in V$
74		snex	$⊢ \{V\} \in V$
75	73 74	unex	$⊢ w \cup \{V\} \in V$
76	75	elpw	$⊢ w \cup \{V\} \in 𝒫 U \leftrightarrow w \cup \{V\} \subseteq U$
77	72 76	sylibr	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \cup \{V\} \in 𝒫 U$
78	66	simprd	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \in Fin$
79		snfi	$⊢ \{V\} \in Fin$
80		unfi	$⊢ (w \in Fin \land \{V\} \in Fin) \to w \cup \{V\} \in Fin$
81	78 79 80	sylancl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \cup \{V\} \in Fin$
82	77 81	elind	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to w \cup \{V\} \in (𝒫 U \cap Fin)$
83		simplr2	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to [A, v] \subseteq ⋃ w$
84		ssun1	$⊢ ⋃ w \subseteq ⋃ w \cup V$
85	83 84	sstrdi	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to [A, v] \subseteq ⋃ w \cup V$
86	69 5	syl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to A \in ℝ$
87	69 34	syl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to R \in ℝ$
88		elicc2	$⊢ (A \in ℝ \land R \in ℝ) \to (t \in [A, R] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq R))$
89	86 87 88	syl2anc	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to (t \in [A, R] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq R))$
90	89	biimpa	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to (t \in ℝ \land A \leq t \land t \leq R)$
91	90	simp1d	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to t \in ℝ$
92	91	adantrr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to t \in ℝ$
93	90	simp2d	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to A \leq t$
94	93	adantrr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to A \leq t$
95		simprr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to t \leq v$
96	69 17	syl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to [A, B] \subseteq ℝ$
97		simplr	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to v \in [A, B]$
98	96 97	sseldd	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to v \in ℝ$
99		elicc2	$⊢ (A \in ℝ \land v \in ℝ) \to (t \in [A, v] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq v))$
100	86 98 99	syl2anc	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to (t \in [A, v] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq v))$
101	100	adantr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to (t \in [A, v] \leftrightarrow (t \in ℝ \land A \leq t \land t \leq v))$
102	92 94 95 101	mpbir3and	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to t \in [A, v]$
103	85 102	sseldd	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land t \leq v)) \to t \in (⋃ w \cup V)$
104	103	expr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to (t \leq v \to t \in (⋃ w \cup V))$
105	69	adantr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to φ$
106	105 12	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G ball (D) C \subseteq V$
107	91	adantrr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \in ℝ$
108	105 53	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G - C \in ℝ$
109	98	adantr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to v \in ℝ$
110		simplr3	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G - C < v$
111		simprr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to v < t$
112	108 109 107 110 111	lttrd	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G - C < t$
113	105 34	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to R \in ℝ$
114	26 52	readdcld	$⊢ φ \to G + C \in ℝ$
115	105 114	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G + C \in ℝ$
116	90	simp3d	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to t \leq R$
117	116	adantrr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \leq R$
118		min1	$⊢ (G + (\frac{C}{2}) \in ℝ \land B \in ℝ) \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \leq G + (\frac{C}{2})$
119	30 6 118	syl2anc	$⊢ φ \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) \leq G + (\frac{C}{2})$
120	14 119	eqbrtrid	$⊢ φ \to R \leq G + (\frac{C}{2})$
121		rphalflt	$⊢ C \in ℝ^{+} \to \frac{C}{2} < C$
122	11 121	syl	$⊢ φ \to \frac{C}{2} < C$
123	29 52 26 122	ltadd2dd	$⊢ φ \to G + (\frac{C}{2}) < G + C$
124	34 30 114 120 123	lelttrd	$⊢ φ \to R < G + C$
125	105 124	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to R < G + C$
126	107 113 115 117 125	lelttrd	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t < G + C$
127		rexr	$⊢ G - C \in ℝ \to G - C \in ℝ^{*}$
128		rexr	$⊢ G + C \in ℝ \to G + C \in ℝ^{*}$
129		elioo2	$⊢ (G - C \in ℝ^{} \land G + C \in ℝ^{}) \to (t \in (G - C, G + C) \leftrightarrow (t \in ℝ \land G - C < t \land t < G + C))$
130	127 128 129	syl2an	$⊢ (G - C \in ℝ \land G + C \in ℝ) \to (t \in (G - C, G + C) \leftrightarrow (t \in ℝ \land G - C < t \land t < G + C))$
131	108 115 130	syl2anc	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to (t \in (G - C, G + C) \leftrightarrow (t \in ℝ \land G - C < t \land t < G + C))$
132	107 112 126 131	mpbir3and	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \in (G - C, G + C)$
133	105 26	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G \in ℝ$
134	105 11	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to C \in ℝ^{+}$
135	134	rpred	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to C \in ℝ$
136	3	bl2ioo	$⊢ (G \in ℝ \land C \in ℝ) \to G ball (D) C = (G - C, G + C)$
137	133 135 136	syl2anc	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to G ball (D) C = (G - C, G + C)$
138	132 137	eleqtrrd	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \in (G ball (D) C)$
139	106 138	sseldd	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \in V$
140		elun2	$⊢ t \in V \to t \in (⋃ w \cup V)$
141	139 140	syl	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land (t \in [A, R] \land v < t)) \to t \in (⋃ w \cup V)$
142	141	expr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to (v < t \to t \in (⋃ w \cup V))$
143	98	adantr	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to v \in ℝ$
144		lelttric	$⊢ (t \in ℝ \land v \in ℝ) \to (t \leq v \lor v < t)$
145	91 143 144	syl2anc	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to (t \leq v \lor v < t)$
146	104 142 145	mpjaod	$⊢ (((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \land t \in [A, R]) \to t \in (⋃ w \cup V)$
147	146	ex	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to (t \in [A, R] \to t \in (⋃ w \cup V))$
148	147	ssrdv	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to [A, R] \subseteq ⋃ w \cup V$
149		uniun	$⊢ ⋃ (w \cup \{V\}) = ⋃ w \cup ⋃ \{V\}$
150		unisng	$⊢ V \in U \to ⋃ \{V\} = V$
151	70 150	syl	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to ⋃ \{V\} = V$
152	151	uneq2d	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to ⋃ w \cup ⋃ \{V\} = ⋃ w \cup V$
153	149 152	eqtrid	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to ⋃ (w \cup \{V\}) = ⋃ w \cup V$
154	148 153	sseqtrrd	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to [A, R] \subseteq ⋃ (w \cup \{V\})$
155		unieq	$⊢ y = w \cup \{V\} \to ⋃ y = ⋃ (w \cup \{V\})$
156	155	sseq2d	$⊢ y = w \cup \{V\} \to ([A, R] \subseteq ⋃ y \leftrightarrow [A, R] \subseteq ⋃ (w \cup \{V\}))$
157	156	rspcev	$⊢ (w \cup \{V\} \in (𝒫 U \cap Fin) \land [A, R] \subseteq ⋃ (w \cup \{V\})) \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y$
158	82 154 157	syl2anc	$⊢ ((φ \land v \in [A, B]) \land (w \in (𝒫 U \cap Fin) \land [A, v] \subseteq ⋃ w \land G - C < v)) \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y$
159	158	3exp2	$⊢ (φ \land v \in [A, B]) \to (w \in (𝒫 U \cap Fin) \to ([A, v] \subseteq ⋃ w \to (G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y)))$
160	159	rexlimdv	$⊢ (φ \land v \in [A, B]) \to (\exists w \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ w \to (G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y))$
161	63 160	syl5bi	$⊢ (φ \land v \in [A, B]) \to (\exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z \to (G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y))$
162	161	expimpd	$⊢ φ \to ((v \in [A, B] \land \exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z) \to (G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y))$
163	60 162	syl5bi	$⊢ φ \to (v \in S \to (G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y))$
164	163	rexlimdv	$⊢ φ \to (\exists v \in S G - C < v \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y)$
165	56 164	mpd	$⊢ φ \to \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y$
166		oveq2	$⊢ v = R \to [A, v] = [A, R]$
167	166	sseq1d	$⊢ v = R \to ([A, v] \subseteq ⋃ y \leftrightarrow [A, R] \subseteq ⋃ y)$
168	167	rexbidv	$⊢ v = R \to (\exists y \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ y \leftrightarrow \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y)$
169		unieq	$⊢ z = y \to ⋃ z = ⋃ y$
170	169	sseq2d	$⊢ z = y \to ([A, v] \subseteq ⋃ z \leftrightarrow [A, v] \subseteq ⋃ y)$
171	170	cbvrexvw	$⊢ \exists z \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ z \leftrightarrow \exists y \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ y$
172	59 171	bitrdi	$⊢ x = v \to (\exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z \leftrightarrow \exists y \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ y)$
173	172	cbvrabv	$⊢ \{x \in [A, B] \| \exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z\} = \{v \in [A, B] \| \exists y \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ y\}$
174	4 173	eqtri	$⊢ S = \{v \in [A, B] \| \exists y \in (𝒫 U \cap Fin) [A, v] \subseteq ⋃ y\}$
175	168 174	elrab2	$⊢ R \in S \leftrightarrow (R \in [A, B] \land \exists y \in (𝒫 U \cap Fin) [A, R] \subseteq ⋃ y)$
176	49 165 175	sylanbrc	$⊢ φ \to R \in S$
177	18 21 24 176	suprubd	$⊢ φ \to R \leq sup (S ℝ <)$
178	177 13	breqtrrdi	$⊢ φ \to R \leq G$
179		iftrue	$⊢ G + (\frac{C}{2}) \leq B \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) = G + (\frac{C}{2})$
180	14 179	eqtrid	$⊢ G + (\frac{C}{2}) \leq B \to R = G + (\frac{C}{2})$
181	180	breq1d	$⊢ G + (\frac{C}{2}) \leq B \to (R \leq G \leftrightarrow G + (\frac{C}{2}) \leq G)$
182	178 181	syl5ibcom	$⊢ φ \to (G + (\frac{C}{2}) \leq B \to G + (\frac{C}{2}) \leq G)$
183	32 182	mtod	$⊢ φ \to \neg G + (\frac{C}{2}) \leq B$
184		iffalse	$⊢ \neg G + (\frac{C}{2}) \leq B \to if (G + (\frac{C}{2}) \leq B, G + (\frac{C}{2}), B) = B$
185	14 184	eqtrid	$⊢ \neg G + (\frac{C}{2}) \leq B \to R = B$
186	183 185	syl	$⊢ φ \to R = B$
187	186 176	eqeltrrd	$⊢ φ \to B \in S$

Metamath Proof Explorer

Theorem icccmplem2

Proof