Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π΄ =
βͺ π΄ |
3 | 1, 2 | locfinbas 22896 |
. . . . . . 7
β’ (π΄ β (LocFinβπ½) β βͺ π½ =
βͺ π΄) |
4 | 3 | eleq2d 2820 |
. . . . . 6
β’ (π΄ β (LocFinβπ½) β (π₯ β βͺ π½ β π₯ β βͺ π΄)) |
5 | 4 | biimpar 479 |
. . . . 5
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β π₯ β βͺ π½) |
6 | 1 | locfinnei 22897 |
. . . . 5
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π½) β βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
7 | 5, 6 | syldan 592 |
. . . 4
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
8 | | inelcm 4428 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π₯ β π) β (π β© π) β β
) |
9 | 8 | expcom 415 |
. . . . . . . . 9
β’ (π₯ β π β (π₯ β π β (π β© π) β β
)) |
10 | 9 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β§ π₯ β π) β§ π β π΄) β (π₯ β π β (π β© π) β β
)) |
11 | 10 | ss2rabdv 4037 |
. . . . . . 7
β’ (((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β§ π₯ β π) β {π β π΄ β£ π₯ β π } β {π β π΄ β£ (π β© π) β β
}) |
12 | | ssfi 9123 |
. . . . . . . 8
β’ (({π β π΄ β£ (π β© π) β β
} β Fin β§ {π β π΄ β£ π₯ β π } β {π β π΄ β£ (π β© π) β β
}) β {π β π΄ β£ π₯ β π } β Fin) |
13 | 12 | expcom 415 |
. . . . . . 7
β’ ({π β π΄ β£ π₯ β π } β {π β π΄ β£ (π β© π) β β
} β ({π β π΄ β£ (π β© π) β β
} β Fin β {π β π΄ β£ π₯ β π } β Fin)) |
14 | 11, 13 | syl 17 |
. . . . . 6
β’ (((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β§ π₯ β π) β ({π β π΄ β£ (π β© π) β β
} β Fin β {π β π΄ β£ π₯ β π } β Fin)) |
15 | 14 | expimpd 455 |
. . . . 5
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β ((π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin) β {π β π΄ β£ π₯ β π } β Fin)) |
16 | 15 | rexlimdvw 3154 |
. . . 4
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β (βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin) β {π β π΄ β£ π₯ β π } β Fin)) |
17 | 7, 16 | mpd 15 |
. . 3
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π΄) β {π β π΄ β£ π₯ β π } β Fin) |
18 | 17 | ralrimiva 3140 |
. 2
β’ (π΄ β (LocFinβπ½) β βπ₯ β βͺ π΄{π β π΄ β£ π₯ β π } β Fin) |
19 | 2 | isptfin 22890 |
. 2
β’ (π΄ β (LocFinβπ½) β (π΄ β PtFin β βπ₯ β βͺ π΄{π β π΄ β£ π₯ β π } β Fin)) |
20 | 18, 19 | mpbird 257 |
1
β’ (π΄ β (LocFinβπ½) β π΄ β PtFin) |