Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. 2
β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π½ β Top) |
2 | | simp3 1135 |
. 2
β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π = π) |
3 | | simpl1 1188 |
. . . . 5
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β π½ β Top) |
4 | | finlocfin.1 |
. . . . . 6
β’ π = βͺ
π½ |
5 | 4 | topopn 22763 |
. . . . 5
β’ (π½ β Top β π β π½) |
6 | 3, 5 | syl 17 |
. . . 4
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β π β π½) |
7 | | simpr 484 |
. . . 4
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β π₯ β π) |
8 | | simpl2 1189 |
. . . . 5
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β π΄ β Fin) |
9 | | ssrab2 4072 |
. . . . 5
β’ {π β π΄ β£ (π β© π) β β
} β π΄ |
10 | | ssfi 9175 |
. . . . 5
β’ ((π΄ β Fin β§ {π β π΄ β£ (π β© π) β β
} β π΄) β {π β π΄ β£ (π β© π) β β
} β Fin) |
11 | 8, 9, 10 | sylancl 585 |
. . . 4
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β {π β π΄ β£ (π β© π) β β
} β Fin) |
12 | | eleq2 2816 |
. . . . . 6
β’ (π = π β (π₯ β π β π₯ β π)) |
13 | | ineq2 4201 |
. . . . . . . . 9
β’ (π = π β (π β© π) = (π β© π)) |
14 | 13 | neeq1d 2994 |
. . . . . . . 8
β’ (π = π β ((π β© π) β β
β (π β© π) β β
)) |
15 | 14 | rabbidv 3434 |
. . . . . . 7
β’ (π = π β {π β π΄ β£ (π β© π) β β
} = {π β π΄ β£ (π β© π) β β
}) |
16 | 15 | eleq1d 2812 |
. . . . . 6
β’ (π = π β ({π β π΄ β£ (π β© π) β β
} β Fin β {π β π΄ β£ (π β© π) β β
} β
Fin)) |
17 | 12, 16 | anbi12d 630 |
. . . . 5
β’ (π = π β ((π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin) β (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |
18 | 17 | rspcev 3606 |
. . . 4
β’ ((π β π½ β§ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) β
βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
19 | 6, 7, 11, 18 | syl12anc 834 |
. . 3
β’ (((π½ β Top β§ π΄ β Fin β§ π = π) β§ π₯ β π) β βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
20 | 19 | ralrimiva 3140 |
. 2
β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
21 | | finlocfin.2 |
. . 3
β’ π = βͺ
π΄ |
22 | 4, 21 | islocfin 23376 |
. 2
β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |
23 | 1, 2, 20, 22 | syl3anbrc 1340 |
1
β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π΄ β (LocFinβπ½)) |