Theorem stoweidlem46

Description: This lemma proves that sets U(t) as defined in Lemma 1 of BrosowskiDeutsh p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem46.1	|- F/_ t U
	stoweidlem46.2	|- F/_ h Q
	stoweidlem46.3	|- F/ q ph
	stoweidlem46.4	|- F/ t ph
	stoweidlem46.5	|- K = ( topGen ` ran (,) )
	stoweidlem46.6	|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
	stoweidlem46.7	|- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
	stoweidlem46.8	|- T = U. J
	stoweidlem46.9	|- ( ph -> J e. Comp )
	stoweidlem46.10	|- ( ph -> A C_ ( J Cn K ) )
	stoweidlem46.11	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem46.12	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem46.13	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
	stoweidlem46.14	|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
	stoweidlem46.15	|- ( ph -> U e. J )
	stoweidlem46.16	|- ( ph -> Z e. U )
	stoweidlem46.17	|- ( ph -> T e. _V )
Assertion	stoweidlem46	|- ( ph -> ( T \ U ) C_ U. W )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem46.1	|- F/_ t U
2		stoweidlem46.2	|- F/_ h Q
3		stoweidlem46.3	|- F/ q ph
4		stoweidlem46.4	|- F/ t ph
5		stoweidlem46.5	|- K = ( topGen ` ran (,) )
6		stoweidlem46.6	|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
7		stoweidlem46.7	|- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
8		stoweidlem46.8	|- T = U. J
9		stoweidlem46.9	|- ( ph -> J e. Comp )
10		stoweidlem46.10	|- ( ph -> A C_ ( J Cn K ) )
11		stoweidlem46.11	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
12		stoweidlem46.12	|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
13		stoweidlem46.13	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
14		stoweidlem46.14	|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
15		stoweidlem46.15	|- ( ph -> U e. J )
16		stoweidlem46.16	|- ( ph -> Z e. U )
17		stoweidlem46.17	|- ( ph -> T e. _V )
18		nfv	|- F/ q s e. ( T \ U )
19	3 18	nfan	|- F/ q ( ph /\ s e. ( T \ U ) )
20		nfcv	|- F/_ t T
21	20 1	nfdif	|- F/_ t ( T \ U )
22	21	nfel2	|- F/ t s e. ( T \ U )
23	4 22	nfan	|- F/ t ( ph /\ s e. ( T \ U ) )
24	9	adantr	|- ( ( ph /\ s e. ( T \ U ) ) -> J e. Comp )
25	10	adantr	|- ( ( ph /\ s e. ( T \ U ) ) -> A C_ ( J Cn K ) )
26	11	3adant1r	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
27	12	3adant1r	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
28	13	adantlr	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ x e. RR ) -> ( t e. T |-> x ) e. A )
29	14	adantlr	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
30	15	adantr	|- ( ( ph /\ s e. ( T \ U ) ) -> U e. J )
31	16	adantr	|- ( ( ph /\ s e. ( T \ U ) ) -> Z e. U )
32		simpr	|- ( ( ph /\ s e. ( T \ U ) ) -> s e. ( T \ U ) )
33	19 23 2 5 6 8 24 25 26 27 28 29 30 31 32	stoweidlem43	|- ( ( ph /\ s e. ( T \ U ) ) -> E. h ( h e. Q /\ 0 < ( h ` s ) ) )
34		nfv	|- F/ g ( h e. Q /\ 0 < ( h ` s ) )
35	2	nfel2	|- F/ h g e. Q
36		nfv	|- F/ h 0 < ( g ` s )
37	35 36	nfan	|- F/ h ( g e. Q /\ 0 < ( g ` s ) )
38		eleq1	|- ( h = g -> ( h e. Q <-> g e. Q ) )
39		fveq1	|- ( h = g -> ( h ` s ) = ( g ` s ) )
40	39	breq2d	|- ( h = g -> ( 0 < ( h ` s ) <-> 0 < ( g ` s ) ) )
41	38 40	anbi12d	|- ( h = g -> ( ( h e. Q /\ 0 < ( h ` s ) ) <-> ( g e. Q /\ 0 < ( g ` s ) ) ) )
42	34 37 41	cbvexv1	|- ( E. h ( h e. Q /\ 0 < ( h ` s ) ) <-> E. g ( g e. Q /\ 0 < ( g ` s ) ) )
43	33 42	sylib	|- ( ( ph /\ s e. ( T \ U ) ) -> E. g ( g e. Q /\ 0 < ( g ` s ) ) )
44		rabexg	|- ( T e. _V -> { t e. T | 0 < ( g ` t ) } e. _V )
45	17 44	syl	|- ( ph -> { t e. T | 0 < ( g ` t ) } e. _V )
46	45	ad2antrr	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> { t e. T | 0 < ( g ` t ) } e. _V )
47		eldifi	|- ( s e. ( T \ U ) -> s e. T )
48	47	ad2antlr	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> s e. T )
49		simprr	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> 0 < ( g ` s ) )
50		fveq2	|- ( t = s -> ( g ` t ) = ( g ` s ) )
51	50	breq2d	|- ( t = s -> ( 0 < ( g ` t ) <-> 0 < ( g ` s ) ) )
52	51	elrab	|- ( s e. { t e. T | 0 < ( g ` t ) } <-> ( s e. T /\ 0 < ( g ` s ) ) )
53	48 49 52	sylanbrc	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> s e. { t e. T | 0 < ( g ` t ) } )
54		simpll	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> ph )
55	10	adantr	|- ( ( ph /\ g e. Q ) -> A C_ ( J Cn K ) )
56		simpr	|- ( ( ph /\ g e. Q ) -> g e. Q )
57	56 6	eleqtrdi	|- ( ( ph /\ g e. Q ) -> g e. { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } )
58		fveq1	|- ( h = g -> ( h ` Z ) = ( g ` Z ) )
59	58	eqeq1d	|- ( h = g -> ( ( h ` Z ) = 0 <-> ( g ` Z ) = 0 ) )
60		fveq1	|- ( h = g -> ( h ` t ) = ( g ` t ) )
61	60	breq2d	|- ( h = g -> ( 0 <_ ( h ` t ) <-> 0 <_ ( g ` t ) ) )
62	60	breq1d	|- ( h = g -> ( ( h ` t ) <_ 1 <-> ( g ` t ) <_ 1 ) )
63	61 62	anbi12d	|- ( h = g -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) )
64	63	ralbidv	|- ( h = g -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) )
65	59 64	anbi12d	|- ( h = g -> ( ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) <-> ( ( g ` Z ) = 0 /\ A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) ) )
66	65	elrab	|- ( g e. { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } <-> ( g e. A /\ ( ( g ` Z ) = 0 /\ A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) ) )
67	57 66	sylib	|- ( ( ph /\ g e. Q ) -> ( g e. A /\ ( ( g ` Z ) = 0 /\ A. t e. T ( 0 <_ ( g ` t ) /\ ( g ` t ) <_ 1 ) ) ) )
68	67	simpld	|- ( ( ph /\ g e. Q ) -> g e. A )
69	55 68	sseldd	|- ( ( ph /\ g e. Q ) -> g e. ( J Cn K ) )
70	69	ad2ant2r	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> g e. ( J Cn K ) )
71		nfcv	|- F/_ t 0
72		nfcv	|- F/_ t g
73		nfv	|- F/ t g e. ( J Cn K )
74	4 73	nfan	|- F/ t ( ph /\ g e. ( J Cn K ) )
75		eqid	|- { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( g ` t ) }
76		0xr	|- 0 e. RR*
77	76	a1i	|- ( ( ph /\ g e. ( J Cn K ) ) -> 0 e. RR* )
78		simpr	|- ( ( ph /\ g e. ( J Cn K ) ) -> g e. ( J Cn K ) )
79	71 72 74 5 8 75 77 78	rfcnpre1	|- ( ( ph /\ g e. ( J Cn K ) ) -> { t e. T | 0 < ( g ` t ) } e. J )
80	54 70 79	syl2anc	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> { t e. T | 0 < ( g ` t ) } e. J )
81		eqidd	|- ( ( ph /\ g e. Q ) -> { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( g ` t ) } )
82		nfv	|- F/ h { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( g ` t ) }
83		nfcv	|- F/_ h g
84	60	breq2d	|- ( h = g -> ( 0 < ( h ` t ) <-> 0 < ( g ` t ) ) )
85	84	rabbidv	|- ( h = g -> { t e. T | 0 < ( h ` t ) } = { t e. T | 0 < ( g ` t ) } )
86	85	eqeq2d	|- ( h = g -> ( { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } <-> { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( g ` t ) } ) )
87	82 83 2 86	rspcegf	|- ( ( g e. Q /\ { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( g ` t ) } ) -> E. h e. Q { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } )
88	56 81 87	syl2anc	|- ( ( ph /\ g e. Q ) -> E. h e. Q { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } )
89	88	ad2ant2r	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> E. h e. Q { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } )
90		eqeq1	|- ( w = { t e. T | 0 < ( g ` t ) } -> ( w = { t e. T | 0 < ( h ` t ) } <-> { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } ) )
91	90	rexbidv	|- ( w = { t e. T | 0 < ( g ` t ) } -> ( E. h e. Q w = { t e. T | 0 < ( h ` t ) } <-> E. h e. Q { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } ) )
92	91	elrab	|- ( { t e. T | 0 < ( g ` t ) } e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } <-> ( { t e. T | 0 < ( g ` t ) } e. J /\ E. h e. Q { t e. T | 0 < ( g ` t ) } = { t e. T | 0 < ( h ` t ) } ) )
93	80 89 92	sylanbrc	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> { t e. T | 0 < ( g ` t ) } e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } )
94	93 7	eleqtrrdi	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> { t e. T | 0 < ( g ` t ) } e. W )
95		nfcv	|- F/_ w { t e. T | 0 < ( g ` t ) }
96		nfv	|- F/ w s e. { t e. T | 0 < ( g ` t ) }
97		nfrab1	|- F/_ w { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
98	7 97	nfcxfr	|- F/_ w W
99	98	nfel2	|- F/ w { t e. T | 0 < ( g ` t ) } e. W
100	96 99	nfan	|- F/ w ( s e. { t e. T | 0 < ( g ` t ) } /\ { t e. T | 0 < ( g ` t ) } e. W )
101		eleq2	|- ( w = { t e. T | 0 < ( g ` t ) } -> ( s e. w <-> s e. { t e. T | 0 < ( g ` t ) } ) )
102		eleq1	|- ( w = { t e. T | 0 < ( g ` t ) } -> ( w e. W <-> { t e. T | 0 < ( g ` t ) } e. W ) )
103	101 102	anbi12d	|- ( w = { t e. T | 0 < ( g ` t ) } -> ( ( s e. w /\ w e. W ) <-> ( s e. { t e. T | 0 < ( g ` t ) } /\ { t e. T | 0 < ( g ` t ) } e. W ) ) )
104	95 100 103	spcegf	|- ( { t e. T | 0 < ( g ` t ) } e. _V -> ( ( s e. { t e. T | 0 < ( g ` t ) } /\ { t e. T | 0 < ( g ` t ) } e. W ) -> E. w ( s e. w /\ w e. W ) ) )
105	104	imp	|- ( ( { t e. T | 0 < ( g ` t ) } e. _V /\ ( s e. { t e. T | 0 < ( g ` t ) } /\ { t e. T | 0 < ( g ` t ) } e. W ) ) -> E. w ( s e. w /\ w e. W ) )
106	46 53 94 105	syl12anc	|- ( ( ( ph /\ s e. ( T \ U ) ) /\ ( g e. Q /\ 0 < ( g ` s ) ) ) -> E. w ( s e. w /\ w e. W ) )
107	43 106	exlimddv	|- ( ( ph /\ s e. ( T \ U ) ) -> E. w ( s e. w /\ w e. W ) )
108		nfcv	|- F/_ w s
109	108 98	elunif	|- ( s e. U. W <-> E. w ( s e. w /\ w e. W ) )
110	107 109	sylibr	|- ( ( ph /\ s e. ( T \ U ) ) -> s e. U. W )
111	110	ex	|- ( ph -> ( s e. ( T \ U ) -> s e. U. W ) )
112	111	ssrdv	|- ( ph -> ( T \ U ) C_ U. W )