Step | Hyp | Ref
| Expression |
1 | | elfvdm 6925 |
. . . 4
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | | fmval 23438 |
. . . 4
β’ ((π β dom βMet β§
π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
3 | 1, 2 | syl3an1 1163 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
4 | 3 | eleq1d 2818 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·))) |
5 | | simp1 1136 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π· β (βMetβπ)) |
6 | | simp2 1137 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π΅ β (fBasβπ)) |
7 | | simp3 1138 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β πΉ:πβΆπ) |
8 | 1 | 3ad2ant1 1133 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β π β dom βMet) |
9 | | eqid 2732 |
. . . . 5
β’ ran
(π¦ β π΅ β¦ (πΉ β π¦)) = ran (π¦ β π΅ β¦ (πΉ β π¦)) |
10 | 9 | fbasrn 23379 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β dom βMet) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
11 | 6, 7, 8, 10 | syl3anc 1371 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
12 | | fgcfil 24779 |
. . 3
β’ ((π· β (βMetβπ) β§ ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
13 | 5, 11, 12 | syl2anc 584 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
14 | | imassrn 6068 |
. . . . . . . 8
β’ (πΉ β π¦) β ran πΉ |
15 | | frn 6721 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β ran πΉ β π) |
16 | 15 | 3ad2ant3 1135 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran πΉ β π) |
17 | 14, 16 | sstrid 3992 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β π) |
18 | 8, 17 | ssexd 5323 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β V) |
19 | 18 | ralrimivw 3150 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β βπ¦ β π΅ (πΉ β π¦) β V) |
20 | | eqid 2732 |
. . . . . 6
β’ (π¦ β π΅ β¦ (πΉ β π¦)) = (π¦ β π΅ β¦ (πΉ β π¦)) |
21 | | raleq 3322 |
. . . . . . 7
β’ (π = (πΉ β π¦) β (βπ£ β π (π’π·π£) < π₯ β βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
22 | 21 | raleqbi1dv 3333 |
. . . . . 6
β’ (π = (πΉ β π¦) β (βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
23 | 20, 22 | rexrnmptw 7093 |
. . . . 5
β’
(βπ¦ β
π΅ (πΉ β π¦) β V β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
24 | 19, 23 | syl 17 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
25 | | simpl3 1193 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ:πβΆπ) |
26 | 25 | ffnd 6715 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ Fn π) |
27 | | fbelss 23328 |
. . . . . . . 8
β’ ((π΅ β (fBasβπ) β§ π¦ β π΅) β π¦ β π) |
28 | 6, 27 | sylan 580 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β π¦ β π) |
29 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ§) β (π’π·π£) = ((πΉβπ§)π·π£)) |
30 | 29 | breq1d 5157 |
. . . . . . . . 9
β’ (π’ = (πΉβπ§) β ((π’π·π£) < π₯ β ((πΉβπ§)π·π£) < π₯)) |
31 | 30 | ralbidv 3177 |
. . . . . . . 8
β’ (π’ = (πΉβπ§) β (βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
32 | 31 | ralima 7236 |
. . . . . . 7
β’ ((πΉ Fn π β§ π¦ β π) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
33 | 26, 28, 32 | syl2anc 584 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
34 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π£ = (πΉβπ€) β ((πΉβπ§)π·π£) = ((πΉβπ§)π·(πΉβπ€))) |
35 | 34 | breq1d 5157 |
. . . . . . . . 9
β’ (π£ = (πΉβπ€) β (((πΉβπ§)π·π£) < π₯ β ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
36 | 35 | ralima 7236 |
. . . . . . . 8
β’ ((πΉ Fn π β§ π¦ β π) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
37 | 26, 28, 36 | syl2anc 584 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
38 | 37 | ralbidv 3177 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
39 | 33, 38 | bitrd 278 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
40 | 39 | rexbidva 3176 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
41 | 24, 40 | bitrd 278 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
42 | 41 | ralbidv 3177 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
43 | 4, 13, 42 | 3bitrd 304 |
1
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |