Theorem 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	⊢ Ⅎ 𝑡 𝑈
	stoweidlem50.2	⊢ Ⅎ 𝑡 𝜑
	stoweidlem50.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem50.4	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
	stoweidlem50.5	⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
	stoweidlem50.6	⊢ 𝑇 = ∪ 𝐽
	stoweidlem50.7	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stoweidlem50.8	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	stoweidlem50.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	stoweidlem50.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem50.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem50.12	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
	stoweidlem50.13	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
	stoweidlem50.14	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
	stoweidlem50.15	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion	stoweidlem50	⊢ ( 𝜑 → ∃ 𝑢 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem50.1	⊢ Ⅎ 𝑡 𝑈
2		stoweidlem50.2	⊢ Ⅎ 𝑡 𝜑
3		stoweidlem50.3	⊢ 𝐾 = ( topGen ‘ ran (,) )
4		stoweidlem50.4	⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
5		stoweidlem50.5	⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
6		stoweidlem50.6	⊢ 𝑇 = ∪ 𝐽
7		stoweidlem50.7	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8		stoweidlem50.8	⊢ ( 𝜑 → 𝐽 ∈ Comp )
9		stoweidlem50.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
10		stoweidlem50.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11		stoweidlem50.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12		stoweidlem50.12	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
13		stoweidlem50.13	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
14		stoweidlem50.14	⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
15		stoweidlem50.15	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
16		nfrab1	⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
17	4 16	nfcxfr	⊢ Ⅎ ℎ 𝑄
18		nfv	⊢ Ⅎ 𝑞 𝜑
19	9 7	sseqtrdi	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
20	8	uniexd	⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
21	6 20	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ V )
22	1 17 18 2 3 4 5 6 8 19 10 11 12 13 14 15 21	stoweidlem46	⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 )
23		dfin4	⊢ ( 𝑇 ∩ 𝑈 ) = ( 𝑇 ∖ ( 𝑇 ∖ 𝑈 ) )
24		elssuni	⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
25	14 24	syl	⊢ ( 𝜑 → 𝑈 ⊆ ∪ 𝐽 )
26	25 6	sseqtrrdi	⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
27		sseqin2	⊢ ( 𝑈 ⊆ 𝑇 ↔ ( 𝑇 ∩ 𝑈 ) = 𝑈 )
28	26 27	sylib	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = 𝑈 )
29	23 28	syl5eqr	⊢ ( 𝜑 → ( 𝑇 ∖ ( 𝑇 ∖ 𝑈 ) ) = 𝑈 )
30	29 14	eqeltrd	⊢ ( 𝜑 → ( 𝑇 ∖ ( 𝑇 ∖ 𝑈 ) ) ∈ 𝐽 )
31		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
32	8 31	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
33		difssd	⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ 𝑇 )
34	6	iscld2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑇 ∖ 𝑈 ) ⊆ 𝑇 ) → ( ( 𝑇 ∖ 𝑈 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑇 ∖ ( 𝑇 ∖ 𝑈 ) ) ∈ 𝐽 ) )
35	32 33 34	syl2anc	⊢ ( 𝜑 → ( ( 𝑇 ∖ 𝑈 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑇 ∖ ( 𝑇 ∖ 𝑈 ) ) ∈ 𝐽 ) )
36	30 35	mpbird	⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ∈ ( Clsd ‘ 𝐽 ) )
37		cmpcld	⊢ ( ( 𝐽 ∈ Comp ∧ ( 𝑇 ∖ 𝑈 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t ( 𝑇 ∖ 𝑈 ) ) ∈ Comp )
38	8 36 37	syl2anc	⊢ ( 𝜑 → ( 𝐽 ↾t ( 𝑇 ∖ 𝑈 ) ) ∈ Comp )
39	6	cmpsub	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑇 ∖ 𝑈 ) ⊆ 𝑇 ) → ( ( 𝐽 ↾t ( 𝑇 ∖ 𝑈 ) ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 → ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) )
40	32 33 39	syl2anc	⊢ ( 𝜑 → ( ( 𝐽 ↾t ( 𝑇 ∖ 𝑈 ) ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 → ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) )
41	38 40	mpbid	⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝒫 𝐽 ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 → ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
42		ssrab2	⊢ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ⊆ 𝐽
43	5 42	eqsstri	⊢ 𝑊 ⊆ 𝐽
44	5 8	rabexd	⊢ ( 𝜑 → 𝑊 ∈ V )
45		elpwg	⊢ ( 𝑊 ∈ V → ( 𝑊 ∈ 𝒫 𝐽 ↔ 𝑊 ⊆ 𝐽 ) )
46	44 45	syl	⊢ ( 𝜑 → ( 𝑊 ∈ 𝒫 𝐽 ↔ 𝑊 ⊆ 𝐽 ) )
47	43 46	mpbiri	⊢ ( 𝜑 → 𝑊 ∈ 𝒫 𝐽 )
48		unieq	⊢ ( 𝑐 = 𝑊 → ∪ 𝑐 = ∪ 𝑊 )
49	48	sseq2d	⊢ ( 𝑐 = 𝑊 → ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 ↔ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) )
50		pweq	⊢ ( 𝑐 = 𝑊 → 𝒫 𝑐 = 𝒫 𝑊 )
51	50	ineq1d	⊢ ( 𝑐 = 𝑊 → ( 𝒫 𝑐 ∩ Fin ) = ( 𝒫 𝑊 ∩ Fin ) )
52	51	rexeqdv	⊢ ( 𝑐 = 𝑊 → ( ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ↔ ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
53	49 52	imbi12d	⊢ ( 𝑐 = 𝑊 → ( ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 → ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ↔ ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 → ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) )
54	53	rspccva	⊢ ( ( ∀ 𝑐 ∈ 𝒫 𝐽 ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑐 → ∃ 𝑢 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ∧ 𝑊 ∈ 𝒫 𝐽 ) → ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 → ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
55	41 47 54	syl2anc	⊢ ( 𝜑 → ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 → ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
56	55	imp	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) → ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
57		df-rex	⊢ ( ∃ 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ↔ ∃ 𝑢 ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
58	56 57	sylib	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) → ∃ 𝑢 ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
59		elinel2	⊢ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) → 𝑢 ∈ Fin )
60	59	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ∈ Fin )
61		elinel1	⊢ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) → 𝑢 ∈ 𝒫 𝑊 )
62	61	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ∈ 𝒫 𝑊 )
63	62	elpwid	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ⊆ 𝑊 )
64		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
65	60 63 64	3jca	⊢ ( ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) ∧ ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
66	65	ex	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) → ( ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) → ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) )
67	66	eximdv	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) → ( ∃ 𝑢 ( 𝑢 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) → ∃ 𝑢 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) )
68	58 67	mpd	⊢ ( ( 𝜑 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 ) → ∃ 𝑢 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
69	22 68	mpdan	⊢ ( 𝜑 → ∃ 𝑢 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )