Step | Hyp | Ref
| Expression |
1 | | topontop 22415 |
. . . . 5
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β πΎ β Top) |
3 | | toponuni 22416 |
. . . . . 6
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
4 | 3 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β π = βͺ πΎ) |
5 | | locfincf.1 |
. . . . . . 7
β’ π = βͺ
π½ |
6 | | eqid 2733 |
. . . . . . 7
β’ βͺ π₯ =
βͺ π₯ |
7 | 5, 6 | locfinbas 23026 |
. . . . . 6
β’ (π₯ β (LocFinβπ½) β π = βͺ π₯) |
8 | 7 | adantl 483 |
. . . . 5
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β π = βͺ π₯) |
9 | 4, 8 | eqtr3d 2775 |
. . . 4
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β βͺ πΎ = βͺ
π₯) |
10 | 4 | eleq2d 2820 |
. . . . . 6
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β (π¦ β π β π¦ β βͺ πΎ)) |
11 | 5 | locfinnei 23027 |
. . . . . . . 8
β’ ((π₯ β (LocFinβπ½) β§ π¦ β π) β βπ β π½ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β Fin)) |
12 | 11 | ex 414 |
. . . . . . 7
β’ (π₯ β (LocFinβπ½) β (π¦ β π β βπ β π½ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
13 | | ssrexv 4052 |
. . . . . . . 8
β’ (π½ β πΎ β (βπ β π½ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β Fin) β
βπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((πΎ β (TopOnβπ) β§ π½ β πΎ) β (βπ β π½ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β Fin) β
βπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
15 | 12, 14 | sylan9r 510 |
. . . . . 6
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β (π¦ β π β βπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
16 | 10, 15 | sylbird 260 |
. . . . 5
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β (π¦ β βͺ πΎ β βπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
17 | 16 | ralrimiv 3146 |
. . . 4
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β βπ¦ β βͺ πΎβπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β Fin)) |
18 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
19 | 18, 6 | islocfin 23021 |
. . . 4
β’ (π₯ β (LocFinβπΎ) β (πΎ β Top β§ βͺ πΎ =
βͺ π₯ β§ βπ¦ β βͺ πΎβπ β πΎ (π¦ β π β§ {π β π₯ β£ (π β© π) β β
} β
Fin))) |
20 | 2, 9, 17, 19 | syl3anbrc 1344 |
. . 3
β’ (((πΎ β (TopOnβπ) β§ π½ β πΎ) β§ π₯ β (LocFinβπ½)) β π₯ β (LocFinβπΎ)) |
21 | 20 | ex 414 |
. 2
β’ ((πΎ β (TopOnβπ) β§ π½ β πΎ) β (π₯ β (LocFinβπ½) β π₯ β (LocFinβπΎ))) |
22 | 21 | ssrdv 3989 |
1
β’ ((πΎ β (TopOnβπ) β§ π½ β πΎ) β (LocFinβπ½) β (LocFinβπΎ)) |