Step | Hyp | Ref
| Expression |
1 | | iscfil 24652 |
. 2
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) |
2 | | xmetf 23705 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
3 | 2 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β π·:(π Γ π)βΆβ*) |
4 | 3 | ffund 6676 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β Fun π·) |
5 | | filelss 23226 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π¦ β πΉ) β π¦ β π) |
6 | 5 | ad4ant24 753 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β π¦ β π) |
7 | | xpss12 5652 |
. . . . . . . . 9
β’ ((π¦ β π β§ π¦ β π) β (π¦ Γ π¦) β (π Γ π)) |
8 | 6, 6, 7 | syl2anc 585 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β (π¦ Γ π¦) β (π Γ π)) |
9 | 3 | fdmd 6683 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β dom π· = (π Γ π)) |
10 | 8, 9 | sseqtrrd 3989 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β (π¦ Γ π¦) β dom π·) |
11 | | funimassov 7535 |
. . . . . . 7
β’ ((Fun
π· β§ (π¦ Γ π¦) β dom π·) β ((π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ§ β π¦ βπ€ β π¦ (π§π·π€) β (0[,)π₯))) |
12 | 4, 10, 11 | syl2anc 585 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β ((π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ§ β π¦ βπ€ β π¦ (π§π·π€) β (0[,)π₯))) |
13 | | 0xr 11210 |
. . . . . . . . 9
β’ 0 β
β* |
14 | 13 | a1i 11 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β 0 β
β*) |
15 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β π₯ β β+) |
16 | 15 | rpxrd 12966 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β π₯ β β*) |
17 | | simp-4l 782 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β π· β (βMetβπ)) |
18 | 6 | sselda 3948 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ π§ β π¦) β π§ β π) |
19 | 18 | adantrr 716 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β π§ β π) |
20 | 6 | sselda 3948 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ π€ β π¦) β π€ β π) |
21 | 20 | adantrl 715 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β π€ β π) |
22 | | xmetcl 23707 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π§ β π β§ π€ β π) β (π§π·π€) β
β*) |
23 | 17, 19, 21, 22 | syl3anc 1372 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β (π§π·π€) β
β*) |
24 | | xmetge0 23720 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π§ β π β§ π€ β π) β 0 β€ (π§π·π€)) |
25 | 17, 19, 21, 24 | syl3anc 1372 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β 0 β€ (π§π·π€)) |
26 | | elico1 13316 |
. . . . . . . . . 10
β’ ((0
β β* β§ π₯ β β*) β ((π§π·π€) β (0[,)π₯) β ((π§π·π€) β β* β§ 0 β€
(π§π·π€) β§ (π§π·π€) < π₯))) |
27 | | df-3an 1090 |
. . . . . . . . . 10
β’ (((π§π·π€) β β* β§ 0 β€
(π§π·π€) β§ (π§π·π€) < π₯) β (((π§π·π€) β β* β§ 0 β€
(π§π·π€)) β§ (π§π·π€) < π₯)) |
28 | 26, 27 | bitrdi 287 |
. . . . . . . . 9
β’ ((0
β β* β§ π₯ β β*) β ((π§π·π€) β (0[,)π₯) β (((π§π·π€) β β* β§ 0 β€
(π§π·π€)) β§ (π§π·π€) < π₯))) |
29 | 28 | baibd 541 |
. . . . . . . 8
β’ (((0
β β* β§ π₯ β β*) β§ ((π§π·π€) β β* β§ 0 β€
(π§π·π€))) β ((π§π·π€) β (0[,)π₯) β (π§π·π€) < π₯)) |
30 | 14, 16, 23, 25, 29 | syl22anc 838 |
. . . . . . 7
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β§ (π§ β π¦ β§ π€ β π¦)) β ((π§π·π€) β (0[,)π₯) β (π§π·π€) < π₯)) |
31 | 30 | 2ralbidva 3207 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β (βπ§ β π¦ βπ€ β π¦ (π§π·π€) β (0[,)π₯) β βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
32 | 12, 31 | bitrd 279 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β§ π¦ β πΉ) β ((π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
33 | 32 | rexbidva 3170 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π₯ β β+) β
(βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
34 | 33 | ralbidva 3169 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ)) β (βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
35 | 34 | pm5.32da 580 |
. 2
β’ (π· β (βMetβπ) β ((πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |
36 | 1, 35 | bitrd 279 |
1
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |