Step | Hyp | Ref
| Expression |
1 | | simpl2 1001 |
. . 3
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β πΉ:π΄βΆβ) |
2 | | eqid 2177 |
. . . . . 6
β’
((MetOpenβ(abs β β )) βΎt π΄) = ((MetOpenβ(abs β
β )) βΎt π΄) |
3 | | eqid 2177 |
. . . . . 6
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
4 | 2, 3 | dvcnp2cntop 14202 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π₯ β dom (π D πΉ)) β πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯)) |
5 | 4 | ralrimiva 2550 |
. . . 4
β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β βπ₯ β dom (π D πΉ)πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯)) |
6 | | raleq 2673 |
. . . . 5
β’ (dom
(π D πΉ) = π΄ β (βπ₯ β dom (π D πΉ)πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯) β
βπ₯ β π΄ πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯))) |
7 | 6 | biimpd 144 |
. . . 4
β’ (dom
(π D πΉ) = π΄ β (βπ₯ β dom (π D πΉ)πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯) β
βπ₯ β π΄ πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯))) |
8 | 5, 7 | mpan9 281 |
. . 3
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β βπ₯ β π΄ πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯)) |
9 | 3 | cntoptopon 14071 |
. . . . 5
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
10 | | simpl3 1002 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β π΄ β π) |
11 | | simpl1 1000 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β π β β) |
12 | 10, 11 | sstrd 3167 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β π΄ β β) |
13 | | resttopon 13710 |
. . . . 5
β’
(((MetOpenβ(abs β β )) β (TopOnββ)
β§ π΄ β β)
β ((MetOpenβ(abs β β )) βΎt π΄) β (TopOnβπ΄)) |
14 | 9, 12, 13 | sylancr 414 |
. . . 4
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β ((MetOpenβ(abs β
β )) βΎt π΄) β (TopOnβπ΄)) |
15 | | cncnp 13769 |
. . . 4
β’
((((MetOpenβ(abs β β )) βΎt π΄) β (TopOnβπ΄) β§ (MetOpenβ(abs
β β )) β (TopOnββ)) β (πΉ β (((MetOpenβ(abs β
β )) βΎt π΄) Cn (MetOpenβ(abs β β )))
β (πΉ:π΄βΆβ β§ βπ₯ β π΄ πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯)))) |
16 | 14, 9, 15 | sylancl 413 |
. . 3
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β (πΉ β (((MetOpenβ(abs β
β )) βΎt π΄) Cn (MetOpenβ(abs β β )))
β (πΉ:π΄βΆβ β§ βπ₯ β π΄ πΉ β ((((MetOpenβ(abs β
β )) βΎt π΄) CnP (MetOpenβ(abs β β
)))βπ₯)))) |
17 | 1, 8, 16 | mpbir2and 944 |
. 2
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β πΉ β (((MetOpenβ(abs β
β )) βΎt π΄) Cn (MetOpenβ(abs β β
)))) |
18 | | ssid 3177 |
. . 3
β’ β
β β |
19 | 9 | toponrestid 13560 |
. . . 4
β’
(MetOpenβ(abs β β )) = ((MetOpenβ(abs β
β )) βΎt β) |
20 | 3, 2, 19 | cncfcncntop 14119 |
. . 3
β’ ((π΄ β β β§ β
β β) β (π΄βcnββ) = (((MetOpenβ(abs β β
)) βΎt π΄)
Cn (MetOpenβ(abs β β )))) |
21 | 12, 18, 20 | sylancl 413 |
. 2
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β (π΄βcnββ) = (((MetOpenβ(abs β β
)) βΎt π΄)
Cn (MetOpenβ(abs β β )))) |
22 | 17, 21 | eleqtrrd 2257 |
1
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β πΉ β (π΄βcnββ)) |