Step | Hyp | Ref
| Expression |
1 | | df-hlim 29963 |
. . 3
β’
βπ£ = {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)} |
2 | 1 | relopabiv 5780 |
. 2
β’ Rel
βπ£ |
3 | | relres 5970 |
. 2
β’ Rel
((βπ‘βπ½) βΎ ( β βm
β)) |
4 | 1 | eleq2i 2826 |
. . 3
β’
(β¨π, π₯β© β
βπ£ β β¨π, π₯β© β {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)}) |
5 | | opabidw 5485 |
. . 3
β’
(β¨π, π₯β© β {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)} β ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
6 | | h2hl.3 |
. . . . . . . 8
β’ β
= (BaseSetβπ) |
7 | 6 | hlex 29889 |
. . . . . . 7
β’ β
β V |
8 | | nnex 12167 |
. . . . . . 7
β’ β
β V |
9 | 7, 8 | elmap 8815 |
. . . . . 6
β’ (π β ( β
βm β) β π:ββΆ β) |
10 | 9 | anbi1i 625 |
. . . . 5
β’ ((π β ( β
βm β) β§ β¨π, π₯β© β
(βπ‘βπ½)) β (π:ββΆ β β§ β¨π, π₯β© β
(βπ‘βπ½))) |
11 | | df-br 5110 |
. . . . . . 7
β’ (π(βπ‘βπ½)π₯ β β¨π, π₯β© β
(βπ‘βπ½)) |
12 | | h2hl.5 |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
13 | | h2hl.2 |
. . . . . . . . . 10
β’ π β NrmCVec |
14 | | h2hl.4 |
. . . . . . . . . . 11
β’ π· = (IndMetβπ) |
15 | 6, 14 | imsxmet 29683 |
. . . . . . . . . 10
β’ (π β NrmCVec β π· β (βMetβ
β)) |
16 | 13, 15 | mp1i 13 |
. . . . . . . . 9
β’ (π:ββΆ β β
π· β (βMetβ
β)) |
17 | | nnuz 12814 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
18 | | 1zzd 12542 |
. . . . . . . . 9
β’ (π:ββΆ β β
1 β β€) |
19 | | eqidd 2734 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
20 | | id 22 |
. . . . . . . . 9
β’ (π:ββΆ β β
π:ββΆ
β) |
21 | 12, 16, 17, 18, 19, 20 | lmmbrf 24649 |
. . . . . . . 8
β’ (π:ββΆ β β
(π(βπ‘βπ½)π₯ β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦))) |
22 | | eluznn 12851 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
23 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
24 | | h2hl.1 |
. . . . . . . . . . . . . . . . . 18
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
25 | 24, 13, 6, 14 | h2hmetdval 29969 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β β§ π₯ β β) β ((πβπ)π·π₯) = (normββ((πβπ) ββ π₯))) |
26 | 23, 25 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆ β β§
π β β) β§
π₯ β β) β
((πβπ)π·π₯) = (normββ((πβπ) ββ π₯))) |
27 | 26 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆ β β§
π β β) β§
π₯ β β) β
(((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
28 | 27 | an32s 651 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆ β β§
π₯ β β) β§
π β β) β
(((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
29 | 22, 28 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π:ββΆ β β§
π₯ β β) β§
(π β β β§
π β
(β€β₯βπ))) β (((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
30 | 29 | anassrs 469 |
. . . . . . . . . . . 12
β’ ((((π:ββΆ β β§
π₯ β β) β§
π β β) β§
π β
(β€β₯βπ)) β (((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
31 | 30 | ralbidva 3169 |
. . . . . . . . . . 11
β’ (((π:ββΆ β β§
π₯ β β) β§
π β β) β
(βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
32 | 31 | rexbidva 3170 |
. . . . . . . . . 10
β’ ((π:ββΆ β β§
π₯ β β) β
(βπ β β
βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
33 | 32 | ralbidv 3171 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π₯ β β) β
(βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ¦ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
34 | 33 | pm5.32da 580 |
. . . . . . . 8
β’ (π:ββΆ β β
((π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·π₯) < π¦) β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
35 | 21, 34 | bitrd 279 |
. . . . . . 7
β’ (π:ββΆ β β
(π(βπ‘βπ½)π₯ β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
36 | 11, 35 | bitr3id 285 |
. . . . . 6
β’ (π:ββΆ β β
(β¨π, π₯β© β
(βπ‘βπ½) β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
37 | 36 | pm5.32i 576 |
. . . . 5
β’ ((π:ββΆ β β§
β¨π, π₯β© β
(βπ‘βπ½)) β (π:ββΆ β β§ (π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
38 | 10, 37 | bitr2i 276 |
. . . 4
β’ ((π:ββΆ β β§
(π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) β (π β ( β βm β)
β§ β¨π, π₯β© β
(βπ‘βπ½))) |
39 | | anass 470 |
. . . 4
β’ (((π:ββΆ β β§
π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦) β (π:ββΆ β β§ (π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
40 | | opelres 5947 |
. . . . 5
β’ (π₯ β V β (β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β)) β (π β
( β βm β) β§ β¨π, π₯β© β
(βπ‘βπ½)))) |
41 | 40 | elv 3453 |
. . . 4
β’
(β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β)) β (π β
( β βm β) β§ β¨π, π₯β© β
(βπ‘βπ½))) |
42 | 38, 39, 41 | 3bitr4i 303 |
. . 3
β’ (((π:ββΆ β β§
π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦) β β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β))) |
43 | 4, 5, 42 | 3bitri 297 |
. 2
β’
(β¨π, π₯β© β
βπ£ β β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β))) |
44 | 2, 3, 43 | eqrelriiv 5750 |
1
β’
βπ£ = ((βπ‘βπ½) βΎ ( β
βm β)) |