Step | Hyp | Ref
| Expression |
1 | | lmmbr.3 |
. . . 4
β’ (π β π· β (βMetβπ)) |
2 | | lmmbr.2 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
3 | 2 | mopntopon 23944 |
. . . 4
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
4 | 1, 3 | syl 17 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
5 | 4 | lmbr 22761 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) |
6 | | rpxr 12982 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β*) |
7 | 2 | blopn 24008 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β*) β (π(ballβπ·)π₯) β π½) |
8 | 6, 7 | syl3an3 1165 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β (π(ballβπ·)π₯) β π½) |
9 | | blcntr 23918 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β π β (π(ballβπ·)π₯)) |
10 | | eleq2 2822 |
. . . . . . . . . . . . . 14
β’ (π’ = (π(ballβπ·)π₯) β (π β π’ β π β (π(ballβπ·)π₯))) |
11 | | feq3 6700 |
. . . . . . . . . . . . . . 15
β’ (π’ = (π(ballβπ·)π₯) β ((πΉ βΎ π¦):π¦βΆπ’ β (πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
12 | 11 | rexbidv 3178 |
. . . . . . . . . . . . . 14
β’ (π’ = (π(ballβπ·)π₯) β (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
13 | 10, 12 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ (π’ = (π(ballβπ·)π₯) β ((π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β (π β (π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
14 | 13 | rspcva 3610 |
. . . . . . . . . . . 12
β’ (((π(ballβπ·)π₯) β π½ β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (π β (π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
15 | 14 | impancom 452 |
. . . . . . . . . . 11
β’ (((π(ballβπ·)π₯) β π½ β§ π β (π(ballβπ·)π₯)) β (βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
16 | 8, 9, 15 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
17 | 16 | 3expa 1118 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
18 | 17 | adantlrl 718 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ π₯ β β+) β
(βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
19 | 18 | impancom 452 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (π₯ β β+ β
βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
20 | 19 | ralrimiv 3145 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) |
21 | 2 | mopni2 24001 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π’ β π½ β§ π β π’) β βπ₯ β β+ (π(ballβπ·)π₯) β π’) |
22 | | r19.29 3114 |
. . . . . . . . . . . 12
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ βπ₯ β β+ (π(ballβπ·)π₯) β π’) β βπ₯ β β+ (βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’)) |
23 | | fss 6734 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β (πΉ βΎ π¦):π¦βΆπ’) |
24 | 23 | expcom 414 |
. . . . . . . . . . . . . . 15
β’ ((π(ballβπ·)π₯) β π’ β ((πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β (πΉ βΎ π¦):π¦βΆπ’)) |
25 | 24 | reximdv 3170 |
. . . . . . . . . . . . . 14
β’ ((π(ballβπ·)π₯) β π’ β (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) |
26 | 25 | impcom 408 |
. . . . . . . . . . . . 13
β’
((βπ¦ β
ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
27 | 26 | rexlimivw 3151 |
. . . . . . . . . . . 12
β’
(βπ₯ β
β+ (βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ βπ₯ β β+ (π(ballβπ·)π₯) β π’) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
29 | 21, 28 | sylan2 593 |
. . . . . . . . . 10
β’
((βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β§ (π· β (βMetβπ) β§ π’ β π½ β§ π β π’)) β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) |
30 | 29 | 3exp2 1354 |
. . . . . . . . 9
β’
(βπ₯ β
β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯) β (π· β (βMetβπ) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) |
31 | 30 | impcom 408 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ βπ₯ β β+
βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
32 | 31 | adantlr 713 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β (π’ β π½ β (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
33 | 32 | ralrimiv 3145 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) |
34 | 20, 33 | impbida 799 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (πΉ β (π βpm β) β§ π β π)) β (βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’) β βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
35 | 34 | pm5.32da 579 |
. . . 4
β’ (π· β (βMetβπ) β (((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
36 | | df-3an 1089 |
. . . 4
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’))) |
37 | | df-3an 1089 |
. . . 4
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)) β ((πΉ β (π βpm β) β§ π β π) β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯))) |
38 | 35, 36, 37 | 3bitr4g 313 |
. . 3
β’ (π· β (βMetβπ) β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
39 | 1, 38 | syl 17 |
. 2
β’ (π β ((πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)) β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |
40 | 5, 39 | bitrd 278 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran
β€β₯(πΉ
βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) |