Step | Hyp | Ref
| Expression |
1 | | elfvdm 6921 |
. . . 4
β’ (π· β (βMetβπ) β π β dom βMet) |
2 | | fmval 23798 |
. . . 4
β’ ((π β dom βMet β§
π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
3 | 1, 2 | syl3an1 1160 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) |
4 | 3 | eleq1d 2812 |
. 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 2726 |
. . . . 5
β’ ran
(π¦ β π΅ β¦ (πΉ β π¦)) = ran (π¦ β π΅ β¦ (πΉ β π¦)) |
10 | 9 | fbasrn 23739 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β dom βMet) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
11 | 6, 7, 8, 10 | syl3anc 1368 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) |
12 | | fgcfil 25150 |
. . 3
β’ ((π· β (βMetβπ) β§ ran (π¦ β π΅ β¦ (πΉ β π¦)) β (fBasβπ)) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
13 | 5, 11, 12 | syl2anc 583 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((πfilGenran (π¦ β π΅ β¦ (πΉ β π¦))) β (CauFilβπ·) β βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯)) |
14 | | imassrn 6063 |
. . . . . . . 8
β’ (πΉ β π¦) β ran πΉ |
15 | | frn 6717 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β ran πΉ β π) |
16 | 15 | 3ad2ant3 1132 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ran πΉ β π) |
17 | 14, 16 | sstrid 3988 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β π) |
18 | 8, 17 | ssexd 5317 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (πΉ β π¦) β V) |
19 | 18 | ralrimivw 3144 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β βπ¦ β π΅ (πΉ β π¦) β V) |
20 | | eqid 2726 |
. . . . . 6
β’ (π¦ β π΅ β¦ (πΉ β π¦)) = (π¦ β π΅ β¦ (πΉ β π¦)) |
21 | | raleq 3316 |
. . . . . . 7
β’ (π = (πΉ β π¦) β (βπ£ β π (π’π·π£) < π₯ β βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
22 | 21 | raleqbi1dv 3327 |
. . . . . 6
β’ (π = (πΉ β π¦) β (βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
23 | 20, 22 | rexrnmptw 7089 |
. . . . 5
β’
(βπ¦ β
π΅ (πΉ β π¦) β V β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
24 | 19, 23 | syl 17 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯)) |
25 | | simpl3 1190 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ:πβΆπ) |
26 | 25 | ffnd 6711 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β πΉ Fn π) |
27 | | fbelss 23688 |
. . . . . . . 8
β’ ((π΅ β (fBasβπ) β§ π¦ β π΅) β π¦ β π) |
28 | 6, 27 | sylan 579 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β π¦ β π) |
29 | | oveq1 7411 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ§) β (π’π·π£) = ((πΉβπ§)π·π£)) |
30 | 29 | breq1d 5151 |
. . . . . . . . 9
β’ (π’ = (πΉβπ§) β ((π’π·π£) < π₯ β ((πΉβπ§)π·π£) < π₯)) |
31 | 30 | ralbidv 3171 |
. . . . . . . 8
β’ (π’ = (πΉβπ§) β (βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
32 | 31 | ralima 7234 |
. . . . . . 7
β’ ((πΉ Fn π β§ π¦ β π) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
33 | 26, 28, 32 | syl2anc 583 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯)) |
34 | | oveq2 7412 |
. . . . . . . . . 10
β’ (π£ = (πΉβπ€) β ((πΉβπ§)π·π£) = ((πΉβπ§)π·(πΉβπ€))) |
35 | 34 | breq1d 5151 |
. . . . . . . . 9
β’ (π£ = (πΉβπ€) β (((πΉβπ§)π·π£) < π₯ β ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
36 | 35 | ralima 7234 |
. . . . . . . 8
β’ ((πΉ Fn π β§ π¦ β π) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
37 | 26, 28, 36 | syl2anc 583 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
38 | 37 | ralbidv 3171 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ§ β π¦ βπ£ β (πΉ β π¦)((πΉβπ§)π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
39 | 33, 38 | bitrd 279 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π¦ β π΅) β (βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
40 | 39 | rexbidva 3170 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ¦ β π΅ βπ’ β (πΉ β π¦)βπ£ β (πΉ β π¦)(π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
41 | 24, 40 | bitrd 279 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
42 | 41 | ralbidv 3171 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (βπ₯ β β+ βπ β ran (π¦ β π΅ β¦ (πΉ β π¦))βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |
43 | 4, 13, 42 | 3bitrd 305 |
1
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) |