Metamath Proof Explorer

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

Proof

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