Step | Hyp | Ref
| Expression |
1 | | qndenserrn.i |
. . . . 5
β’ (π β πΌ β Fin) |
2 | | qndenserrn.j |
. . . . . 6
β’ π½ =
(TopOpenβ(β^βπΌ)) |
3 | 2 | rrxtop 45582 |
. . . . 5
β’ (πΌ β Fin β π½ β Top) |
4 | 1, 3 | syl 17 |
. . . 4
β’ (π β π½ β Top) |
5 | | reex 11203 |
. . . . . . 7
β’ β
β V |
6 | | qssre 12947 |
. . . . . . 7
β’ β
β β |
7 | | mapss 8885 |
. . . . . . 7
β’ ((β
β V β§ β β β) β (β βm
πΌ) β (β
βm πΌ)) |
8 | 5, 6, 7 | mp2an 689 |
. . . . . 6
β’ (β
βm πΌ)
β (β βm πΌ) |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β (β
βm πΌ)
β (β βm πΌ)) |
10 | | eqid 2726 |
. . . . . . . 8
β’
(β^βπΌ) =
(β^βπΌ) |
11 | | eqid 2726 |
. . . . . . . 8
β’
(Baseβ(β^βπΌ)) = (Baseβ(β^βπΌ)) |
12 | 1, 10, 11 | rrxbasefi 25293 |
. . . . . . 7
β’ (π β
(Baseβ(β^βπΌ)) = (β βm πΌ)) |
13 | 12 | eqcomd 2732 |
. . . . . 6
β’ (π β (β
βm πΌ) =
(Baseβ(β^βπΌ))) |
14 | | rrxtps 45579 |
. . . . . . 7
β’ (πΌ β Fin β
(β^βπΌ) β
TopSp) |
15 | | eqid 2726 |
. . . . . . . 8
β’
(TopOpenβ(β^βπΌ)) = (TopOpenβ(β^βπΌ)) |
16 | 11, 15 | tpsuni 22793 |
. . . . . . 7
β’
((β^βπΌ)
β TopSp β (Baseβ(β^βπΌ)) = βͺ
(TopOpenβ(β^βπΌ))) |
17 | 1, 14, 16 | 3syl 18 |
. . . . . 6
β’ (π β
(Baseβ(β^βπΌ)) = βͺ
(TopOpenβ(β^βπΌ))) |
18 | 2 | unieqi 4914 |
. . . . . . . 8
β’ βͺ π½ =
βͺ (TopOpenβ(β^βπΌ)) |
19 | 18 | eqcomi 2735 |
. . . . . . 7
β’ βͺ (TopOpenβ(β^βπΌ)) = βͺ π½ |
20 | 19 | a1i 11 |
. . . . . 6
β’ (π β βͺ (TopOpenβ(β^βπΌ)) = βͺ π½) |
21 | 13, 17, 20 | 3eqtrd 2770 |
. . . . 5
β’ (π β (β
βm πΌ) =
βͺ π½) |
22 | 9, 21 | sseqtrd 4017 |
. . . 4
β’ (π β (β
βm πΌ)
β βͺ π½) |
23 | | eqid 2726 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
24 | 23 | clsss3 22918 |
. . . 4
β’ ((π½ β Top β§ (β
βm πΌ)
β βͺ π½) β ((clsβπ½)β(β βm πΌ)) β βͺ π½) |
25 | 4, 22, 24 | syl2anc 583 |
. . 3
β’ (π β ((clsβπ½)β(β
βm πΌ))
β βͺ π½) |
26 | 21 | eqcomd 2732 |
. . 3
β’ (π β βͺ π½ =
(β βm πΌ)) |
27 | 25, 26 | sseqtrd 4017 |
. 2
β’ (π β ((clsβπ½)β(β
βm πΌ))
β (β βm πΌ)) |
28 | 1 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β§ π£ β π½) β§ π₯ β π£) β πΌ β Fin) |
29 | | id 22 |
. . . . . . . . . . . 12
β’ (π£ β π½ β π£ β π½) |
30 | 29, 2 | eleqtrdi 2837 |
. . . . . . . . . . 11
β’ (π£ β π½ β π£ β (TopOpenβ(β^βπΌ))) |
31 | 30 | ad2antlr 724 |
. . . . . . . . . 10
β’ (((π β§ π£ β π½) β§ π₯ β π£) β π£ β (TopOpenβ(β^βπΌ))) |
32 | | ne0i 4329 |
. . . . . . . . . . 11
β’ (π₯ β π£ β π£ β β
) |
33 | 32 | adantl 481 |
. . . . . . . . . 10
β’ (((π β§ π£ β π½) β§ π₯ β π£) β π£ β β
) |
34 | 28, 15, 31, 33 | qndenserrnopn 45591 |
. . . . . . . . 9
β’ (((π β§ π£ β π½) β§ π₯ β π£) β βπ¦ β (β βm πΌ)π¦ β π£) |
35 | | df-rex 3065 |
. . . . . . . . 9
β’
(βπ¦ β
(β βm πΌ)π¦ β π£ β βπ¦(π¦ β (β βm πΌ) β§ π¦ β π£)) |
36 | 34, 35 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π£ β π½) β§ π₯ β π£) β βπ¦(π¦ β (β βm πΌ) β§ π¦ β π£)) |
37 | | simpr 484 |
. . . . . . . . . . 11
β’ ((π¦ β (β
βm πΌ) β§
π¦ β π£) β π¦ β π£) |
38 | | simpl 482 |
. . . . . . . . . . 11
β’ ((π¦ β (β
βm πΌ) β§
π¦ β π£) β π¦ β (β βm πΌ)) |
39 | 37, 38 | elind 4189 |
. . . . . . . . . 10
β’ ((π¦ β (β
βm πΌ) β§
π¦ β π£) β π¦ β (π£ β© (β βm πΌ))) |
40 | 39 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π£ β π½) β§ π₯ β π£) β ((π¦ β (β βm πΌ) β§ π¦ β π£) β π¦ β (π£ β© (β βm πΌ)))) |
41 | 40 | eximdv 1912 |
. . . . . . . 8
β’ (((π β§ π£ β π½) β§ π₯ β π£) β (βπ¦(π¦ β (β βm πΌ) β§ π¦ β π£) β βπ¦ π¦ β (π£ β© (β βm πΌ)))) |
42 | 36, 41 | mpd 15 |
. . . . . . 7
β’ (((π β§ π£ β π½) β§ π₯ β π£) β βπ¦ π¦ β (π£ β© (β βm πΌ))) |
43 | | n0 4341 |
. . . . . . 7
β’ ((π£ β© (β
βm πΌ)) β
β
β βπ¦
π¦ β (π£ β© (β
βm πΌ))) |
44 | 42, 43 | sylibr 233 |
. . . . . 6
β’ (((π β§ π£ β π½) β§ π₯ β π£) β (π£ β© (β βm πΌ)) β
β
) |
45 | 44 | ex 412 |
. . . . 5
β’ ((π β§ π£ β π½) β (π₯ β π£ β (π£ β© (β βm πΌ)) β
β
)) |
46 | 45 | adantlr 712 |
. . . 4
β’ (((π β§ π₯ β (β βm πΌ)) β§ π£ β π½) β (π₯ β π£ β (π£ β© (β βm πΌ)) β
β
)) |
47 | 46 | ralrimiva 3140 |
. . 3
β’ ((π β§ π₯ β (β βm πΌ)) β βπ£ β π½ (π₯ β π£ β (π£ β© (β βm πΌ)) β
β
)) |
48 | 4 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β (β βm πΌ)) β π½ β Top) |
49 | 22 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β (β βm πΌ)) β (β
βm πΌ)
β βͺ π½) |
50 | | simpr 484 |
. . . . 5
β’ ((π β§ π₯ β (β βm πΌ)) β π₯ β (β βm πΌ)) |
51 | 21 | adantr 480 |
. . . . 5
β’ ((π β§ π₯ β (β βm πΌ)) β (β
βm πΌ) =
βͺ π½) |
52 | 50, 51 | eleqtrd 2829 |
. . . 4
β’ ((π β§ π₯ β (β βm πΌ)) β π₯ β βͺ π½) |
53 | 23 | elcls 22932 |
. . . 4
β’ ((π½ β Top β§ (β
βm πΌ)
β βͺ π½ β§ π₯ β βͺ π½) β (π₯ β ((clsβπ½)β(β βm πΌ)) β βπ£ β π½ (π₯ β π£ β (π£ β© (β βm πΌ)) β
β
))) |
54 | 48, 49, 52, 53 | syl3anc 1368 |
. . 3
β’ ((π β§ π₯ β (β βm πΌ)) β (π₯ β ((clsβπ½)β(β βm πΌ)) β βπ£ β π½ (π₯ β π£ β (π£ β© (β βm πΌ)) β
β
))) |
55 | 47, 54 | mpbird 257 |
. 2
β’ ((π β§ π₯ β (β βm πΌ)) β π₯ β ((clsβπ½)β(β βm πΌ))) |
56 | 27, 55 | eqelssd 3998 |
1
β’ (π β ((clsβπ½)β(β
βm πΌ)) =
(β βm πΌ)) |