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