Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β π΄ β π) |
2 | | metdscn.f |
. . . . 5
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
3 | 2 | metdsval 24213 |
. . . 4
β’ (π΄ β π β (πΉβπ΄) = inf(ran (π¦ β π β¦ (π΄π·π¦)), β*, <
)) |
4 | 1, 3 | syl 17 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β (πΉβπ΄) = inf(ran (π¦ β π β¦ (π΄π·π¦)), β*, <
)) |
5 | 4 | breq2d 5118 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β (π
β€ (πΉβπ΄) β π
β€ inf(ran (π¦ β π β¦ (π΄π·π¦)), β*, <
))) |
6 | | simpll1 1213 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β π· β (βMetβπ)) |
7 | 1 | adantr 482 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β π΄ β π) |
8 | | simpl2 1193 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β π β π) |
9 | 8 | sselda 3945 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β π€ β π) |
10 | | xmetcl 23687 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π€ β π) β (π΄π·π€) β
β*) |
11 | 6, 7, 9, 10 | syl3anc 1372 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β (π΄π·π€) β
β*) |
12 | | oveq2 7366 |
. . . . . 6
β’ (π¦ = π€ β (π΄π·π¦) = (π΄π·π€)) |
13 | 12 | cbvmptv 5219 |
. . . . 5
β’ (π¦ β π β¦ (π΄π·π¦)) = (π€ β π β¦ (π΄π·π€)) |
14 | 11, 13 | fmptd 7063 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β (π¦ β π β¦ (π΄π·π¦)):πβΆβ*) |
15 | 14 | frnd 6677 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β ran
(π¦ β π β¦ (π΄π·π¦)) β
β*) |
16 | | simpr 486 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β π
β
β*) |
17 | | infxrgelb 13255 |
. . 3
β’ ((ran
(π¦ β π β¦ (π΄π·π¦)) β β* β§ π
β β*)
β (π
β€ inf(ran
(π¦ β π β¦ (π΄π·π¦)), β*, < ) β
βπ§ β ran (π¦ β π β¦ (π΄π·π¦))π
β€ π§)) |
18 | 15, 16, 17 | syl2anc 585 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β (π
β€ inf(ran (π¦ β π β¦ (π΄π·π¦)), β*, < ) β
βπ§ β ran (π¦ β π β¦ (π΄π·π¦))π
β€ π§)) |
19 | 16 | adantr 482 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β π
β
β*) |
20 | | elbl2 23746 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π
β β*) β§ (π΄ β π β§ π€ β π)) β (π€ β (π΄(ballβπ·)π
) β (π΄π·π€) < π
)) |
21 | 6, 19, 7, 9, 20 | syl22anc 838 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β (π€ β (π΄(ballβπ·)π
) β (π΄π·π€) < π
)) |
22 | | xrltnle 11223 |
. . . . . . 7
β’ (((π΄π·π€) β β* β§ π
β β*)
β ((π΄π·π€) < π
β Β¬ π
β€ (π΄π·π€))) |
23 | 11, 19, 22 | syl2anc 585 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β ((π΄π·π€) < π
β Β¬ π
β€ (π΄π·π€))) |
24 | 21, 23 | bitrd 279 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β (π€ β (π΄(ballβπ·)π
) β Β¬ π
β€ (π΄π·π€))) |
25 | 24 | con2bid 355 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β§ π€ β π) β (π
β€ (π΄π·π€) β Β¬ π€ β (π΄(ballβπ·)π
))) |
26 | 25 | ralbidva 3173 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β
(βπ€ β π π
β€ (π΄π·π€) β βπ€ β π Β¬ π€ β (π΄(ballβπ·)π
))) |
27 | | ovex 7391 |
. . . . 5
β’ (π΄π·π€) β V |
28 | 27 | rgenw 3069 |
. . . 4
β’
βπ€ β
π (π΄π·π€) β V |
29 | | breq2 5110 |
. . . . 5
β’ (π§ = (π΄π·π€) β (π
β€ π§ β π
β€ (π΄π·π€))) |
30 | 13, 29 | ralrnmptw 7045 |
. . . 4
β’
(βπ€ β
π (π΄π·π€) β V β (βπ§ β ran (π¦ β π β¦ (π΄π·π¦))π
β€ π§ β βπ€ β π π
β€ (π΄π·π€))) |
31 | 28, 30 | ax-mp 5 |
. . 3
β’
(βπ§ β
ran (π¦ β π β¦ (π΄π·π¦))π
β€ π§ β βπ€ β π π
β€ (π΄π·π€)) |
32 | | disj 4408 |
. . 3
β’ ((π β© (π΄(ballβπ·)π
)) = β
β βπ€ β π Β¬ π€ β (π΄(ballβπ·)π
)) |
33 | 26, 31, 32 | 3bitr4g 314 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β
(βπ§ β ran
(π¦ β π β¦ (π΄π·π¦))π
β€ π§ β (π β© (π΄(ballβπ·)π
)) = β
)) |
34 | 5, 18, 33 | 3bitrd 305 |
1
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π
β β*) β (π
β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)π
)) = β
)) |