Step | Hyp | Ref
| Expression |
1 | | distop 22368 |
. . . 4
β’ (π΄ β Fin β π«
π΄ β
Top) |
2 | | pwfi 9128 |
. . . . 5
β’ (π΄ β Fin β π«
π΄ β
Fin) |
3 | 2 | biimpi 215 |
. . . 4
β’ (π΄ β Fin β π«
π΄ β
Fin) |
4 | 1, 3 | elind 4158 |
. . 3
β’ (π΄ β Fin β π«
π΄ β (Top β©
Fin)) |
5 | | fincmp 22767 |
. . 3
β’
(π« π΄ β
(Top β© Fin) β π« π΄ β Comp) |
6 | 4, 5 | syl 17 |
. 2
β’ (π΄ β Fin β π«
π΄ β
Comp) |
7 | | simpr 486 |
. . . . . . . 8
β’
((π« π΄ β
Comp β§ π₯ β π΄) β π₯ β π΄) |
8 | 7 | snssd 4773 |
. . . . . . 7
β’
((π« π΄ β
Comp β§ π₯ β π΄) β {π₯} β π΄) |
9 | | vsnex 5390 |
. . . . . . . 8
β’ {π₯} β V |
10 | 9 | elpw 4568 |
. . . . . . 7
β’ ({π₯} β π« π΄ β {π₯} β π΄) |
11 | 8, 10 | sylibr 233 |
. . . . . 6
β’
((π« π΄ β
Comp β§ π₯ β π΄) β {π₯} β π« π΄) |
12 | 11 | fmpttd 7067 |
. . . . 5
β’
(π« π΄ β
Comp β (π₯ β π΄ β¦ {π₯}):π΄βΆπ« π΄) |
13 | 12 | frnd 6680 |
. . . 4
β’
(π« π΄ β
Comp β ran (π₯ β
π΄ β¦ {π₯}) β π« π΄) |
14 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π΄ β¦ {π₯}) = (π₯ β π΄ β¦ {π₯}) |
15 | 14 | rnmpt 5914 |
. . . . . . 7
β’ ran
(π₯ β π΄ β¦ {π₯}) = {π¦ β£ βπ₯ β π΄ π¦ = {π₯}} |
16 | 15 | unieqi 4882 |
. . . . . 6
β’ βͺ ran (π₯ β π΄ β¦ {π₯}) = βͺ {π¦ β£ βπ₯ β π΄ π¦ = {π₯}} |
17 | 9 | dfiun2 4997 |
. . . . . 6
β’ βͺ π₯ β π΄ {π₯} = βͺ {π¦ β£ βπ₯ β π΄ π¦ = {π₯}} |
18 | | iunid 5024 |
. . . . . 6
β’ βͺ π₯ β π΄ {π₯} = π΄ |
19 | 16, 17, 18 | 3eqtr2ri 2768 |
. . . . 5
β’ π΄ = βͺ
ran (π₯ β π΄ β¦ {π₯}) |
20 | 19 | a1i 11 |
. . . 4
β’
(π« π΄ β
Comp β π΄ = βͺ ran (π₯ β π΄ β¦ {π₯})) |
21 | | unipw 5411 |
. . . . . 6
β’ βͺ π« π΄ = π΄ |
22 | 21 | eqcomi 2742 |
. . . . 5
β’ π΄ = βͺ
π« π΄ |
23 | 22 | cmpcov 22763 |
. . . 4
β’
((π« π΄ β
Comp β§ ran (π₯ β
π΄ β¦ {π₯}) β π« π΄ β§ π΄ = βͺ ran (π₯ β π΄ β¦ {π₯})) β βπ¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin)π΄ = βͺ π¦) |
24 | 13, 20, 23 | mpd3an23 1464 |
. . 3
β’
(π« π΄ β
Comp β βπ¦ β
(π« ran (π₯ β
π΄ β¦ {π₯}) β© Fin)π΄ = βͺ π¦) |
25 | | elinel2 4160 |
. . . . . 6
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β π¦ β Fin) |
26 | | elinel1 4159 |
. . . . . . . 8
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β π¦ β π« ran (π₯ β π΄ β¦ {π₯})) |
27 | 26 | elpwid 4573 |
. . . . . . 7
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β π¦ β ran (π₯ β π΄ β¦ {π₯})) |
28 | | snfi 8994 |
. . . . . . . . . 10
β’ {π₯} β Fin |
29 | 28 | rgenw 3065 |
. . . . . . . . 9
β’
βπ₯ β
π΄ {π₯} β Fin |
30 | 14 | fmpt 7062 |
. . . . . . . . 9
β’
(βπ₯ β
π΄ {π₯} β Fin β (π₯ β π΄ β¦ {π₯}):π΄βΆFin) |
31 | 29, 30 | mpbi 229 |
. . . . . . . 8
β’ (π₯ β π΄ β¦ {π₯}):π΄βΆFin |
32 | | frn 6679 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ {π₯}):π΄βΆFin β ran (π₯ β π΄ β¦ {π₯}) β Fin) |
33 | 31, 32 | mp1i 13 |
. . . . . . 7
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β ran (π₯ β π΄ β¦ {π₯}) β Fin) |
34 | 27, 33 | sstrd 3958 |
. . . . . 6
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β π¦ β Fin) |
35 | | unifi 9291 |
. . . . . 6
β’ ((π¦ β Fin β§ π¦ β Fin) β βͺ π¦
β Fin) |
36 | 25, 34, 35 | syl2anc 585 |
. . . . 5
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β βͺ π¦
β Fin) |
37 | | eleq1 2822 |
. . . . 5
β’ (π΄ = βͺ
π¦ β (π΄ β Fin β βͺ π¦
β Fin)) |
38 | 36, 37 | syl5ibrcom 247 |
. . . 4
β’ (π¦ β (π« ran (π₯ β π΄ β¦ {π₯}) β© Fin) β (π΄ = βͺ π¦ β π΄ β Fin)) |
39 | 38 | rexlimiv 3142 |
. . 3
β’
(βπ¦ β
(π« ran (π₯ β
π΄ β¦ {π₯}) β© Fin)π΄ = βͺ π¦ β π΄ β Fin) |
40 | 24, 39 | syl 17 |
. 2
β’
(π« π΄ β
Comp β π΄ β
Fin) |
41 | 6, 40 | impbii 208 |
1
β’ (π΄ β Fin β π«
π΄ β
Comp) |