icccmplem1

	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	icccmplem1	$⊢ φ \to (A \in S \land \forall y \in S y \leq B)$

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	5	rexrd	$⊢ φ \to A \in ℝ^{*}$
11	6	rexrd	$⊢ φ \to B \in ℝ^{*}$
12		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
13	10 11 7 12	syl3anc	$⊢ φ \to A \in [A, B]$
14	9 13	sseldd	$⊢ φ \to A \in ⋃ U$
15		eluni2	$⊢ A \in ⋃ U \leftrightarrow \exists u \in U A \in u$
16	14 15	sylib	$⊢ φ \to \exists u \in U A \in u$
17		snssi	$⊢ u \in U \to \{u\} \subseteq U$
18	17	ad2antrl	$⊢ (φ \land (u \in U \land A \in u)) \to \{u\} \subseteq U$
19		snex	$⊢ \{u\} \in V$
20	19	elpw	$⊢ \{u\} \in 𝒫 U \leftrightarrow \{u\} \subseteq U$
21	18 20	sylibr	$⊢ (φ \land (u \in U \land A \in u)) \to \{u\} \in 𝒫 U$
22		snfi	$⊢ \{u\} \in Fin$
23	22	a1i	$⊢ (φ \land (u \in U \land A \in u)) \to \{u\} \in Fin$
24	21 23	elind	$⊢ (φ \land (u \in U \land A \in u)) \to \{u\} \in (𝒫 U \cap Fin)$
25	10	adantr	$⊢ (φ \land (u \in U \land A \in u)) \to A \in ℝ^{*}$
26		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
27	25 26	syl	$⊢ (φ \land (u \in U \land A \in u)) \to [A, A] = \{A\}$
28		snssi	$⊢ A \in u \to \{A\} \subseteq u$
29	28	ad2antll	$⊢ (φ \land (u \in U \land A \in u)) \to \{A\} \subseteq u$
30	27 29	eqsstrd	$⊢ (φ \land (u \in U \land A \in u)) \to [A, A] \subseteq u$
31		unieq	$⊢ z = \{u\} \to ⋃ z = ⋃ \{u\}$
32		unisnv	$⊢ ⋃ \{u\} = u$
33	31 32	eqtrdi	$⊢ z = \{u\} \to ⋃ z = u$
34	33	sseq2d	$⊢ z = \{u\} \to ([A, A] \subseteq ⋃ z \leftrightarrow [A, A] \subseteq u)$
35	34	rspcev	$⊢ (\{u\} \in (𝒫 U \cap Fin) \land [A, A] \subseteq u) \to \exists z \in (𝒫 U \cap Fin) [A, A] \subseteq ⋃ z$
36	24 30 35	syl2anc	$⊢ (φ \land (u \in U \land A \in u)) \to \exists z \in (𝒫 U \cap Fin) [A, A] \subseteq ⋃ z$
37	16 36	rexlimddv	$⊢ φ \to \exists z \in (𝒫 U \cap Fin) [A, A] \subseteq ⋃ z$
38		oveq2	$⊢ x = A \to [A, x] = [A, A]$
39	38	sseq1d	$⊢ x = A \to ([A, x] \subseteq ⋃ z \leftrightarrow [A, A] \subseteq ⋃ z)$
40	39	rexbidv	$⊢ x = A \to (\exists z \in (𝒫 U \cap Fin) [A, x] \subseteq ⋃ z \leftrightarrow \exists z \in (𝒫 U \cap Fin) [A, A] \subseteq ⋃ z)$
41	40 4	elrab2	$⊢ A \in S \leftrightarrow (A \in [A, B] \land \exists z \in (𝒫 U \cap Fin) [A, A] \subseteq ⋃ z)$
42	13 37 41	sylanbrc	$⊢ φ \to A \in S$
43	4	ssrab3	$⊢ S \subseteq [A, B]$
44	43	sseli	$⊢ y \in S \to y \in [A, B]$
45		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
46	5 6 45	syl2anc	$⊢ φ \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
47	46	biimpa	$⊢ (φ \land y \in [A, B]) \to (y \in ℝ \land A \leq y \land y \leq B)$
48	47	simp3d	$⊢ (φ \land y \in [A, B]) \to y \leq B$
49	44 48	sylan2	$⊢ (φ \land y \in S) \to y \leq B$
50	49	ralrimiva	$⊢ φ \to \forall y \in S y \leq B$
51	42 50	jca	$⊢ φ \to (A \in S \land \forall y \in S y \leq B)$

Metamath Proof Explorer

Theorem icccmplem1

Proof