Step | Hyp | Ref
| Expression |
1 | | elfvdm 6939 |
. . . 4
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | | fmval 23867 |
. . . 4
β’ ((π β dom βMet β§
π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
3 | 1, 2 | syl3an1 1160 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
4 | 3 | eleq1d 2814 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·))) |
5 | | simp1 1133 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π· β (βMetβπ)) |
6 | | simp2 1134 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π΅ β (fBasβπ)) |
7 | | simp3 1135 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β πΉ:πβΆπ) |
8 | 1 | 3ad2ant1 1130 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π β dom βMet) |
9 | | eqid 2728 |
. . . . 5
β’ ran
(π¦ β π΅ β¦ (πΉ β π¦)) = ran (π¦ β π΅ β¦ (πΉ β π¦)) |
10 | 9 | fbasrn 23808 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β dom βMet) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
11 | 6, 7, 8, 10 | syl3anc 1368 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
12 | | fgcfil 25219 |
. . 3
β’ ((π· β (βMetβπ) β§ ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
13 | 5, 11, 12 | syl2anc 582 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
14 | | imassrn 6079 |
. . . . . . . 8
β’ (πΉ β π¦) β ran πΉ |
15 | | frn 6734 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β ran πΉ β π) |
16 | 15 | 3ad2ant3 1132 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran πΉ β π) |
17 | 14, 16 | sstrid 3993 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β π) |
18 | 8, 17 | ssexd 5328 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β V) |
19 | 18 | ralrimivw 3147 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β βπ¦ β π΅ (πΉ β π¦) β V) |
20 | | eqid 2728 |
. . . . . 6
β’ (π¦ β π΅ β¦ (πΉ β π¦)) = (π¦ β π΅ β¦ (πΉ β π¦)) |
21 | | raleq 3320 |
. . . . . . 7
β’ (π = (πΉ β π¦) β (βπ£ β π (π’π·π£) < π₯ β βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
22 | 21 | raleqbi1dv 3331 |
. . . . . 6
β’ (π = (πΉ β π¦) β (βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
23 | 20, 22 | rexrnmptw 7110 |
. . . . 5
β’
(βπ¦ β
π΅ (πΉ β π¦) β V β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
24 | 19, 23 | syl 17 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
25 | | simpl3 1190 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ:πβΆπ) |
26 | 25 | ffnd 6728 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ Fn π) |
27 | | fbelss 23757 |
. . . . . . . 8
β’ ((π΅ β (fBasβπ) β§ π¦ β π΅) β π¦ β π) |
28 | 6, 27 | sylan 578 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β π¦ β π) |
29 | | oveq1 7433 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ§) β (π’π·π£) = ((πΉβπ§)π·π£)) |
30 | 29 | breq1d 5162 |
. . . . . . . . 9
β’ (π’ = (πΉβπ§) β ((π’π·π£) < π₯ β ((πΉβπ§)π·π£) < π₯)) |
31 | 30 | ralbidv 3175 |
. . . . . . . 8
β’ (π’ = (πΉβπ§) β (βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
32 | 31 | ralima 7256 |
. . . . . . 7
β’ ((πΉ Fn π β§ π¦ β π) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
33 | 26, 28, 32 | syl2anc 582 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
34 | | oveq2 7434 |
. . . . . . . . . 10
β’ (π£ = (πΉβπ€) β ((πΉβπ§)π·π£) = ((πΉβπ§)π·(πΉβπ€))) |
35 | 34 | breq1d 5162 |
. . . . . . . . 9
β’ (π£ = (πΉβπ€) β (((πΉβπ§)π·π£) < π₯ β ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
36 | 35 | ralima 7256 |
. . . . . . . 8
β’ ((πΉ Fn π β§ π¦ β π) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
37 | 26, 28, 36 | syl2anc 582 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
38 | 37 | ralbidv 3175 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
39 | 33, 38 | bitrd 278 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
40 | 39 | rexbidva 3174 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
41 | 24, 40 | bitrd 278 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
42 | 41 | ralbidv 3175 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
43 | 4, 13, 42 | 3bitrd 304 |
1
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |