Step | Hyp | Ref
| Expression |
1 | | df-locfin 23010 |
. . . 4
β’ LocFin =
(π β Top β¦
{π¦ β£ (βͺ π =
βͺ π¦ β§ βπ₯ β βͺ πβπ β π (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))}) |
2 | 1 | mptrcl 7007 |
. . 3
β’ (π΄ β (LocFinβπ½) β π½ β Top) |
3 | | eqimss2 4041 |
. . . . . . . . . . 11
β’ (π = βͺ
π¦ β βͺ π¦
β π) |
4 | | sspwuni 5103 |
. . . . . . . . . . 11
β’ (π¦ β π« π β βͺ π¦
β π) |
5 | 3, 4 | sylibr 233 |
. . . . . . . . . 10
β’ (π = βͺ
π¦ β π¦ β π« π) |
6 | | velpw 4607 |
. . . . . . . . . 10
β’ (π¦ β π« π«
π β π¦ β π« π) |
7 | 5, 6 | sylibr 233 |
. . . . . . . . 9
β’ (π = βͺ
π¦ β π¦ β π« π« π) |
8 | 7 | adantr 481 |
. . . . . . . 8
β’ ((π = βͺ
π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin)) β π¦ β π« π«
π) |
9 | 8 | abssi 4067 |
. . . . . . 7
β’ {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β
π« π« π |
10 | | islocfin.1 |
. . . . . . . . 9
β’ π = βͺ
π½ |
11 | 10 | topopn 22407 |
. . . . . . . 8
β’ (π½ β Top β π β π½) |
12 | | pwexg 5376 |
. . . . . . . 8
β’ (π β π½ β π« π β V) |
13 | | pwexg 5376 |
. . . . . . . 8
β’
(π« π β
V β π« π« π β V) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . 7
β’ (π½ β Top β π«
π« π β
V) |
15 | | ssexg 5323 |
. . . . . . 7
β’ (({π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β
π« π« π β§
π« π« π
β V) β {π¦ β£
(π = βͺ π¦
β§ βπ₯ β
π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β
V) |
16 | 9, 14, 15 | sylancr 587 |
. . . . . 6
β’ (π½ β Top β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β
V) |
17 | | unieq 4919 |
. . . . . . . . . . 11
β’ (π = π½ β βͺ π = βͺ
π½) |
18 | 17, 10 | eqtr4di 2790 |
. . . . . . . . . 10
β’ (π = π½ β βͺ π = π) |
19 | 18 | eqeq1d 2734 |
. . . . . . . . 9
β’ (π = π½ β (βͺ π = βͺ
π¦ β π = βͺ π¦)) |
20 | | rexeq 3321 |
. . . . . . . . . 10
β’ (π = π½ β (βπ β π (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin) β
βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))) |
21 | 18, 20 | raleqbidv 3342 |
. . . . . . . . 9
β’ (π = π½ β (βπ₯ β βͺ πβπ β π (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin) β
βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))) |
22 | 19, 21 | anbi12d 631 |
. . . . . . . 8
β’ (π = π½ β ((βͺ π = βͺ
π¦ β§ βπ₯ β βͺ πβπ β π (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin)) β (π = βͺ
π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin)))) |
23 | 22 | abbidv 2801 |
. . . . . . 7
β’ (π = π½ β {π¦ β£ (βͺ π = βͺ
π¦ β§ βπ₯ β βͺ πβπ β π (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} = {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))}) |
24 | 23, 1 | fvmptg 6996 |
. . . . . 6
β’ ((π½ β Top β§ {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β V)
β (LocFinβπ½) =
{π¦ β£ (π = βͺ
π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))}) |
25 | 16, 24 | mpdan 685 |
. . . . 5
β’ (π½ β Top β
(LocFinβπ½) = {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))}) |
26 | 25 | eleq2d 2819 |
. . . 4
β’ (π½ β Top β (π΄ β (LocFinβπ½) β π΄ β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β
Fin))})) |
27 | | elex 3492 |
. . . . . 6
β’ (π΄ β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β π΄ β V) |
28 | 27 | adantl 482 |
. . . . 5
β’ ((π½ β Top β§ π΄ β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))}) β π΄ β V) |
29 | | simpr 485 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π = π) β π = π) |
30 | | islocfin.2 |
. . . . . . . . . 10
β’ π = βͺ
π΄ |
31 | 29, 30 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π½ β Top β§ π = π) β π = βͺ π΄) |
32 | 11 | adantr 481 |
. . . . . . . . 9
β’ ((π½ β Top β§ π = π) β π β π½) |
33 | 31, 32 | eqeltrrd 2834 |
. . . . . . . 8
β’ ((π½ β Top β§ π = π) β βͺ π΄ β π½) |
34 | 33 | elexd 3494 |
. . . . . . 7
β’ ((π½ β Top β§ π = π) β βͺ π΄ β V) |
35 | | uniexb 7750 |
. . . . . . 7
β’ (π΄ β V β βͺ π΄
β V) |
36 | 34, 35 | sylibr 233 |
. . . . . 6
β’ ((π½ β Top β§ π = π) β π΄ β V) |
37 | 36 | adantrr 715 |
. . . . 5
β’ ((π½ β Top β§ (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin))) β π΄ β V) |
38 | | unieq 4919 |
. . . . . . . . 9
β’ (π¦ = π΄ β βͺ π¦ = βͺ
π΄) |
39 | 38, 30 | eqtr4di 2790 |
. . . . . . . 8
β’ (π¦ = π΄ β βͺ π¦ = π) |
40 | 39 | eqeq2d 2743 |
. . . . . . 7
β’ (π¦ = π΄ β (π = βͺ π¦ β π = π)) |
41 | | rabeq 3446 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β {π β π¦ β£ (π β© π) β β
} = {π β π΄ β£ (π β© π) β β
}) |
42 | 41 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π¦ = π΄ β ({π β π¦ β£ (π β© π) β β
} β Fin β {π β π΄ β£ (π β© π) β β
} β Fin)) |
43 | 42 | anbi2d 629 |
. . . . . . . . 9
β’ (π¦ = π΄ β ((π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin) β (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |
44 | 43 | rexbidv 3178 |
. . . . . . . 8
β’ (π¦ = π΄ β (βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin) β
βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |
45 | 44 | ralbidv 3177 |
. . . . . . 7
β’ (π¦ = π΄ β (βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin) β
βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |
46 | 40, 45 | anbi12d 631 |
. . . . . 6
β’ (π¦ = π΄ β ((π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin)) β (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
47 | 46 | elabg 3666 |
. . . . 5
β’ (π΄ β V β (π΄ β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
48 | 28, 37, 47 | pm5.21nd 800 |
. . . 4
β’ (π½ β Top β (π΄ β {π¦ β£ (π = βͺ π¦ β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π¦ β£ (π β© π) β β
} β Fin))} β (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
49 | 26, 48 | bitrd 278 |
. . 3
β’ (π½ β Top β (π΄ β (LocFinβπ½) β (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
50 | 2, 49 | biadanii 820 |
. 2
β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
51 | | 3anass 1095 |
. 2
β’ ((π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β Fin)) β (π½ β Top β§ (π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin)))) |
52 | 50, 51 | bitr4i 277 |
1
β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β
} β
Fin))) |