Step | Hyp | Ref
| Expression |
1 | | df-hlim 30220 |
. . 3
β’
βπ£ = {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)} |
2 | 1 | relopabiv 5820 |
. 2
β’ Rel
βπ£ |
3 | | relres 6010 |
. 2
β’ Rel
((βπ‘βπ½) βΎ ( β βm
β)) |
4 | 1 | eleq2i 2825 |
. . 3
β’
(β¨π, π₯β© β
βπ£ β β¨π, π₯β© β {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)}) |
5 | | opabidw 5524 |
. . 3
β’
(β¨π, π₯β© β {β¨π, π₯β© β£ ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)} β ((π:ββΆ β β§ π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
6 | | h2hl.3 |
. . . . . . . 8
β’ β
= (BaseSetβπ) |
7 | 6 | hlex 30146 |
. . . . . . 7
β’ β
β V |
8 | | nnex 12217 |
. . . . . . 7
β’ β
β V |
9 | 7, 8 | elmap 8864 |
. . . . . 6
β’ (π β ( β
βm β) β π:ββΆ β) |
10 | 9 | anbi1i 624 |
. . . . 5
β’ ((π β ( β
βm β) β§ β¨π, π₯β© β
(βπ‘βπ½)) β (π:ββΆ β β§ β¨π, π₯β© β
(βπ‘βπ½))) |
11 | | df-br 5149 |
. . . . . . 7
β’ (π(βπ‘βπ½)π₯ β β¨π, π₯β© β
(βπ‘βπ½)) |
12 | | h2hl.5 |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
13 | | h2hl.2 |
. . . . . . . . . 10
β’ π β NrmCVec |
14 | | h2hl.4 |
. . . . . . . . . . 11
β’ π· = (IndMetβπ) |
15 | 6, 14 | imsxmet 29940 |
. . . . . . . . . 10
β’ (π β NrmCVec β π· β (βMetβ
β)) |
16 | 13, 15 | mp1i 13 |
. . . . . . . . 9
β’ (π:ββΆ β β
π· β (βMetβ
β)) |
17 | | nnuz 12864 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
18 | | 1zzd 12592 |
. . . . . . . . 9
β’ (π:ββΆ β β
1 β β€) |
19 | | eqidd 2733 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
20 | | id 22 |
. . . . . . . . 9
β’ (π:ββΆ β β
π:ββΆ
β) |
21 | 12, 16, 17, 18, 19, 20 | lmmbrf 24778 |
. . . . . . . 8
β’ (π:ββΆ β β
(π(βπ‘βπ½)π₯ β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦))) |
22 | | eluznn 12901 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
23 | | ffvelcdm 7083 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
24 | | h2hl.1 |
. . . . . . . . . . . . . . . . . 18
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
25 | 24, 13, 6, 14 | h2hmetdval 30226 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β β§ π₯ β β) β ((πβπ)π·π₯) = (normββ((πβπ) ββ π₯))) |
26 | 23, 25 | sylan 580 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆ β β§
π β β) β§
π₯ β β) β
((πβπ)π·π₯) = (normββ((πβπ) ββ π₯))) |
27 | 26 | breq1d 5158 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆ β β§
π β β) β§
π₯ β β) β
(((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
28 | 27 | an32s 650 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆ β β§
π₯ β β) β§
π β β) β
(((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
29 | 22, 28 | sylan2 593 |
. . . . . . . . . . . . 13
β’ (((π:ββΆ β β§
π₯ β β) β§
(π β β β§
π β
(β€β₯βπ))) β (((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
30 | 29 | anassrs 468 |
. . . . . . . . . . . 12
β’ ((((π:ββΆ β β§
π₯ β β) β§
π β β) β§
π β
(β€β₯βπ)) β (((πβπ)π·π₯) < π¦ β
(normββ((πβπ) ββ π₯)) < π¦)) |
31 | 30 | ralbidva 3175 |
. . . . . . . . . . 11
β’ (((π:ββΆ β β§
π₯ β β) β§
π β β) β
(βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
32 | 31 | rexbidva 3176 |
. . . . . . . . . 10
β’ ((π:ββΆ β β§
π₯ β β) β
(βπ β β
βπ β
(β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
33 | 32 | ralbidv 3177 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π₯ β β) β
(βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·π₯) < π¦ β βπ¦ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) |
34 | 33 | pm5.32da 579 |
. . . . . . . 8
β’ (π:ββΆ β β
((π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·π₯) < π¦) β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
35 | 21, 34 | bitrd 278 |
. . . . . . 7
β’ (π:ββΆ β β
(π(βπ‘βπ½)π₯ β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
36 | 11, 35 | bitr3id 284 |
. . . . . 6
β’ (π:ββΆ β β
(β¨π, π₯β© β
(βπ‘βπ½) β (π₯ β β β§ βπ¦ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
37 | 36 | pm5.32i 575 |
. . . . 5
β’ ((π:ββΆ β β§
β¨π, π₯β© β
(βπ‘βπ½)) β (π:ββΆ β β§ (π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
38 | 10, 37 | bitr2i 275 |
. . . 4
β’ ((π:ββΆ β β§
(π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦)) β (π β ( β βm β)
β§ β¨π, π₯β© β
(βπ‘βπ½))) |
39 | | anass 469 |
. . . 4
β’ (((π:ββΆ β β§
π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦) β (π:ββΆ β β§ (π₯ β β β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦))) |
40 | | opelres 5987 |
. . . . 5
β’ (π₯ β V β (β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β)) β (π β
( β βm β) β§ β¨π, π₯β© β
(βπ‘βπ½)))) |
41 | 40 | elv 3480 |
. . . 4
β’
(β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β)) β (π β
( β βm β) β§ β¨π, π₯β© β
(βπ‘βπ½))) |
42 | 38, 39, 41 | 3bitr4i 302 |
. . 3
β’ (((π:ββΆ β β§
π₯ β β) β§
βπ¦ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ π₯)) < π¦) β β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β))) |
43 | 4, 5, 42 | 3bitri 296 |
. 2
β’
(β¨π, π₯β© β
βπ£ β β¨π, π₯β© β
((βπ‘βπ½) βΎ ( β βm
β))) |
44 | 2, 3, 43 | eqrelriiv 5790 |
1
β’
βπ£ = ((βπ‘βπ½) βΎ ( β
βm β)) |