Step | Hyp | Ref
| Expression |
1 | | iscmet3.2 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
2 | 1 | cmetcau 24669 |
. . . 4
β’ ((π· β (CMetβπ) β§ π β (Cauβπ·)) β π β dom
(βπ‘βπ½)) |
3 | 2 | a1d 25 |
. . 3
β’ ((π· β (CMetβπ) β§ π β (Cauβπ·)) β (π:πβΆπ β π β dom
(βπ‘βπ½))) |
4 | 3 | ralrimiva 3140 |
. 2
β’ (π· β (CMetβπ) β βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) |
5 | | iscmet3.4 |
. . . . 5
β’ (π β π· β (Metβπ)) |
6 | 5 | adantr 482 |
. . . 4
β’ ((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β π· β (Metβπ)) |
7 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β π β (CauFilβπ·)) |
8 | | 1rp 12924 |
. . . . . . . . . . 11
β’ 1 β
β+ |
9 | | rphalfcl 12947 |
. . . . . . . . . . 11
β’ (1 β
β+ β (1 / 2) β β+) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
β’ (1 / 2)
β β+ |
11 | | rpexpcl 13992 |
. . . . . . . . . 10
β’ (((1 / 2)
β β+ β§ π β β€) β ((1 / 2)βπ) β
β+) |
12 | 10, 11 | mpan 689 |
. . . . . . . . 9
β’ (π β β€ β ((1 /
2)βπ) β
β+) |
13 | | cfili 24648 |
. . . . . . . . 9
β’ ((π β (CauFilβπ·) β§ ((1 / 2)βπ) β β+)
β βπ‘ β
π βπ’ β π‘ βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ)) |
14 | 7, 12, 13 | syl2an 597 |
. . . . . . . 8
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β§ π β β€) β βπ‘ β π βπ’ β π‘ βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ)) |
15 | 14 | ralrimiva 3140 |
. . . . . . 7
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β βπ β β€ βπ‘ β π βπ’ β π‘ βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ)) |
16 | | vex 3448 |
. . . . . . . 8
β’ π β V |
17 | | znnen 16099 |
. . . . . . . . 9
β’ β€
β β |
18 | | nnenom 13891 |
. . . . . . . . 9
β’ β
β Ο |
19 | 17, 18 | entri 8951 |
. . . . . . . 8
β’ β€
β Ο |
20 | | raleq 3308 |
. . . . . . . . 9
β’ (π‘ = (π βπ) β (βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ) β βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
21 | 20 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π‘ = (π βπ) β (βπ’ β π‘ βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ) β βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
22 | 16, 19, 21 | axcc4 10380 |
. . . . . . 7
β’
(βπ β
β€ βπ‘ β
π βπ’ β π‘ βπ£ β π‘ (π’π·π£) < ((1 / 2)βπ) β βπ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
23 | 15, 22 | syl 17 |
. . . . . 6
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β βπ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
24 | | iscmet3.3 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β π β β€) |
26 | | iscmet3.1 |
. . . . . . . . . . . 12
β’ π =
(β€β₯βπ) |
27 | 26 | uzenom 13875 |
. . . . . . . . . . 11
β’ (π β β€ β π β
Ο) |
28 | | endom 8922 |
. . . . . . . . . . 11
β’ (π β Ο β π βΌ
Ο) |
29 | 25, 27, 28 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β π βΌ Ο) |
30 | | dfin5 3919 |
. . . . . . . . . . . . . . 15
β’ (( I
βπ) β© β© π β (π...π)(π βπ)) = {π₯ β ( I βπ) β£ π₯ β β©
π β (π...π)(π βπ)} |
31 | | fzn0 13461 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π...π) β β
β π β (β€β₯βπ)) |
32 | 31 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯βπ) β (π...π) β β
) |
33 | 32, 26 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (π...π) β β
) |
34 | | metxmet 23703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
35 | 5, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π· β (βMetβπ)) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β π· β (βMetβπ)) |
37 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (CauFilβπ·) β§ π :β€βΆπ) β π β (CauFilβπ·)) |
38 | | cfilfil 24647 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π· β (βMetβπ) β§ π β (CauFilβπ·)) β π β (Filβπ)) |
39 | 36, 37, 38 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β π β (Filβπ)) |
40 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β π :β€βΆπ) |
41 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π...π) β π β β€) |
42 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π :β€βΆπ β§ π β β€) β (π βπ) β π) |
43 | 40, 41, 42 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β (π...π)) β (π βπ) β π) |
44 | | filelss 23219 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (Filβπ) β§ (π βπ) β π) β (π βπ) β π) |
45 | 39, 43, 44 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β (π...π)) β (π βπ) β π) |
46 | 45 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β βπ β (π...π)(π βπ) β π) |
47 | | r19.2z 4453 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π...π) β β
β§ βπ β (π...π)(π βπ) β π) β βπ β (π...π)(π βπ) β π) |
48 | 33, 46, 47 | syl2anr 598 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β βπ β (π...π)(π βπ) β π) |
49 | | iinss 5017 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(π...π)(π βπ) β π β β©
π β (π...π)(π βπ) β π) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β β©
π β (π...π)(π βπ) β π) |
51 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β π· β (Metβπ)) |
52 | | elfvdm 6880 |
. . . . . . . . . . . . . . . . . 18
β’ (π· β (Metβπ) β π β dom Met) |
53 | | fvi 6918 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom Met β ( I
βπ) = π) |
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β ( I βπ) = π) |
55 | 50, 54 | sseqtrrd 3986 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β β©
π β (π...π)(π βπ) β ( I βπ)) |
56 | | sseqin2 4176 |
. . . . . . . . . . . . . . . 16
β’ (β© π β (π...π)(π βπ) β ( I βπ) β (( I βπ) β© β©
π β (π...π)(π βπ)) = β©
π β (π...π)(π βπ)) |
57 | 55, 56 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β (( I βπ) β© β©
π β (π...π)(π βπ)) = β©
π β (π...π)(π βπ)) |
58 | 30, 57 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β {π₯ β ( I βπ) β£ π₯ β β©
π β (π...π)(π βπ)} = β©
π β (π...π)(π βπ)) |
59 | 39 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β π β (Filβπ)) |
60 | 43 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β βπ β (π...π)(π βπ) β π) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β βπ β (π...π)(π βπ) β π) |
62 | 33 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β (π...π) β β
) |
63 | | fzfid 13884 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β (π...π) β Fin) |
64 | | iinfi 9358 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (Filβπ) β§ (βπ β (π...π)(π βπ) β π β§ (π...π) β β
β§ (π...π) β Fin)) β β© π β (π...π)(π βπ) β (fiβπ)) |
65 | 59, 61, 62, 63, 64 | syl13anc 1373 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β β©
π β (π...π)(π βπ) β (fiβπ)) |
66 | | filfi 23226 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Filβπ) β (fiβπ) = π) |
67 | 59, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β (fiβπ) = π) |
68 | 65, 67 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β β©
π β (π...π)(π βπ) β π) |
69 | | fileln0 23217 |
. . . . . . . . . . . . . . 15
β’ ((π β (Filβπ) β§ β© π β (π...π)(π βπ) β π) β β©
π β (π...π)(π βπ) β β
) |
70 | 39, 68, 69 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β β©
π β (π...π)(π βπ) β β
) |
71 | 58, 70 | eqnetrd 3008 |
. . . . . . . . . . . . 13
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β {π₯ β ( I βπ) β£ π₯ β β©
π β (π...π)(π βπ)} β β
) |
72 | | rabn0 4346 |
. . . . . . . . . . . . 13
β’ ({π₯ β ( I βπ) β£ π₯ β β©
π β (π...π)(π βπ)} β β
β βπ₯ β ( I βπ)π₯ β β©
π β (π...π)(π βπ)) |
73 | 71, 72 | sylib 217 |
. . . . . . . . . . . 12
β’ ((((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β§ π β π) β βπ₯ β ( I βπ)π₯ β β©
π β (π...π)(π βπ)) |
74 | 73 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ π :β€βΆπ)) β βπ β π βπ₯ β ( I βπ)π₯ β β©
π β (π...π)(π βπ)) |
75 | 74 | adantrrr 724 |
. . . . . . . . . 10
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β βπ β π βπ₯ β ( I βπ)π₯ β β©
π β (π...π)(π βπ)) |
76 | | fvex 6856 |
. . . . . . . . . . 11
β’ ( I
βπ) β
V |
77 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ) β (π₯ β β©
π β (π...π)(π βπ) β (πβπ) β β©
π β (π...π)(π βπ))) |
78 | | fvex 6856 |
. . . . . . . . . . . . 13
β’ (πβπ) β V |
79 | | eliin 4960 |
. . . . . . . . . . . . 13
β’ ((πβπ) β V β ((πβπ) β β©
π β (π...π)(π βπ) β βπ β (π...π)(πβπ) β (π βπ))) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((πβπ) β β©
π β (π...π)(π βπ) β βπ β (π...π)(πβπ) β (π βπ)) |
81 | 77, 80 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π₯ = (πβπ) β (π₯ β β©
π β (π...π)(π βπ) β βπ β (π...π)(πβπ) β (π βπ))) |
82 | 76, 81 | axcc4dom 10382 |
. . . . . . . . . 10
β’ ((π βΌ Ο β§
βπ β π βπ₯ β ( I βπ)π₯ β β©
π β (π...π)(π βπ)) β βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) |
83 | 29, 75, 82 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) |
84 | | df-ral 3062 |
. . . . . . . . . . . . 13
β’
(βπ β
(Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½)) β βπ(π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½)))) |
85 | | 19.29 1877 |
. . . . . . . . . . . . 13
β’
((βπ(π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) β βπ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) |
86 | 84, 85 | sylanb 582 |
. . . . . . . . . . . 12
β’
((βπ β
(Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½)) β§ βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) β βπ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) |
87 | 24 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π β β€) |
88 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π· β (Metβπ)) |
89 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π:πβΆ( I βπ)) |
90 | | feq3 6652 |
. . . . . . . . . . . . . . . . 17
β’ (( I
βπ) = π β (π:πβΆ( I βπ) β π:πβΆπ)) |
91 | 88, 52, 53, 90 | 4syl 19 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β (π:πβΆ( I βπ) β π:πβΆπ)) |
92 | 89, 91 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π:πβΆπ) |
93 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
94 | 93 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)) |
95 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π βπ) = (π βπ)) |
96 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((1 / 2)βπ) = ((1 / 2)βπ)) |
97 | 96 | breq2d 5118 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π’π·π£) < ((1 / 2)βπ) β (π’π·π£) < ((1 / 2)βπ))) |
98 | 95, 97 | raleqbidv 3318 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ) β βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
99 | 95, 98 | raleqbidv 3318 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ) β βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ))) |
100 | 99 | cbvralvw 3224 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β€ βπ’ β
(π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ) β βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)) |
101 | 94, 100 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)) |
102 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β βπ β π βπ β (π...π)(πβπ) β (π βπ)) |
103 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π βπ) = (π βπ)) |
104 | 103 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πβπ) β (π βπ) β (πβπ) β (π βπ))) |
105 | 104 | cbvralvw 3224 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(π...π)(πβπ) β (π βπ) β βπ β (π...π)(πβπ) β (π βπ)) |
106 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π...π) = (π...π)) |
107 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πβπ) = (πβπ)) |
108 | 107 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πβπ) β (π βπ) β (πβπ) β (π βπ))) |
109 | 106, 108 | raleqbidv 3318 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (βπ β (π...π)(πβπ) β (π βπ) β βπ β (π...π)(πβπ) β (π βπ))) |
110 | 105, 109 | bitrid 283 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (βπ β (π...π)(πβπ) β (π βπ) β βπ β (π...π)(πβπ) β (π βπ))) |
111 | 110 | cbvralvw 3224 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
π βπ β (π...π)(πβπ) β (π βπ) β βπ β π βπ β (π...π)(πβπ) β (π βπ)) |
112 | 102, 111 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β βπ β π βπ β (π...π)(πβπ) β (π βπ)) |
113 | 88, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π· β (βMetβπ)) |
114 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π β (CauFilβπ·)) |
115 | 113, 114,
38 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π β (Filβπ)) |
116 | 93 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π :β€βΆπ) |
117 | 26, 1, 87, 88, 92, 101, 112 | iscmet3lem1 24671 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π β (Cauβπ·)) |
118 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β (π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½)))) |
119 | 117, 92, 118 | mp2d 49 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β π β dom
(βπ‘βπ½)) |
120 | 26, 1, 87, 88, 92, 101, 112, 115, 116, 119 | iscmet3lem2 24672 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)))) β (π½ fLim π) β β
) |
121 | 120 | ex 414 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β (((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) β (π½ fLim π) β β
)) |
122 | 121 | exlimdv 1937 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β (βπ((π β (Cauβπ·) β (π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) β (π½ fLim π) β β
)) |
123 | 86, 122 | syl5 34 |
. . . . . . . . . . 11
β’ ((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β ((βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½)) β§ βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ))) β (π½ fLim π) β β
)) |
124 | 123 | expdimp 454 |
. . . . . . . . . 10
β’ (((π β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β (βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)) β (π½ fLim π) β β
)) |
125 | 124 | an32s 651 |
. . . . . . . . 9
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β (βπ(π:πβΆ( I βπ) β§ βπ β π βπ β (π...π)(πβπ) β (π βπ)) β (π½ fLim π) β β
)) |
126 | 83, 125 | mpd 15 |
. . . . . . . 8
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ (π β (CauFilβπ·) β§ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)))) β (π½ fLim π) β β
) |
127 | 126 | expr 458 |
. . . . . . 7
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β ((π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)) β (π½ fLim π) β β
)) |
128 | 127 | exlimdv 1937 |
. . . . . 6
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β (βπ (π :β€βΆπ β§ βπ β β€ βπ’ β (π βπ)βπ£ β (π βπ)(π’π·π£) < ((1 / 2)βπ)) β (π½ fLim π) β β
)) |
129 | 23, 128 | mpd 15 |
. . . . 5
β’ (((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β§ π β (CauFilβπ·)) β (π½ fLim π) β β
) |
130 | 129 | ralrimiva 3140 |
. . . 4
β’ ((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β βπ β (CauFilβπ·)(π½ fLim π) β β
) |
131 | 1 | iscmet 24664 |
. . . 4
β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β
)) |
132 | 6, 130, 131 | sylanbrc 584 |
. . 3
β’ ((π β§ βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½))) β π· β (CMetβπ)) |
133 | 132 | ex 414 |
. 2
β’ (π β (βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½)) β π· β (CMetβπ))) |
134 | 4, 133 | impbid2 225 |
1
β’ (π β (π· β (CMetβπ) β βπ β (Cauβπ·)(π:πβΆπ β π β dom
(βπ‘βπ½)))) |