Step | Hyp | Ref
| Expression |
1 | | simp2 1137 |
. . . . 5
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β TopSp) |
2 | | neipcfilu.x |
. . . . . 6
β’ π = (Baseβπ) |
3 | | neipcfilu.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
4 | 2, 3 | istps 22443 |
. . . . 5
β’ (π β TopSp β π½ β (TopOnβπ)) |
5 | 1, 4 | sylib 217 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π½ β (TopOnβπ)) |
6 | | simp3 1138 |
. . . . 5
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β π) |
7 | 6 | snssd 4812 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β {π} β π) |
8 | 6 | snn0d 4779 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β {π} β β
) |
9 | | neifil 23391 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ {π} β π β§ {π} β β
) β ((neiβπ½)β{π}) β (Filβπ)) |
10 | 5, 7, 8, 9 | syl3anc 1371 |
. . 3
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (Filβπ)) |
11 | | filfbas 23359 |
. . 3
β’
(((neiβπ½)β{π}) β (Filβπ) β ((neiβπ½)β{π}) β (fBasβπ)) |
12 | 10, 11 | syl 17 |
. 2
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (fBasβπ)) |
13 | | eqid 2732 |
. . . . . . . . . 10
β’ (π€ β {π}) = (π€ β {π}) |
14 | | imaeq1 6054 |
. . . . . . . . . . 11
β’ (π£ = π€ β (π£ β {π}) = (π€ β {π})) |
15 | 14 | rspceeqv 3633 |
. . . . . . . . . 10
β’ ((π€ β π β§ (π€ β {π}) = (π€ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π})) |
16 | 13, 15 | mpan2 689 |
. . . . . . . . 9
β’ (π€ β π β βπ£ β π (π€ β {π}) = (π£ β {π})) |
17 | | vex 3478 |
. . . . . . . . . . 11
β’ π€ β V |
18 | 17 | imaex 7909 |
. . . . . . . . . 10
β’ (π€ β {π}) β V |
19 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π})) |
20 | 19 | elrnmpt 5955 |
. . . . . . . . . 10
β’ ((π€ β {π}) β V β ((π€ β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π}))) |
21 | 18, 20 | ax-mp 5 |
. . . . . . . . 9
β’ ((π€ β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π})) |
22 | 16, 21 | sylibr 233 |
. . . . . . . 8
β’ (π€ β π β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π}))) |
23 | 22 | ad2antlr 725 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π}))) |
24 | | neipcfilu.u |
. . . . . . . . . . . . 13
β’ π = (UnifStβπ) |
25 | 2, 24, 3 | isusp 23773 |
. . . . . . . . . . . 12
β’ (π β UnifSp β (π β (UnifOnβπ) β§ π½ = (unifTopβπ))) |
26 | 25 | simplbi 498 |
. . . . . . . . . . 11
β’ (π β UnifSp β π β (UnifOnβπ)) |
27 | 26 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β (UnifOnβπ)) |
28 | | eqid 2732 |
. . . . . . . . . . 11
β’
(unifTopβπ) =
(unifTopβπ) |
29 | 28 | utopsnneip 23760 |
. . . . . . . . . 10
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβ(unifTopβπ))β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
30 | 27, 6, 29 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβ(unifTopβπ))β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
31 | 30 | eleq2d 2819 |
. . . . . . . 8
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((π€ β {π}) β ((neiβ(unifTopβπ))β{π}) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π})))) |
32 | 31 | ad3antrrr 728 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((π€ β {π}) β ((neiβ(unifTopβπ))β{π}) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π})))) |
33 | 23, 32 | mpbird 256 |
. . . . . 6
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ((neiβ(unifTopβπ))β{π})) |
34 | | simpl1 1191 |
. . . . . . . . . 10
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ (π£ β π β§ π€ β π β§ ((π€ β {π}) Γ (π€ β {π})) β π£)) β π β UnifSp) |
35 | 34 | 3anassrs 1360 |
. . . . . . . . 9
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β π β UnifSp) |
36 | 25 | simprbi 497 |
. . . . . . . . 9
β’ (π β UnifSp β π½ = (unifTopβπ)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β π½ = (unifTopβπ)) |
38 | 37 | fveq2d 6895 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (neiβπ½) = (neiβ(unifTopβπ))) |
39 | 38 | fveq1d 6893 |
. . . . . 6
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((neiβπ½)β{π}) = ((neiβ(unifTopβπ))β{π})) |
40 | 33, 39 | eleqtrrd 2836 |
. . . . 5
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ((neiβπ½)β{π})) |
41 | | simpr 485 |
. . . . 5
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((π€ β {π}) Γ (π€ β {π})) β π£) |
42 | | id 22 |
. . . . . . . 8
β’ (π = (π€ β {π}) β π = (π€ β {π})) |
43 | 42 | sqxpeqd 5708 |
. . . . . . 7
β’ (π = (π€ β {π}) β (π Γ π) = ((π€ β {π}) Γ (π€ β {π}))) |
44 | 43 | sseq1d 4013 |
. . . . . 6
β’ (π = (π€ β {π}) β ((π Γ π) β π£ β ((π€ β {π}) Γ (π€ β {π})) β π£)) |
45 | 44 | rspcev 3612 |
. . . . 5
β’ (((π€ β {π}) β ((neiβπ½)β{π}) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
46 | 40, 41, 45 | syl2anc 584 |
. . . 4
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
47 | 27 | adantr 481 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π β (UnifOnβπ)) |
48 | 6 | adantr 481 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π β π) |
49 | | simpr 485 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π£ β π) |
50 | | simpll1 1212 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β π β (UnifOnβπ)) |
51 | | simplr 767 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β π’ β π) |
52 | | ustexsym 23727 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π’ β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π’)) |
53 | 50, 51, 52 | syl2anc 584 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β βπ€ β π (β‘π€ = π€ β§ π€ β π’)) |
54 | 50 | ad2antrr 724 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π β (UnifOnβπ)) |
55 | | simplr 767 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π€ β π) |
56 | | ustssxp 23716 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π€ β π) β π€ β (π Γ π)) |
57 | 54, 55, 56 | syl2anc 584 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π€ β (π Γ π)) |
58 | | simpll2 1213 |
. . . . . . . . . . . 12
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ ((π’ β π’) β π£ β§ π€ β π β§ (β‘π€ = π€ β§ π€ β π’))) β π β π) |
59 | 58 | 3anassrs 1360 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π β π) |
60 | | ustneism 23735 |
. . . . . . . . . . 11
β’ ((π€ β (π Γ π) β§ π β π) β ((π€ β {π}) Γ (π€ β {π})) β (π€ β β‘π€)) |
61 | 57, 59, 60 | syl2anc 584 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β ((π€ β {π}) Γ (π€ β {π})) β (π€ β β‘π€)) |
62 | | simprl 769 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β β‘π€ = π€) |
63 | 62 | coeq2d 5862 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β β‘π€) = (π€ β π€)) |
64 | | coss1 5855 |
. . . . . . . . . . . . . 14
β’ (π€ β π’ β (π€ β π€) β (π’ β π€)) |
65 | | coss2 5856 |
. . . . . . . . . . . . . 14
β’ (π€ β π’ β (π’ β π€) β (π’ β π’)) |
66 | 64, 65 | sstrd 3992 |
. . . . . . . . . . . . 13
β’ (π€ β π’ β (π€ β π€) β (π’ β π’)) |
67 | 66 | ad2antll 727 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β π€) β (π’ β π’)) |
68 | | simpllr 774 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π’ β π’) β π£) |
69 | 67, 68 | sstrd 3992 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β π€) β π£) |
70 | 63, 69 | eqsstrd 4020 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β β‘π€) β π£) |
71 | 61, 70 | sstrd 3992 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β ((π€ β {π}) Γ (π€ β {π})) β π£) |
72 | 71 | ex 413 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β ((β‘π€ = π€ β§ π€ β π’) β ((π€ β {π}) Γ (π€ β {π})) β π£)) |
73 | 72 | reximdva 3168 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β (βπ€ β π (β‘π€ = π€ β§ π€ β π’) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£)) |
74 | 53, 73 | mpd 15 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
75 | | ustexhalf 23722 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π£ β π) β βπ’ β π (π’ β π’) β π£) |
76 | 75 | 3adant2 1131 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β π β§ π£ β π) β βπ’ β π (π’ β π’) β π£) |
77 | 74, 76 | r19.29a 3162 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π β§ π£ β π) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
78 | 47, 48, 49, 77 | syl3anc 1371 |
. . . 4
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
79 | 46, 78 | r19.29a 3162 |
. . 3
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
80 | 79 | ralrimiva 3146 |
. 2
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β βπ£ β π βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
81 | | iscfilu 23800 |
. . 3
β’ (π β (UnifOnβπ) β (((neiβπ½)β{π}) β (CauFiluβπ) β (((neiβπ½)β{π}) β (fBasβπ) β§ βπ£ β π βπ β ((neiβπ½)β{π})(π Γ π) β π£))) |
82 | 27, 81 | syl 17 |
. 2
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β (((neiβπ½)β{π}) β (CauFiluβπ) β (((neiβπ½)β{π}) β (fBasβπ) β§ βπ£ β π βπ β ((neiβπ½)β{π})(π Γ π) β π£))) |
83 | 12, 80, 82 | mpbir2and 711 |
1
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (CauFiluβπ)) |