Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. . . . 5
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β TopSp) |
2 | | neipcfilu.x |
. . . . . 6
β’ π = (Baseβπ) |
3 | | neipcfilu.j |
. . . . . 6
β’ π½ = (TopOpenβπ) |
4 | 2, 3 | istps 22436 |
. . . . 5
β’ (π β TopSp β π½ β (TopOnβπ)) |
5 | 1, 4 | sylib 217 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π½ β (TopOnβπ)) |
6 | | simp3 1139 |
. . . . 5
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β π) |
7 | 6 | snssd 4813 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β {π} β π) |
8 | 6 | snn0d 4780 |
. . . 4
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β {π} β β
) |
9 | | neifil 23384 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ {π} β π β§ {π} β β
) β ((neiβπ½)β{π}) β (Filβπ)) |
10 | 5, 7, 8, 9 | syl3anc 1372 |
. . 3
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (Filβπ)) |
11 | | filfbas 23352 |
. . 3
β’
(((neiβπ½)β{π}) β (Filβπ) β ((neiβπ½)β{π}) β (fBasβπ)) |
12 | 10, 11 | syl 17 |
. 2
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (fBasβπ)) |
13 | | eqid 2733 |
. . . . . . . . . 10
β’ (π€ β {π}) = (π€ β {π}) |
14 | | imaeq1 6055 |
. . . . . . . . . . 11
β’ (π£ = π€ β (π£ β {π}) = (π€ β {π})) |
15 | 14 | rspceeqv 3634 |
. . . . . . . . . 10
β’ ((π€ β π β§ (π€ β {π}) = (π€ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π})) |
16 | 13, 15 | mpan2 690 |
. . . . . . . . 9
β’ (π€ β π β βπ£ β π (π€ β {π}) = (π£ β {π})) |
17 | | vex 3479 |
. . . . . . . . . . 11
β’ π€ β V |
18 | 17 | imaex 7907 |
. . . . . . . . . 10
β’ (π€ β {π}) β V |
19 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π£ β π β¦ (π£ β {π})) = (π£ β π β¦ (π£ β {π})) |
20 | 19 | elrnmpt 5956 |
. . . . . . . . . 10
β’ ((π€ β {π}) β V β ((π€ β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π}))) |
21 | 18, 20 | ax-mp 5 |
. . . . . . . . 9
β’ ((π€ β {π}) β ran (π£ β π β¦ (π£ β {π})) β βπ£ β π (π€ β {π}) = (π£ β {π})) |
22 | 16, 21 | sylibr 233 |
. . . . . . . 8
β’ (π€ β π β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π}))) |
23 | 22 | ad2antlr 726 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π}))) |
24 | | neipcfilu.u |
. . . . . . . . . . . . 13
β’ π = (UnifStβπ) |
25 | 2, 24, 3 | isusp 23766 |
. . . . . . . . . . . 12
β’ (π β UnifSp β (π β (UnifOnβπ) β§ π½ = (unifTopβπ))) |
26 | 25 | simplbi 499 |
. . . . . . . . . . 11
β’ (π β UnifSp β π β (UnifOnβπ)) |
27 | 26 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β π β (UnifOnβπ)) |
28 | | eqid 2733 |
. . . . . . . . . . 11
β’
(unifTopβπ) =
(unifTopβπ) |
29 | 28 | utopsnneip 23753 |
. . . . . . . . . 10
β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβ(unifTopβπ))β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
30 | 27, 6, 29 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβ(unifTopβπ))β{π}) = ran (π£ β π β¦ (π£ β {π}))) |
31 | 30 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((π€ β {π}) β ((neiβ(unifTopβπ))β{π}) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π})))) |
32 | 31 | ad3antrrr 729 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((π€ β {π}) β ((neiβ(unifTopβπ))β{π}) β (π€ β {π}) β ran (π£ β π β¦ (π£ β {π})))) |
33 | 23, 32 | mpbird 257 |
. . . . . 6
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ((neiβ(unifTopβπ))β{π})) |
34 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ (π£ β π β§ π€ β π β§ ((π€ β {π}) Γ (π€ β {π})) β π£)) β π β UnifSp) |
35 | 34 | 3anassrs 1361 |
. . . . . . . . 9
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β π β UnifSp) |
36 | 25 | simprbi 498 |
. . . . . . . . 9
β’ (π β UnifSp β π½ = (unifTopβπ)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β π½ = (unifTopβπ)) |
38 | 37 | fveq2d 6896 |
. . . . . . 7
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (neiβπ½) = (neiβ(unifTopβπ))) |
39 | 38 | fveq1d 6894 |
. . . . . 6
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((neiβπ½)β{π}) = ((neiβ(unifTopβπ))β{π})) |
40 | 33, 39 | eleqtrrd 2837 |
. . . . 5
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β (π€ β {π}) β ((neiβπ½)β{π})) |
41 | | simpr 486 |
. . . . 5
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β ((π€ β {π}) Γ (π€ β {π})) β π£) |
42 | | id 22 |
. . . . . . . 8
β’ (π = (π€ β {π}) β π = (π€ β {π})) |
43 | 42 | sqxpeqd 5709 |
. . . . . . 7
β’ (π = (π€ β {π}) β (π Γ π) = ((π€ β {π}) Γ (π€ β {π}))) |
44 | 43 | sseq1d 4014 |
. . . . . 6
β’ (π = (π€ β {π}) β ((π Γ π) β π£ β ((π€ β {π}) Γ (π€ β {π})) β π£)) |
45 | 44 | rspcev 3613 |
. . . . 5
β’ (((π€ β {π}) β ((neiβπ½)β{π}) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
46 | 40, 41, 45 | syl2anc 585 |
. . . 4
β’
(((((π β UnifSp
β§ π β TopSp β§
π β π) β§ π£ β π) β§ π€ β π) β§ ((π€ β {π}) Γ (π€ β {π})) β π£) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
47 | 27 | adantr 482 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π β (UnifOnβπ)) |
48 | 6 | adantr 482 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π β π) |
49 | | simpr 486 |
. . . . 5
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β π£ β π) |
50 | | simpll1 1213 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β π β (UnifOnβπ)) |
51 | | simplr 768 |
. . . . . . . 8
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β π’ β π) |
52 | | ustexsym 23720 |
. . . . . . . 8
β’ ((π β (UnifOnβπ) β§ π’ β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π’)) |
53 | 50, 51, 52 | syl2anc 585 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β βπ€ β π (β‘π€ = π€ β§ π€ β π’)) |
54 | 50 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π β (UnifOnβπ)) |
55 | | simplr 768 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π€ β π) |
56 | | ustssxp 23709 |
. . . . . . . . . . . 12
β’ ((π β (UnifOnβπ) β§ π€ β π) β π€ β (π Γ π)) |
57 | 54, 55, 56 | syl2anc 585 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π€ β (π Γ π)) |
58 | | simpll2 1214 |
. . . . . . . . . . . 12
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ ((π’ β π’) β π£ β§ π€ β π β§ (β‘π€ = π€ β§ π€ β π’))) β π β π) |
59 | 58 | 3anassrs 1361 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β π β π) |
60 | | ustneism 23728 |
. . . . . . . . . . 11
β’ ((π€ β (π Γ π) β§ π β π) β ((π€ β {π}) Γ (π€ β {π})) β (π€ β β‘π€)) |
61 | 57, 59, 60 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β ((π€ β {π}) Γ (π€ β {π})) β (π€ β β‘π€)) |
62 | | simprl 770 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β β‘π€ = π€) |
63 | 62 | coeq2d 5863 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β β‘π€) = (π€ β π€)) |
64 | | coss1 5856 |
. . . . . . . . . . . . . 14
β’ (π€ β π’ β (π€ β π€) β (π’ β π€)) |
65 | | coss2 5857 |
. . . . . . . . . . . . . 14
β’ (π€ β π’ β (π’ β π€) β (π’ β π’)) |
66 | 64, 65 | sstrd 3993 |
. . . . . . . . . . . . 13
β’ (π€ β π’ β (π€ β π€) β (π’ β π’)) |
67 | 66 | ad2antll 728 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β π€) β (π’ β π’)) |
68 | | simpllr 775 |
. . . . . . . . . . . 12
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π’ β π’) β π£) |
69 | 67, 68 | sstrd 3993 |
. . . . . . . . . . 11
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β π€) β π£) |
70 | 63, 69 | eqsstrd 4021 |
. . . . . . . . . 10
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β (π€ β β‘π€) β π£) |
71 | 61, 70 | sstrd 3993 |
. . . . . . . . 9
β’
((((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β§ (β‘π€ = π€ β§ π€ β π’)) β ((π€ β {π}) Γ (π€ β {π})) β π£) |
72 | 71 | ex 414 |
. . . . . . . 8
β’
(((((π β
(UnifOnβπ) β§
π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β§ π€ β π) β ((β‘π€ = π€ β§ π€ β π’) β ((π€ β {π}) Γ (π€ β {π})) β π£)) |
73 | 72 | reximdva 3169 |
. . . . . . 7
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β (βπ€ β π (β‘π€ = π€ β§ π€ β π’) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£)) |
74 | 53, 73 | mpd 15 |
. . . . . 6
β’ ((((π β (UnifOnβπ) β§ π β π β§ π£ β π) β§ π’ β π) β§ (π’ β π’) β π£) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
75 | | ustexhalf 23715 |
. . . . . . 7
β’ ((π β (UnifOnβπ) β§ π£ β π) β βπ’ β π (π’ β π’) β π£) |
76 | 75 | 3adant2 1132 |
. . . . . 6
β’ ((π β (UnifOnβπ) β§ π β π β§ π£ β π) β βπ’ β π (π’ β π’) β π£) |
77 | 74, 76 | r19.29a 3163 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β π β§ π£ β π) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
78 | 47, 48, 49, 77 | syl3anc 1372 |
. . . 4
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β βπ€ β π ((π€ β {π}) Γ (π€ β {π})) β π£) |
79 | 46, 78 | r19.29a 3163 |
. . 3
β’ (((π β UnifSp β§ π β TopSp β§ π β π) β§ π£ β π) β βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
80 | 79 | ralrimiva 3147 |
. 2
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β βπ£ β π βπ β ((neiβπ½)β{π})(π Γ π) β π£) |
81 | | iscfilu 23793 |
. . 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 712 |
1
β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (CauFiluβπ)) |