Step | Hyp | Ref
| Expression |
1 | | lmmbr.2 |
. . 3
β’ π½ = (MetOpenβπ·) |
2 | | lmmbr.3 |
. . 3
β’ (π β π· β (βMetβπ)) |
3 | 1, 2 | lmmbr 24645 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
4 | | df-3an 1090 |
. . . 4
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
5 | | uzf 12774 |
. . . . . . . . . 10
β’
β€β₯:β€βΆπ« β€ |
6 | | ffn 6672 |
. . . . . . . . . 10
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
7 | | reseq2 5936 |
. . . . . . . . . . . 12
β’ (π¦ =
(β€β₯βπ) β (πΉ βΎ π¦) = (πΉ βΎ (β€β₯βπ))) |
8 | | id 22 |
. . . . . . . . . . . 12
β’ (π¦ =
(β€β₯βπ) β π¦ = (β€β₯βπ)) |
9 | 7, 8 | feq12d 6660 |
. . . . . . . . . . 11
β’ (π¦ =
(β€β₯βπ) β ((πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯))) |
10 | 9 | rexrn 7041 |
. . . . . . . . . 10
β’
(β€β₯ Fn β€ β (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯))) |
11 | 5, 6, 10 | mp2b 10 |
. . . . . . . . 9
β’
(βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯)) |
12 | | simp2l 1200 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β πΉ β (π βpm
β)) |
13 | | elfvdm 6883 |
. . . . . . . . . . . . . . . 16
β’ (π· β (βMetβπ) β π β dom βMet) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β π β dom
βMet) |
15 | | cnex 11140 |
. . . . . . . . . . . . . . 15
β’ β
β V |
16 | | elpmg 8787 |
. . . . . . . . . . . . . . 15
β’ ((π β dom βMet β§
β β V) β (πΉ
β (π
βpm β) β (Fun πΉ β§ πΉ β (β Γ π)))) |
17 | 14, 15, 16 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β (πΉ β (π βpm β) β (Fun
πΉ β§ πΉ β (β Γ π)))) |
18 | 12, 17 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β (Fun
πΉ β§ πΉ β (β Γ π))) |
19 | 18 | simpld 496 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β Fun πΉ) |
20 | | ffvresb 7076 |
. . . . . . . . . . . 12
β’ (Fun
πΉ β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(ballβπ·)π₯)))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(ballβπ·)π₯)))) |
22 | | rpxr 12932 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β+
β π₯ β
β*) |
23 | | elbl 23764 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β*) β ((πΉβπ) β (π(ballβπ·)π₯) β ((πΉβπ) β π β§ (ππ·(πΉβπ)) < π₯))) |
24 | 22, 23 | syl3an3 1166 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β ((πΉβπ) β (π(ballβπ·)π₯) β ((πΉβπ) β π β§ (ππ·(πΉβπ)) < π₯))) |
25 | | xmetsym 23723 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (βMetβπ) β§ π β π β§ (πΉβπ) β π) β (ππ·(πΉβπ)) = ((πΉβπ)π·π)) |
26 | 25 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (βMetβπ) β§ π β π β§ (πΉβπ) β π) β ((ππ·(πΉβπ)) < π₯ β ((πΉβπ)π·π) < π₯)) |
27 | 26 | 3expa 1119 |
. . . . . . . . . . . . . . . . . 18
β’ (((π· β (βMetβπ) β§ π β π) β§ (πΉβπ) β π) β ((ππ·(πΉβπ)) < π₯ β ((πΉβπ)π·π) < π₯)) |
28 | 27 | pm5.32da 580 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (βMetβπ) β§ π β π) β (((πΉβπ) β π β§ (ππ·(πΉβπ)) < π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
29 | 28 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β (((πΉβπ) β π β§ (ππ·(πΉβπ)) < π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
30 | 24, 29 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β ((πΉβπ) β (π(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
31 | 30 | 3adant2l 1179 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β ((πΉβπ) β (π(ballβπ·)π₯) β ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
32 | 31 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β ((π β dom πΉ β§ (πΉβπ) β (π(ballβπ·)π₯)) β (π β dom πΉ β§ ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
33 | | 3anass 1096 |
. . . . . . . . . . . . 13
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯) β (π β dom πΉ β§ ((πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
34 | 32, 33 | bitr4di 289 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β ((π β dom πΉ β§ (πΉβπ) β (π(ballβπ·)π₯)) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
35 | 34 | ralbidv 3171 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β (π(ballβπ·)π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
36 | 21, 35 | bitrd 279 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β ((πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
37 | 36 | rexbidv 3172 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β
(βπ β β€
(πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(π(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
38 | 11, 37 | bitrid 283 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π) β§ π₯ β β+) β
(βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
39 | 38 | 3expa 1119 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ π₯ β β+) β
(βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
40 | 39 | ralbidva 3169 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β (βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
41 | 40 | pm5.32da 580 |
. . . . 5
β’ (π· β (βMetβπ) β (((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
42 | 2, 41 | syl 17 |
. . . 4
β’ (π β (((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
43 | 4, 42 | bitrid 283 |
. . 3
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
44 | | df-3an 1090 |
. . 3
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
45 | 43, 44 | bitr4di 289 |
. 2
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
46 | 3, 45 | bitrd 279 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |