Step | Hyp | Ref
| Expression |
1 | | lmmbr.3 |
. . . 4
β’ (π β π· β (βMetβπ)) |
2 | | lmmbr.2 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
3 | 2 | mopntopon 23815 |
. . . 4
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
4 | 1, 3 | syl 17 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
5 | 4 | lmbr 22632 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) |
6 | | rpxr 12932 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β*) |
7 | 2 | blopn 23879 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β*) β (π(ballβπ·)π₯) β π½) |
8 | 6, 7 | syl3an3 1166 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β (π(ballβπ·)π₯) β π½) |
9 | | blcntr 23789 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β π β (π(ballβπ·)π₯)) |
10 | | eleq2 2823 |
. . . . . . . . . . . . . 14
β’ (π’ = (π(ballβπ·)π₯) β (π β π’ β π β (π(ballβπ·)π₯))) |
11 | | feq3 6655 |
. . . . . . . . . . . . . . 15
β’ (π’ = (π(ballβπ·)π₯) β ((πΉ βΎ π¦):π¦βΆπ’ β (πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
12 | 11 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π’ = (π(ballβπ·)π₯) β (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
13 | 10, 12 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π’ = (π(ballβπ·)π₯) β ((π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β (π β (π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
14 | 13 | rspcva 3581 |
. . . . . . . . . . . 12
β’ (((π(ballβπ·)π₯) β π½ β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (π β (π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
15 | 14 | impancom 453 |
. . . . . . . . . . 11
β’ (((π(ballβπ·)π₯) β π½ β§ π β (π(ballβπ·)π₯)) β (βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
16 | 8, 9, 15 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
17 | 16 | 3expa 1119 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
18 | 17 | adantlrl 719 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
19 | 18 | impancom 453 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (π₯ β β+ β
βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
20 | 19 | ralrimiv 3139 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) |
21 | 2 | mopni2 23872 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π’ β π½ β§ π β π’) β βπ₯ β β+ (π(ballβπ·)π₯) β π’) |
22 | | r19.29 3114 |
. . . . . . . . . . . 12
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ βπ₯ β β+ (π(ballβπ·)π₯) β π’) β βπ₯ β β+ (βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’)) |
23 | | fss 6689 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β (πΉ βΎ π¦):π¦βΆπ’) |
24 | 23 | expcom 415 |
. . . . . . . . . . . . . . 15
β’ ((π(ballβπ·)π₯) β π’ β ((πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β (πΉ βΎ π¦):π¦βΆπ’)) |
25 | 24 | reximdv 3164 |
. . . . . . . . . . . . . 14
β’ ((π(ballβπ·)π₯) β π’ β (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) |
26 | 25 | impcom 409 |
. . . . . . . . . . . . 13
β’
((βπ¦ β
ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
27 | 26 | rexlimivw 3145 |
. . . . . . . . . . . 12
β’
(βπ₯ β
β+ (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ βπ₯ β β+ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
29 | 21, 28 | sylan2 594 |
. . . . . . . . . 10
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π· β (βMetβπ) β§ π’ β π½ β§ π β π’)) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
30 | 29 | 3exp2 1355 |
. . . . . . . . 9
β’
(βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β (π· β (βMetβπ) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) |
31 | 30 | impcom 409 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ βπ₯ β β+
βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
32 | 31 | adantlr 714 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
33 | 32 | ralrimiv 3139 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) |
34 | 20, 33 | impbida 800 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β (βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
35 | 34 | pm5.32da 580 |
. . . 4
β’ (π· β (βMetβπ) β (((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
36 | | df-3an 1090 |
. . . 4
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
37 | | df-3an 1090 |
. . . 4
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
38 | 35, 36, 37 | 3bitr4g 314 |
. . 3
β’ (π· β (βMetβπ) β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
39 | 1, 38 | syl 17 |
. 2
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
40 | 5, 39 | bitrd 279 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |