Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . 3
β’ π½ = (MetOpenβπΆ) |
2 | | metcn.4 |
. . 3
β’ πΎ = (MetOpenβπ·) |
3 | 1, 2 | metcnp3 23912 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) |
4 | | ffun 6676 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β Fun πΉ) |
5 | 4 | ad2antlr 726 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β Fun πΉ) |
6 | | simpll1 1213 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β πΆ β
(βMetβπ)) |
7 | | simpll3 1215 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β π β π) |
8 | | rpxr 12931 |
. . . . . . . . . . 11
β’ (π§ β β+
β π§ β
β*) |
9 | 8 | ad2antll 728 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β π§ β
β*) |
10 | | blssm 23787 |
. . . . . . . . . 10
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β β*) β (π(ballβπΆ)π§) β π) |
11 | 6, 7, 9, 10 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (π(ballβπΆ)π§) β π) |
12 | | fdm 6682 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β dom πΉ = π) |
13 | 12 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β dom πΉ = π) |
14 | 11, 13 | sseqtrrd 3990 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (π(ballβπΆ)π§) β dom πΉ) |
15 | | funimass4 6912 |
. . . . . . . 8
β’ ((Fun
πΉ β§ (π(ballβπΆ)π§) β dom πΉ) β ((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ€ β (π(ballβπΆ)π§)(πΉβπ€) β ((πΉβπ)(ballβπ·)π¦))) |
16 | 5, 14, 15 | syl2anc 585 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β ((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ€ β (π(ballβπΆ)π§)(πΉβπ€) β ((πΉβπ)(ballβπ·)π¦))) |
17 | | elbl 23757 |
. . . . . . . . . . 11
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β β*) β (π€ β (π(ballβπΆ)π§) β (π€ β π β§ (ππΆπ€) < π§))) |
18 | 6, 7, 9, 17 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (π€ β (π(ballβπΆ)π§) β (π€ β π β§ (ππΆπ€) < π§))) |
19 | 18 | imbi1d 342 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β ((π€ β (π(ballβπΆ)π§) β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)) β ((π€ β π β§ (ππΆπ€) < π§) β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)))) |
20 | | impexp 452 |
. . . . . . . . . 10
β’ (((π€ β π β§ (ππΆπ€) < π§) β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)) β (π€ β π β ((ππΆπ€) < π§ β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)))) |
21 | | simpl2 1193 |
. . . . . . . . . . . . . 14
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β π· β (βMetβπ)) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π· β (βMetβπ)) |
23 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π¦ β β+) |
24 | 23 | rpxrd 12965 |
. . . . . . . . . . . . 13
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π¦ β β*) |
25 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β πΉ:πβΆπ) |
26 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π β π) |
27 | 25, 26 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (πΉβπ) β π) |
28 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β πΉ:πβΆπ) |
29 | 28 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (πΉβπ€) β π) |
30 | | elbl2 23759 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π¦ β β*) β§ ((πΉβπ) β π β§ (πΉβπ€) β π)) β ((πΉβπ€) β ((πΉβπ)(ballβπ·)π¦) β ((πΉβπ)π·(πΉβπ€)) < π¦)) |
31 | 22, 24, 27, 29, 30 | syl22anc 838 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β ((πΉβπ€) β ((πΉβπ)(ballβπ·)π¦) β ((πΉβπ)π·(πΉβπ€)) < π¦)) |
32 | 31 | imbi2d 341 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (((ππΆπ€) < π§ β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)) β ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
33 | 32 | pm5.74da 803 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β ((π€ β π β ((ππΆπ€) < π§ β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦))) β (π€ β π β ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
34 | 20, 33 | bitrid 283 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (((π€ β π β§ (ππΆπ€) < π§) β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)) β (π€ β π β ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
35 | 19, 34 | bitrd 279 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β ((π€ β (π(ballβπΆ)π§) β (πΉβπ€) β ((πΉβπ)(ballβπ·)π¦)) β (π€ β π β ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
36 | 35 | ralbidv2 3171 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (βπ€ β
(π(ballβπΆ)π§)(πΉβπ€) β ((πΉβπ)(ballβπ·)π¦) β βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
37 | 16, 36 | bitrd 279 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β ((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
38 | 37 | anassrs 469 |
. . . . 5
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ π§ β β+)
β ((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
39 | 38 | rexbidva 3174 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ§ β
β+ (πΉ
β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ§ β β+ βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
40 | 39 | ralbidva 3173 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦))) |
41 | 40 | pm5.32da 580 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β ((πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
42 | 3, 41 | bitrd 279 |
1
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |