Step | Hyp | Ref
| Expression |
1 | | lmcvg.3 |
. 2
β’ (π β π β π) |
2 | | eleq2 2823 |
. . . 4
β’ (π’ = π β (π β π’ β π β π)) |
3 | | eleq2 2823 |
. . . . 5
β’ (π’ = π β ((πΉβπ) β π’ β (πΉβπ) β π)) |
4 | 3 | rexralbidv 3221 |
. . . 4
β’ (π’ = π β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π)) |
5 | 2, 4 | imbi12d 345 |
. . 3
β’ (π’ = π β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π))) |
6 | | lmcvg.5 |
. . . . . 6
β’ (π β πΉ(βπ‘βπ½)π) |
7 | | lmrcl 22735 |
. . . . . . . . 9
β’ (πΉ(βπ‘βπ½)π β π½ β Top) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β π½ β Top) |
9 | | toptopon2 22420 |
. . . . . . . 8
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
10 | 8, 9 | sylib 217 |
. . . . . . 7
β’ (π β π½ β (TopOnββͺ π½)) |
11 | | lmcvg.1 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
12 | | lmcvg.4 |
. . . . . . 7
β’ (π β π β β€) |
13 | 10, 11, 12 | lmbr2 22763 |
. . . . . 6
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (βͺ π½ βpm β)
β§ π β βͺ π½
β§ βπ’ β
π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))))) |
14 | 6, 13 | mpbid 231 |
. . . . 5
β’ (π β (πΉ β (βͺ π½ βpm β)
β§ π β βͺ π½
β§ βπ’ β
π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)))) |
15 | 14 | simp3d 1145 |
. . . 4
β’ (π β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’))) |
16 | | simpr 486 |
. . . . . . . 8
β’ ((π β dom πΉ β§ (πΉβπ) β π’) β (πΉβπ) β π’) |
17 | 16 | ralimi 3084 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β (β€β₯βπ)(πΉβπ) β π’) |
18 | 17 | reximi 3085 |
. . . . . 6
β’
(βπ β
π βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) |
19 | 18 | imim2i 16 |
. . . . 5
β’ ((π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) |
20 | 19 | ralimi 3084 |
. . . 4
β’
(βπ’ β
π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π’)) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) |
21 | 15, 20 | syl 17 |
. . 3
β’ (π β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) |
22 | | lmcvg.6 |
. . 3
β’ (π β π β π½) |
23 | 5, 21, 22 | rspcdva 3614 |
. 2
β’ (π β (π β π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π)) |
24 | 1, 23 | mpd 15 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π) |