Step | Hyp | Ref
| Expression |
1 | | locfintop 22895 |
. . . . 5
β’ (π΄ β (LocFinβπ½) β π½ β Top) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β π½ β Top) |
3 | | ssequn2 4147 |
. . . . . . . 8
β’ (βͺ π΅
β βͺ π½ β (βͺ π½ βͺ βͺ π΅) =
βͺ π½) |
4 | 3 | biimpi 215 |
. . . . . . 7
β’ (βͺ π΅
β βͺ π½ β (βͺ π½ βͺ βͺ π΅) =
βͺ π½) |
5 | 4 | adantl 483 |
. . . . . 6
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β (βͺ π½ βͺ βͺ π΅) =
βͺ π½) |
6 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
7 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π΄ =
βͺ π΄ |
8 | 6, 7 | locfinbas 22896 |
. . . . . . . 8
β’ (π΄ β (LocFinβπ½) β βͺ π½ =
βͺ π΄) |
9 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β βͺ π½ = βͺ
π΄) |
10 | 9 | uneq1d 4126 |
. . . . . 6
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β (βͺ π½ βͺ βͺ π΅) =
(βͺ π΄ βͺ βͺ π΅)) |
11 | 5, 10 | eqtr3d 2775 |
. . . . 5
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β βͺ π½ = (βͺ
π΄ βͺ βͺ π΅)) |
12 | | uniun 4895 |
. . . . 5
β’ βͺ (π΄
βͺ π΅) = (βͺ π΄
βͺ βͺ π΅) |
13 | 11, 12 | eqtr4di 2791 |
. . . 4
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β βͺ π½ = βͺ
(π΄ βͺ π΅)) |
14 | 6 | locfinnei 22897 |
. . . . . . 7
β’ ((π΄ β (LocFinβπ½) β§ π₯ β βͺ π½) β βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
15 | 14 | ad4ant14 751 |
. . . . . 6
β’ ((((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β§ π₯ β βͺ π½) β βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) |
16 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ {π β π΄ β£ (π β© π) β β
} β Fin) β {π β π΄ β£ (π β© π) β β
} β Fin) |
17 | | rabfi 9219 |
. . . . . . . . . . . 12
β’ (π΅ β Fin β {π β π΅ β£ (π β© π) β β
} β Fin) |
18 | 17 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ {π β π΄ β£ (π β© π) β β
} β Fin) β {π β π΅ β£ (π β© π) β β
} β Fin) |
19 | | rabun2 4277 |
. . . . . . . . . . . 12
β’ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} = ({π β π΄ β£ (π β© π) β β
} βͺ {π β π΅ β£ (π β© π) β β
}) |
20 | | unfi 9122 |
. . . . . . . . . . . 12
β’ (({π β π΄ β£ (π β© π) β β
} β Fin β§ {π β π΅ β£ (π β© π) β β
} β Fin) β ({π β π΄ β£ (π β© π) β β
} βͺ {π β π΅ β£ (π β© π) β β
}) β Fin) |
21 | 19, 20 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (({π β π΄ β£ (π β© π) β β
} β Fin β§ {π β π΅ β£ (π β© π) β β
} β Fin) β {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin) |
22 | 16, 18, 21 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ {π β π΄ β£ (π β© π) β β
} β Fin) β {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin) |
23 | 22 | ex 414 |
. . . . . . . . 9
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin) β ({π β π΄ β£ (π β© π) β β
} β Fin β {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin)) |
24 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β§ π₯ β βͺ π½) β ({π β π΄ β£ (π β© π) β β
} β Fin β {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin)) |
25 | 24 | anim2d 613 |
. . . . . . 7
β’ ((((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β§ π₯ β βͺ π½) β ((π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin) β (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β
Fin))) |
26 | 25 | reximdv 3164 |
. . . . . 6
β’ ((((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β§ π₯ β βͺ π½) β (βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin) β
βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β
Fin))) |
27 | 15, 26 | mpd 15 |
. . . . 5
β’ ((((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β§ π₯ β βͺ π½) β βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin)) |
28 | 27 | ralrimiva 3140 |
. . . 4
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β βπ₯ β βͺ π½βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β Fin)) |
29 | 2, 13, 28 | 3jca 1129 |
. . 3
β’ (((π΄ β (LocFinβπ½) β§ π΅ β Fin) β§ βͺ π΅
β βͺ π½) β (π½ β Top β§ βͺ π½ =
βͺ (π΄ βͺ π΅) β§ βπ₯ β βͺ π½βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β
Fin))) |
30 | 29 | 3impa 1111 |
. 2
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin β§ βͺ π΅
β βͺ π½) β (π½ β Top β§ βͺ π½ =
βͺ (π΄ βͺ π΅) β§ βπ₯ β βͺ π½βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β
Fin))) |
31 | | eqid 2733 |
. . 3
β’ βͺ (π΄
βͺ π΅) = βͺ (π΄
βͺ π΅) |
32 | 6, 31 | islocfin 22891 |
. 2
β’ ((π΄ βͺ π΅) β (LocFinβπ½) β (π½ β Top β§ βͺ π½ =
βͺ (π΄ βͺ π΅) β§ βπ₯ β βͺ π½βπ β π½ (π₯ β π β§ {π β (π΄ βͺ π΅) β£ (π β© π) β β
} β
Fin))) |
33 | 30, 32 | sylibr 233 |
1
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin β§ βͺ π΅
β βͺ π½) β (π΄ βͺ π΅) β (LocFinβπ½)) |