Step | Hyp | Ref
| Expression |
1 | | isbnd3 36955 |
. 2
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
2 | | metf 24056 |
. . . . . . 7
β’ (π β (Metβπ) β π:(π Γ π)βΆβ) |
3 | 2 | adantr 481 |
. . . . . 6
β’ ((π β (Metβπ) β§ π₯ β β) β π:(π Γ π)βΆβ) |
4 | | ffn 6717 |
. . . . . 6
β’ (π:(π Γ π)βΆβ β π Fn (π Γ π)) |
5 | | ffnov 7537 |
. . . . . . 7
β’ (π:(π Γ π)βΆ(0[,]π₯) β (π Fn (π Γ π) β§ βπ¦ β π βπ§ β π (π¦ππ§) β (0[,]π₯))) |
6 | 5 | baib 536 |
. . . . . 6
β’ (π Fn (π Γ π) β (π:(π Γ π)βΆ(0[,]π₯) β βπ¦ β π βπ§ β π (π¦ππ§) β (0[,]π₯))) |
7 | 3, 4, 6 | 3syl 18 |
. . . . 5
β’ ((π β (Metβπ) β§ π₯ β β) β (π:(π Γ π)βΆ(0[,]π₯) β βπ¦ β π βπ§ β π (π¦ππ§) β (0[,]π₯))) |
8 | | 0red 11221 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π₯ β β) β§ (π¦ β π β§ π§ β π)) β 0 β β) |
9 | | simplr 767 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π₯ β β) β§ (π¦ β π β§ π§ β π)) β π₯ β β) |
10 | | metcl 24058 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ π¦ β π β§ π§ β π) β (π¦ππ§) β β) |
11 | 10 | 3expb 1120 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π¦ β π β§ π§ β π)) β (π¦ππ§) β β) |
12 | 11 | adantlr 713 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π₯ β β) β§ (π¦ β π β§ π§ β π)) β (π¦ππ§) β β) |
13 | | metge0 24071 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ π¦ β π β§ π§ β π) β 0 β€ (π¦ππ§)) |
14 | 13 | 3expb 1120 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π¦ β π β§ π§ β π)) β 0 β€ (π¦ππ§)) |
15 | 14 | adantlr 713 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π₯ β β) β§ (π¦ β π β§ π§ β π)) β 0 β€ (π¦ππ§)) |
16 | | elicc2 13393 |
. . . . . . . . 9
β’ ((0
β β β§ π₯
β β) β ((π¦ππ§) β (0[,]π₯) β ((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯))) |
17 | | df-3an 1089 |
. . . . . . . . 9
β’ (((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯) β (((π¦ππ§) β β β§ 0 β€ (π¦ππ§)) β§ (π¦ππ§) β€ π₯)) |
18 | 16, 17 | bitrdi 286 |
. . . . . . . 8
β’ ((0
β β β§ π₯
β β) β ((π¦ππ§) β (0[,]π₯) β (((π¦ππ§) β β β§ 0 β€ (π¦ππ§)) β§ (π¦ππ§) β€ π₯))) |
19 | 18 | baibd 540 |
. . . . . . 7
β’ (((0
β β β§ π₯
β β) β§ ((π¦ππ§) β β β§ 0 β€ (π¦ππ§))) β ((π¦ππ§) β (0[,]π₯) β (π¦ππ§) β€ π₯)) |
20 | 8, 9, 12, 15, 19 | syl22anc 837 |
. . . . . 6
β’ (((π β (Metβπ) β§ π₯ β β) β§ (π¦ β π β§ π§ β π)) β ((π¦ππ§) β (0[,]π₯) β (π¦ππ§) β€ π₯)) |
21 | 20 | 2ralbidva 3216 |
. . . . 5
β’ ((π β (Metβπ) β§ π₯ β β) β (βπ¦ β π βπ§ β π (π¦ππ§) β (0[,]π₯) β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) |
22 | 7, 21 | bitrd 278 |
. . . 4
β’ ((π β (Metβπ) β§ π₯ β β) β (π:(π Γ π)βΆ(0[,]π₯) β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) |
23 | 22 | rexbidva 3176 |
. . 3
β’ (π β (Metβπ) β (βπ₯ β β π:(π Γ π)βΆ(0[,]π₯) β βπ₯ β β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) |
24 | 23 | pm5.32i 575 |
. 2
β’ ((π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) β (π β (Metβπ) β§ βπ₯ β β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) |
25 | 1, 24 | bitri 274 |
1
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) |