Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <_ p <_ 1 , p__(t_0) = 0, and 0 < p on T \ U . (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem53.1 | |
|
stoweidlem53.2 | |
||
stoweidlem53.3 | |
||
stoweidlem53.4 | |
||
stoweidlem53.5 | |
||
stoweidlem53.6 | |
||
stoweidlem53.7 | |
||
stoweidlem53.8 | |
||
stoweidlem53.9 | |
||
stoweidlem53.10 | |
||
stoweidlem53.11 | |
||
stoweidlem53.12 | |
||
stoweidlem53.13 | |
||
stoweidlem53.14 | |
||
stoweidlem53.15 | |
||
stoweidlem53.16 | |
||
Assertion | stoweidlem53 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoweidlem53.1 | |
|
2 | stoweidlem53.2 | |
|
3 | stoweidlem53.3 | |
|
4 | stoweidlem53.4 | |
|
5 | stoweidlem53.5 | |
|
6 | stoweidlem53.6 | |
|
7 | stoweidlem53.7 | |
|
8 | stoweidlem53.8 | |
|
9 | stoweidlem53.9 | |
|
10 | stoweidlem53.10 | |
|
11 | stoweidlem53.11 | |
|
12 | stoweidlem53.12 | |
|
13 | stoweidlem53.13 | |
|
14 | stoweidlem53.14 | |
|
15 | stoweidlem53.15 | |
|
16 | stoweidlem53.16 | |
|
17 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 | stoweidlem50 | |
18 | nfv | |
|
19 | nfcv | |
|
20 | nfv | |
|
21 | nfra1 | |
|
22 | 20 21 | nfan | |
23 | nfcv | |
|
24 | 22 23 | nfrabw | |
25 | 4 24 | nfcxfr | |
26 | nfrab1 | |
|
27 | 26 | nfeq2 | |
28 | 25 27 | nfrex | |
29 | nfcv | |
|
30 | 28 29 | nfrabw | |
31 | 5 30 | nfcxfr | |
32 | 19 31 | nfss | |
33 | nfcv | |
|
34 | 33 1 | nfdif | |
35 | nfcv | |
|
36 | 34 35 | nfss | |
37 | 18 32 36 | nf3an | |
38 | 2 37 | nfan | |
39 | nfv | |
|
40 | nfv | |
|
41 | nfcv | |
|
42 | nfrab1 | |
|
43 | 5 42 | nfcxfr | |
44 | 41 43 | nfss | |
45 | nfv | |
|
46 | 40 44 45 | nf3an | |
47 | 39 46 | nfan | |
48 | nfv | |
|
49 | nfv | |
|
50 | nfcv | |
|
51 | nfre1 | |
|
52 | nfcv | |
|
53 | 51 52 | nfrabw | |
54 | 5 53 | nfcxfr | |
55 | 50 54 | nfss | |
56 | nfv | |
|
57 | 49 55 56 | nf3an | |
58 | 48 57 | nfan | |
59 | eqid | |
|
60 | cmptop | |
|
61 | 8 60 | syl | |
62 | retop | |
|
63 | 3 62 | eqeltri | |
64 | cnfex | |
|
65 | 61 63 64 | sylancl | |
66 | 9 7 | sseqtrdi | |
67 | 65 66 | ssexd | |
68 | 67 | adantr | |
69 | simpr1 | |
|
70 | simpr2 | |
|
71 | simpr3 | |
|
72 | 15 | adantr | |
73 | 38 47 58 4 5 59 68 69 70 71 72 | stoweidlem35 | |
74 | 17 73 | exlimddv | |
75 | nfv | |
|
76 | nfv | |
|
77 | nfv | |
|
78 | nfcv | |
|
79 | nfre1 | |
|
80 | 78 79 | nfralw | |
81 | 77 80 | nfan | |
82 | 76 81 | nfan | |
83 | 75 82 | nfan | |
84 | nfv | |
|
85 | nfcv | |
|
86 | nfcv | |
|
87 | 85 86 25 | nff | |
88 | nfra1 | |
|
89 | 87 88 | nfan | |
90 | 84 89 | nfan | |
91 | 2 90 | nfan | |
92 | eqid | |
|
93 | simprl | |
|
94 | simprrl | |
|
95 | simprrr | |
|
96 | 66 | adantr | |
97 | 10 | 3adant1r | |
98 | 11 | 3adant1r | |
99 | 12 | adantlr | |
100 | elssuni | |
|
101 | 100 6 | sseqtrrdi | |
102 | 14 101 | syl | |
103 | 102 16 | sseldd | |
104 | 103 | adantr | |
105 | 83 91 3 4 92 93 94 95 6 96 97 98 99 104 | stoweidlem44 | |
106 | 105 | ex | |
107 | 106 | exlimdvv | |
108 | 74 107 | mpd | |