Step | Hyp | Ref
| Expression |
1 | | stoweidlem62.4 |
. . . . 5
β’ π» = (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
2 | | nfmpt1 5211 |
. . . . 5
β’
β²π‘(π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
3 | 1, 2 | nfcxfr 2903 |
. . . 4
β’
β²π‘π» |
4 | | stoweidlem62.3 |
. . . 4
β’
β²π‘π |
5 | | stoweidlem62.5 |
. . . 4
β’ πΎ = (topGenβran
(,)) |
6 | | stoweidlem62.7 |
. . . 4
β’ (π β π½ β Comp) |
7 | | stoweidlem62.6 |
. . . 4
β’ π = βͺ
π½ |
8 | | stoweidlem62.16 |
. . . 4
β’ (π β π β β
) |
9 | | stoweidlem62.8 |
. . . 4
β’ πΆ = (π½ Cn πΎ) |
10 | | stoweidlem62.9 |
. . . 4
β’ (π β π΄ β πΆ) |
11 | | eleq1w 2820 |
. . . . . . 7
β’ (π = β β (π β π΄ β β β π΄)) |
12 | 11 | 3anbi3d 1442 |
. . . . . 6
β’ (π = β β ((π β§ π β π΄ β§ π β π΄) β (π β§ π β π΄ β§ β β π΄))) |
13 | | fveq1 6838 |
. . . . . . . . 9
β’ (π = β β (πβπ‘) = (ββπ‘)) |
14 | 13 | oveq2d 7369 |
. . . . . . . 8
β’ (π = β β ((πβπ‘) + (πβπ‘)) = ((πβπ‘) + (ββπ‘))) |
15 | 14 | mpteq2dv 5205 |
. . . . . . 7
β’ (π = β β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) + (ββπ‘)))) |
16 | 15 | eleq1d 2822 |
. . . . . 6
β’ (π = β β ((π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄ β (π‘ β π β¦ ((πβπ‘) + (ββπ‘))) β π΄)) |
17 | 12, 16 | imbi12d 344 |
. . . . 5
β’ (π = β β (((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) β ((π β§ π β π΄ β§ β β π΄) β (π‘ β π β¦ ((πβπ‘) + (ββπ‘))) β π΄))) |
18 | | stoweidlem62.10 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
19 | 17, 18 | chvarvv 2002 |
. . . 4
β’ ((π β§ π β π΄ β§ β β π΄) β (π‘ β π β¦ ((πβπ‘) + (ββπ‘))) β π΄) |
20 | 13 | oveq2d 7369 |
. . . . . . . 8
β’ (π = β β ((πβπ‘) Β· (πβπ‘)) = ((πβπ‘) Β· (ββπ‘))) |
21 | 20 | mpteq2dv 5205 |
. . . . . . 7
β’ (π = β β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((πβπ‘) Β· (ββπ‘)))) |
22 | 21 | eleq1d 2822 |
. . . . . 6
β’ (π = β β ((π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄ β (π‘ β π β¦ ((πβπ‘) Β· (ββπ‘))) β π΄)) |
23 | 12, 22 | imbi12d 344 |
. . . . 5
β’ (π = β β (((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β ((π β§ π β π΄ β§ β β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (ββπ‘))) β π΄))) |
24 | | stoweidlem62.11 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
25 | 23, 24 | chvarvv 2002 |
. . . 4
β’ ((π β§ π β π΄ β§ β β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (ββπ‘))) β π΄) |
26 | | stoweidlem62.12 |
. . . 4
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
27 | | stoweidlem62.13 |
. . . 4
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
28 | | stoweidlem62.1 |
. . . . . 6
β’
β²π‘πΉ |
29 | 28 | nfrn 5905 |
. . . . . . 7
β’
β²π‘ran
πΉ |
30 | | nfcv 2905 |
. . . . . . 7
β’
β²π‘β |
31 | | nfcv 2905 |
. . . . . . 7
β’
β²π‘
< |
32 | 29, 30, 31 | nfinf 9414 |
. . . . . 6
β’
β²π‘inf(ran πΉ, β, < ) |
33 | | eqid 2736 |
. . . . . 6
β’ (π Γ {-inf(ran πΉ, β, < )}) = (π Γ {-inf(ran πΉ, β, <
)}) |
34 | | cmptop 22730 |
. . . . . . 7
β’ (π½ β Comp β π½ β Top) |
35 | 6, 34 | syl 17 |
. . . . . 6
β’ (π β π½ β Top) |
36 | | stoweidlem62.14 |
. . . . . 6
β’ (π β πΉ β πΆ) |
37 | 36, 9 | eleqtrdi 2848 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn πΎ)) |
38 | 28, 4, 7, 5, 6, 37,
8 | stoweidlem29 44202 |
. . . . . . 7
β’ (π β (inf(ran πΉ, β, < ) β ran πΉ β§ inf(ran πΉ, β, < ) β β β§
βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘))) |
39 | 38 | simp2d 1143 |
. . . . . 6
β’ (π β inf(ran πΉ, β, < ) β
β) |
40 | 28, 32, 4, 7, 33, 5,
35, 9, 36, 39 | stoweidlem47 44220 |
. . . . 5
β’ (π β (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) β πΆ) |
41 | 1, 40 | eqeltrid 2842 |
. . . 4
β’ (π β π» β πΆ) |
42 | 38 | simp3d 1144 |
. . . . . . . . 9
β’ (π β βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘)) |
43 | 42 | r19.21bi 3232 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β inf(ran πΉ, β, < ) β€ (πΉβπ‘)) |
44 | 5, 7, 9, 36 | fcnre 43172 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆβ) |
45 | 44 | ffvelcdmda 7031 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
46 | 39 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β inf(ran πΉ, β, < ) β
β) |
47 | 45, 46 | subge0d 11741 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (0 β€ ((πΉβπ‘) β inf(ran πΉ, β, < )) β inf(ran πΉ, β, < ) β€ (πΉβπ‘))) |
48 | 43, 47 | mpbird 256 |
. . . . . . 7
β’ ((π β§ π‘ β π) β 0 β€ ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
49 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π‘ β π) |
50 | 45, 46 | resubcld 11579 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((πΉβπ‘) β inf(ran πΉ, β, < )) β
β) |
51 | 1 | fvmpt2 6956 |
. . . . . . . 8
β’ ((π‘ β π β§ ((πΉβπ‘) β inf(ran πΉ, β, < )) β β) β
(π»βπ‘) = ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
52 | 49, 50, 51 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (π»βπ‘) = ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
53 | 48, 52 | breqtrrd 5131 |
. . . . . 6
β’ ((π β§ π‘ β π) β 0 β€ (π»βπ‘)) |
54 | 53 | ex 413 |
. . . . 5
β’ (π β (π‘ β π β 0 β€ (π»βπ‘))) |
55 | 4, 54 | ralrimi 3238 |
. . . 4
β’ (π β βπ‘ β π 0 β€ (π»βπ‘)) |
56 | | stoweidlem62.15 |
. . . . 5
β’ (π β πΈ β
β+) |
57 | 56 | rphalfcld 12961 |
. . . 4
β’ (π β (πΈ / 2) β
β+) |
58 | 56 | rpred 12949 |
. . . . . 6
β’ (π β πΈ β β) |
59 | 58 | rehalfcld 12396 |
. . . . 5
β’ (π β (πΈ / 2) β β) |
60 | | 3re 12229 |
. . . . . . 7
β’ 3 β
β |
61 | | 3ne0 12255 |
. . . . . . 7
β’ 3 β
0 |
62 | 60, 61 | rereccli 11916 |
. . . . . 6
β’ (1 / 3)
β β |
63 | 62 | a1i 11 |
. . . . 5
β’ (π β (1 / 3) β
β) |
64 | | rphalflt 12936 |
. . . . . 6
β’ (πΈ β β+
β (πΈ / 2) < πΈ) |
65 | 56, 64 | syl 17 |
. . . . 5
β’ (π β (πΈ / 2) < πΈ) |
66 | | stoweidlem62.17 |
. . . . 5
β’ (π β πΈ < (1 / 3)) |
67 | 59, 58, 63, 65, 66 | lttrd 11312 |
. . . 4
β’ (π β (πΈ / 2) < (1 / 3)) |
68 | 3, 4, 5, 6, 7, 8, 9, 10, 19, 25, 26, 27, 41, 55, 57, 67 | stoweidlem61 44234 |
. . 3
β’ (π β ββ β π΄ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2))) |
69 | | nfra1 3265 |
. . . . . . 7
β’
β²π‘βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) |
70 | 4, 69 | nfan 1902 |
. . . . . 6
β’
β²π‘(π β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2))) |
71 | | rsp 3228 |
. . . . . . 7
β’
(βπ‘ β
π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) β (π‘ β π β (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)))) |
72 | 56 | rpcnd 12951 |
. . . . . . . . . 10
β’ (π β πΈ β β) |
73 | | 2cnd 12227 |
. . . . . . . . . 10
β’ (π β 2 β
β) |
74 | | 2ne0 12253 |
. . . . . . . . . . 11
β’ 2 β
0 |
75 | 74 | a1i 11 |
. . . . . . . . . 10
β’ (π β 2 β 0) |
76 | 72, 73, 75 | divcan2d 11929 |
. . . . . . . . 9
β’ (π β (2 Β· (πΈ / 2)) = πΈ) |
77 | 76 | breq2d 5115 |
. . . . . . . 8
β’ (π β ((absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) β (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
78 | 77 | biimpd 228 |
. . . . . . 7
β’ (π β ((absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) β (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
79 | 71, 78 | sylan9r 509 |
. . . . . 6
β’ ((π β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2))) β (π‘ β π β (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
80 | 70, 79 | ralrimi 3238 |
. . . . 5
β’ ((π β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2))) β βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
81 | 80 | ex 413 |
. . . 4
β’ (π β (βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) β βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
82 | 81 | reximdv 3165 |
. . 3
β’ (π β (ββ β π΄ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < (2 Β· (πΈ / 2)) β ββ β π΄ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
83 | 68, 82 | mpd 15 |
. 2
β’ (π β ββ β π΄ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
84 | | nfmpt1 5211 |
. . 3
β’
β²π‘(π‘ β π β¦ ((ββπ‘) + inf(ran πΉ, β, < ))) |
85 | | nfcv 2905 |
. . 3
β’
β²π‘β |
86 | | nfv 1917 |
. . . . 5
β’
β²π‘ β β π΄ |
87 | | nfra1 3265 |
. . . . 5
β’
β²π‘βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ |
88 | 86, 87 | nfan 1902 |
. . . 4
β’
β²π‘(β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
89 | 4, 88 | nfan 1902 |
. . 3
β’
β²π‘(π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) |
90 | | eqid 2736 |
. . 3
β’ (π‘ β π β¦ ((ββπ‘) + inf(ran πΉ, β, < ))) = (π‘ β π β¦ ((ββπ‘) + inf(ran πΉ, β, < ))) |
91 | 44 | adantr 481 |
. . 3
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β πΉ:πβΆβ) |
92 | 39 | adantr 481 |
. . 3
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β inf(ran πΉ, β, < ) β
β) |
93 | 18 | 3adant1r 1177 |
. . 3
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
94 | 26 | adantlr 713 |
. . 3
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
95 | | stoweidlem62.2 |
. . . . 5
β’
β²ππ |
96 | 10 | sseld 3941 |
. . . . . . . 8
β’ (π β (π β π΄ β π β πΆ)) |
97 | 9 | eleq2i 2829 |
. . . . . . . 8
β’ (π β πΆ β π β (π½ Cn πΎ)) |
98 | 96, 97 | syl6ib 250 |
. . . . . . 7
β’ (π β (π β π΄ β π β (π½ Cn πΎ))) |
99 | | eqid 2736 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
100 | | uniretop 24110 |
. . . . . . . . 9
β’ β =
βͺ (topGenβran (,)) |
101 | 5 | unieqi 4876 |
. . . . . . . . 9
β’ βͺ πΎ =
βͺ (topGenβran (,)) |
102 | 100, 101 | eqtr4i 2767 |
. . . . . . . 8
β’ β =
βͺ πΎ |
103 | 99, 102 | cnf 22581 |
. . . . . . 7
β’ (π β (π½ Cn πΎ) β π:βͺ π½βΆβ) |
104 | 98, 103 | syl6 35 |
. . . . . 6
β’ (π β (π β π΄ β π:βͺ π½βΆβ)) |
105 | | feq2 6647 |
. . . . . . 7
β’ (π = βͺ
π½ β (π:πβΆβ β π:βͺ π½βΆβ)) |
106 | 7, 105 | mp1i 13 |
. . . . . 6
β’ (π β (π:πβΆβ β π:βͺ π½βΆβ)) |
107 | 104, 106 | sylibrd 258 |
. . . . 5
β’ (π β (π β π΄ β π:πβΆβ)) |
108 | 95, 107 | ralrimi 3238 |
. . . 4
β’ (π β βπ β π΄ π:πβΆβ) |
109 | 108 | adantr 481 |
. . 3
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β βπ β π΄ π:πβΆβ) |
110 | | simprl 769 |
. . 3
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β β β π΄) |
111 | 52 | eqcomd 2742 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πΉβπ‘) β inf(ran πΉ, β, < )) = (π»βπ‘)) |
112 | 111 | oveq2d 7369 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < ))) = ((ββπ‘) β (π»βπ‘))) |
113 | 112 | fveq2d 6843 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (absβ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < )))) = (absβ((ββπ‘) β (π»βπ‘)))) |
114 | 113 | adantlr 713 |
. . . . . 6
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π‘ β π) β (absβ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < )))) = (absβ((ββπ‘) β (π»βπ‘)))) |
115 | | simplrr 776 |
. . . . . . 7
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π‘ β π) β βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
116 | | rspa 3229 |
. . . . . . 7
β’
((βπ‘ β
π (absβ((ββπ‘) β (π»βπ‘))) < πΈ β§ π‘ β π) β (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
117 | 115, 116 | sylancom 588 |
. . . . . 6
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π‘ β π) β (absβ((ββπ‘) β (π»βπ‘))) < πΈ) |
118 | 114, 117 | eqbrtrd 5125 |
. . . . 5
β’ (((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β§ π‘ β π) β (absβ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < )))) < πΈ) |
119 | 118 | ex 413 |
. . . 4
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β (π‘ β π β (absβ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < )))) < πΈ)) |
120 | 89, 119 | ralrimi 3238 |
. . 3
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β βπ‘ β π (absβ((ββπ‘) β ((πΉβπ‘) β inf(ran πΉ, β, < )))) < πΈ) |
121 | 84, 85, 32, 89, 90, 91, 92, 93, 94, 109, 110, 120 | stoweidlem21 44194 |
. 2
β’ ((π β§ (β β π΄ β§ βπ‘ β π (absβ((ββπ‘) β (π»βπ‘))) < πΈ)) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |
122 | 83, 121 | rexlimddv 3156 |
1
β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |