stoweidlem50

Description: This lemma proves that sets U(t) as defined in Lemma 1 of BrosowskiDeutsh p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem50.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem50.2	$⊢ Ⅎ t φ$
	stoweidlem50.3	$⊢ K = topGen (ran (.))$
	stoweidlem50.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem50.5	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
	stoweidlem50.6	$⊢ T = ⋃ J$
	stoweidlem50.7	$⊢ C = J Cn K$
	stoweidlem50.8	$⊢ φ \to J \in Comp$
	stoweidlem50.9	$⊢ φ \to A \subseteq C$
	stoweidlem50.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem50.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem50.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem50.13	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem50.14	$⊢ φ \to U \in J$
	stoweidlem50.15	$⊢ φ \to Z \in U$
Assertion	stoweidlem50	$⊢ φ \to \exists u (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem50.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem50.2	$⊢ Ⅎ t φ$
3		stoweidlem50.3	$⊢ K = topGen (ran (.))$
4		stoweidlem50.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
5		stoweidlem50.5	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
6		stoweidlem50.6	$⊢ T = ⋃ J$
7		stoweidlem50.7	$⊢ C = J Cn K$
8		stoweidlem50.8	$⊢ φ \to J \in Comp$
9		stoweidlem50.9	$⊢ φ \to A \subseteq C$
10		stoweidlem50.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
11		stoweidlem50.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
12		stoweidlem50.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
13		stoweidlem50.13	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
14		stoweidlem50.14	$⊢ φ \to U \in J$
15		stoweidlem50.15	$⊢ φ \to Z \in U$
16		nfrab1	$⊢ \underline{Ⅎ} h \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
17	4 16	nfcxfr	$⊢ \underline{Ⅎ} h Q$
18		nfv	$⊢ Ⅎ q φ$
19	9 7	sseqtrdi	$⊢ φ \to A \subseteq J Cn K$
20	8	uniexd	$⊢ φ \to ⋃ J \in V$
21	6 20	eqeltrid	$⊢ φ \to T \in V$
22	1 17 18 2 3 4 5 6 8 19 10 11 12 13 14 15 21	stoweidlem46	$⊢ φ \to T ∖ U \subseteq ⋃ W$
23		dfin4	$⊢ T \cap U = T ∖ (T ∖ U)$
24		elssuni	$⊢ U \in J \to U \subseteq ⋃ J$
25	14 24	syl	$⊢ φ \to U \subseteq ⋃ J$
26	25 6	sseqtrrdi	$⊢ φ \to U \subseteq T$
27		sseqin2	$⊢ U \subseteq T \leftrightarrow T \cap U = U$
28	26 27	sylib	$⊢ φ \to T \cap U = U$
29	23 28	eqtr3id	$⊢ φ \to T ∖ (T ∖ U) = U$
30	29 14	eqeltrd	$⊢ φ \to T ∖ (T ∖ U) \in J$
31		cmptop	$⊢ J \in Comp \to J \in Top$
32	8 31	syl	$⊢ φ \to J \in Top$
33		difssd	$⊢ φ \to T ∖ U \subseteq T$
34	6	iscld2	$⊢ (J \in Top \land T ∖ U \subseteq T) \to (T ∖ U \in Clsd (J) \leftrightarrow T ∖ (T ∖ U) \in J)$
35	32 33 34	syl2anc	$⊢ φ \to (T ∖ U \in Clsd (J) \leftrightarrow T ∖ (T ∖ U) \in J)$
36	30 35	mpbird	$⊢ φ \to T ∖ U \in Clsd (J)$
37		cmpcld	$⊢ (J \in Comp \land T ∖ U \in Clsd (J)) \to J ↾_{𝑡} (T ∖ U) \in Comp$
38	8 36 37	syl2anc	$⊢ φ \to J ↾_{𝑡} (T ∖ U) \in Comp$
39	6	cmpsub	$⊢ (J \in Top \land T ∖ U \subseteq T) \to (J ↾_{𝑡} (T ∖ U) \in Comp \leftrightarrow \forall c \in 𝒫 J (T ∖ U \subseteq ⋃ c \to \exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u))$
40	32 33 39	syl2anc	$⊢ φ \to (J ↾_{𝑡} (T ∖ U) \in Comp \leftrightarrow \forall c \in 𝒫 J (T ∖ U \subseteq ⋃ c \to \exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u))$
41	38 40	mpbid	$⊢ φ \to \forall c \in 𝒫 J (T ∖ U \subseteq ⋃ c \to \exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u)$
42		ssrab2	$⊢ \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\} \subseteq J$
43	5 42	eqsstri	$⊢ W \subseteq J$
44	5 8	rabexd	$⊢ φ \to W \in V$
45		elpwg	$⊢ W \in V \to (W \in 𝒫 J \leftrightarrow W \subseteq J)$
46	44 45	syl	$⊢ φ \to (W \in 𝒫 J \leftrightarrow W \subseteq J)$
47	43 46	mpbiri	$⊢ φ \to W \in 𝒫 J$
48		unieq	$⊢ c = W \to ⋃ c = ⋃ W$
49	48	sseq2d	$⊢ c = W \to (T ∖ U \subseteq ⋃ c \leftrightarrow T ∖ U \subseteq ⋃ W)$
50		pweq	$⊢ c = W \to 𝒫 c = 𝒫 W$
51	50	ineq1d	$⊢ c = W \to 𝒫 c \cap Fin = 𝒫 W \cap Fin$
52	51	rexeqdv	$⊢ c = W \to (\exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u \leftrightarrow \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u)$
53	49 52	imbi12d	$⊢ c = W \to ((T ∖ U \subseteq ⋃ c \to \exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u) \leftrightarrow (T ∖ U \subseteq ⋃ W \to \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u))$
54	53	rspccva	$⊢ (\forall c \in 𝒫 J (T ∖ U \subseteq ⋃ c \to \exists u \in (𝒫 c \cap Fin) T ∖ U \subseteq ⋃ u) \land W \in 𝒫 J) \to (T ∖ U \subseteq ⋃ W \to \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u)$
55	41 47 54	syl2anc	$⊢ φ \to (T ∖ U \subseteq ⋃ W \to \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u)$
56	55	imp	$⊢ (φ \land T ∖ U \subseteq ⋃ W) \to \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u$
57		df-rex	$⊢ \exists u \in (𝒫 W \cap Fin) T ∖ U \subseteq ⋃ u \leftrightarrow \exists u (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)$
58	56 57	sylib	$⊢ (φ \land T ∖ U \subseteq ⋃ W) \to \exists u (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)$
59		elinel2	$⊢ u \in (𝒫 W \cap Fin) \to u \in Fin$
60	59	ad2antrl	$⊢ ((φ \land T ∖ U \subseteq ⋃ W) \land (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)) \to u \in Fin$
61		elinel1	$⊢ u \in (𝒫 W \cap Fin) \to u \in 𝒫 W$
62	61	ad2antrl	$⊢ ((φ \land T ∖ U \subseteq ⋃ W) \land (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)) \to u \in 𝒫 W$
63	62	elpwid	$⊢ ((φ \land T ∖ U \subseteq ⋃ W) \land (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)) \to u \subseteq W$
64		simprr	$⊢ ((φ \land T ∖ U \subseteq ⋃ W) \land (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)) \to T ∖ U \subseteq ⋃ u$
65	60 63 64	3jca	$⊢ ((φ \land T ∖ U \subseteq ⋃ W) \land (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u)) \to (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u)$
66	65	ex	$⊢ (φ \land T ∖ U \subseteq ⋃ W) \to ((u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u) \to (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u))$
67	66	eximdv	$⊢ (φ \land T ∖ U \subseteq ⋃ W) \to (\exists u (u \in (𝒫 W \cap Fin) \land T ∖ U \subseteq ⋃ u) \to \exists u (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u))$
68	58 67	mpd	$⊢ (φ \land T ∖ U \subseteq ⋃ W) \to \exists u (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u)$
69	22 68	mpdan	$⊢ φ \to \exists u (u \in Fin \land u \subseteq W \land T ∖ U \subseteq ⋃ u)$

Metamath Proof Explorer

Theorem stoweidlem50

Proof