Metamath Proof Explorer


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 _tU
stoweidlem46.2 _hQ
stoweidlem46.3 qφ
stoweidlem46.4 tφ
stoweidlem46.5 K=topGenran.
stoweidlem46.6 Q=hA|hZ=0tT0htht1
stoweidlem46.7 W=wJ|hQw=tT|0<ht
stoweidlem46.8 T=J
stoweidlem46.9 φJComp
stoweidlem46.10 φAJCnK
stoweidlem46.11 φfAgAtTft+gtA
stoweidlem46.12 φfAgAtTftgtA
stoweidlem46.13 φxtTxA
stoweidlem46.14 φrTtTrtqAqrqt
stoweidlem46.15 φUJ
stoweidlem46.16 φZU
stoweidlem46.17 φTV
Assertion stoweidlem46 φTUW

Proof

Step Hyp Ref Expression
1 stoweidlem46.1 _tU
2 stoweidlem46.2 _hQ
3 stoweidlem46.3 qφ
4 stoweidlem46.4 tφ
5 stoweidlem46.5 K=topGenran.
6 stoweidlem46.6 Q=hA|hZ=0tT0htht1
7 stoweidlem46.7 W=wJ|hQw=tT|0<ht
8 stoweidlem46.8 T=J
9 stoweidlem46.9 φJComp
10 stoweidlem46.10 φAJCnK
11 stoweidlem46.11 φfAgAtTft+gtA
12 stoweidlem46.12 φfAgAtTftgtA
13 stoweidlem46.13 φxtTxA
14 stoweidlem46.14 φrTtTrtqAqrqt
15 stoweidlem46.15 φUJ
16 stoweidlem46.16 φZU
17 stoweidlem46.17 φTV
18 nfv qsTU
19 3 18 nfan qφsTU
20 nfcv _tT
21 20 1 nfdif _tTU
22 21 nfel2 tsTU
23 4 22 nfan tφsTU
24 9 adantr φsTUJComp
25 10 adantr φsTUAJCnK
26 11 3adant1r φsTUfAgAtTft+gtA
27 12 3adant1r φsTUfAgAtTftgtA
28 13 adantlr φsTUxtTxA
29 14 adantlr φsTUrTtTrtqAqrqt
30 15 adantr φsTUUJ
31 16 adantr φsTUZU
32 simpr φsTUsTU
33 19 23 2 5 6 8 24 25 26 27 28 29 30 31 32 stoweidlem43 φsTUhhQ0<hs
34 nfv ghQ0<hs
35 2 nfel2 hgQ
36 nfv h0<gs
37 35 36 nfan hgQ0<gs
38 eleq1 h=ghQgQ
39 fveq1 h=ghs=gs
40 39 breq2d h=g0<hs0<gs
41 38 40 anbi12d h=ghQ0<hsgQ0<gs
42 34 37 41 cbvexv1 hhQ0<hsggQ0<gs
43 33 42 sylib φsTUggQ0<gs
44 rabexg TVtT|0<gtV
45 17 44 syl φtT|0<gtV
46 45 ad2antrr φsTUgQ0<gstT|0<gtV
47 eldifi sTUsT
48 47 ad2antlr φsTUgQ0<gssT
49 simprr φsTUgQ0<gs0<gs
50 fveq2 t=sgt=gs
51 50 breq2d t=s0<gt0<gs
52 51 elrab stT|0<gtsT0<gs
53 48 49 52 sylanbrc φsTUgQ0<gsstT|0<gt
54 simpll φsTUgQ0<gsφ
55 10 adantr φgQAJCnK
56 simpr φgQgQ
57 56 6 eleqtrdi φgQghA|hZ=0tT0htht1
58 fveq1 h=ghZ=gZ
59 58 eqeq1d h=ghZ=0gZ=0
60 fveq1 h=ght=gt
61 60 breq2d h=g0ht0gt
62 60 breq1d h=ght1gt1
63 61 62 anbi12d h=g0htht10gtgt1
64 63 ralbidv h=gtT0htht1tT0gtgt1
65 59 64 anbi12d h=ghZ=0tT0htht1gZ=0tT0gtgt1
66 65 elrab ghA|hZ=0tT0htht1gAgZ=0tT0gtgt1
67 57 66 sylib φgQgAgZ=0tT0gtgt1
68 67 simpld φgQgA
69 55 68 sseldd φgQgJCnK
70 69 ad2ant2r φsTUgQ0<gsgJCnK
71 nfcv _t0
72 nfcv _tg
73 nfv tgJCnK
74 4 73 nfan tφgJCnK
75 eqid tT|0<gt=tT|0<gt
76 0xr 0*
77 76 a1i φgJCnK0*
78 simpr φgJCnKgJCnK
79 71 72 74 5 8 75 77 78 rfcnpre1 φgJCnKtT|0<gtJ
80 54 70 79 syl2anc φsTUgQ0<gstT|0<gtJ
81 eqidd φgQtT|0<gt=tT|0<gt
82 nfv htT|0<gt=tT|0<gt
83 nfcv _hg
84 60 breq2d h=g0<ht0<gt
85 84 rabbidv h=gtT|0<ht=tT|0<gt
86 85 eqeq2d h=gtT|0<gt=tT|0<httT|0<gt=tT|0<gt
87 82 83 2 86 rspcegf gQtT|0<gt=tT|0<gthQtT|0<gt=tT|0<ht
88 56 81 87 syl2anc φgQhQtT|0<gt=tT|0<ht
89 88 ad2ant2r φsTUgQ0<gshQtT|0<gt=tT|0<ht
90 eqeq1 w=tT|0<gtw=tT|0<httT|0<gt=tT|0<ht
91 90 rexbidv w=tT|0<gthQw=tT|0<hthQtT|0<gt=tT|0<ht
92 91 elrab tT|0<gtwJ|hQw=tT|0<httT|0<gtJhQtT|0<gt=tT|0<ht
93 80 89 92 sylanbrc φsTUgQ0<gstT|0<gtwJ|hQw=tT|0<ht
94 93 7 eleqtrrdi φsTUgQ0<gstT|0<gtW
95 nfcv _wtT|0<gt
96 nfv wstT|0<gt
97 nfrab1 _wwJ|hQw=tT|0<ht
98 7 97 nfcxfr _wW
99 98 nfel2 wtT|0<gtW
100 96 99 nfan wstT|0<gttT|0<gtW
101 eleq2 w=tT|0<gtswstT|0<gt
102 eleq1 w=tT|0<gtwWtT|0<gtW
103 101 102 anbi12d w=tT|0<gtswwWstT|0<gttT|0<gtW
104 95 100 103 spcegf tT|0<gtVstT|0<gttT|0<gtWwswwW
105 104 imp tT|0<gtVstT|0<gttT|0<gtWwswwW
106 46 53 94 105 syl12anc φsTUgQ0<gswswwW
107 43 106 exlimddv φsTUwswwW
108 nfcv _ws
109 108 98 elunif sWwswwW
110 107 109 sylibr φsTUsW
111 110 ex φsTUsW
112 111 ssrdv φTUW