Step | Hyp | Ref
| Expression |
1 | | df1o2 8423 |
. . . 4
β’
1o = {β
} |
2 | | snfi 8994 |
. . . 4
β’ {β
}
β Fin |
3 | 1, 2 | eqeltri 2830 |
. . 3
β’
1o β Fin |
4 | | imassrn 6028 |
. . . . 5
β’ ((π₯ β β β¦
({β
} Γ {π₯}))
β π) β ran
(π₯ β β β¦
({β
} Γ {π₯})) |
5 | | 0ex 5268 |
. . . . . . . . . 10
β’ β
β V |
6 | | eqid 2733 |
. . . . . . . . . . 11
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
7 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π₯ β β β¦
({β
} Γ {π₯})) =
(π₯ β β β¦
({β
} Γ {π₯})) |
8 | 6, 7 | ismrer1 36347 |
. . . . . . . . . 10
β’ (β
β V β (π₯ β
β β¦ ({β
} Γ {π₯})) β (((abs β β ) βΎ
(β Γ β)) Ismty
(βnβ{β
}))) |
9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ{β
})) |
10 | 1 | fveq2i 6849 |
. . . . . . . . . 10
β’
(βnβ1o) =
(βnβ{β
}) |
11 | 10 | oveq2i 7372 |
. . . . . . . . 9
β’ (((abs
β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) = (((abs β β )
βΎ (β Γ β)) Ismty
(βnβ{β
})) |
12 | 9, 11 | eleqtrri 2833 |
. . . . . . . 8
β’ (π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) |
13 | 6 | rexmet 24177 |
. . . . . . . . 9
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
14 | | eqid 2733 |
. . . . . . . . . . 11
β’ (β
βm 1o) = (β βm
1o) |
15 | 14 | rrnmet 36338 |
. . . . . . . . . 10
β’
(1o β Fin β
(βnβ1o) β (Metβ(β
βm 1o))) |
16 | | metxmet 23710 |
. . . . . . . . . 10
β’
((βnβ1o) β
(Metβ(β βm 1o)) β
(βnβ1o) β
(βMetβ(β βm 1o))) |
17 | 3, 15, 16 | mp2b 10 |
. . . . . . . . 9
β’
(βnβ1o) β
(βMetβ(β βm 1o)) |
18 | | isismty 36310 |
. . . . . . . . 9
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§
(βnβ1o) β
(βMetβ(β βm 1o))) β ((π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) β ((π₯ β β β¦ ({β
} Γ
{π₯})):ββ1-1-ontoβ(β βm 1o)
β§ βπ¦ β
β βπ§ β
β (π¦((abs β
β ) βΎ (β Γ β))π§) = (((π₯ β β β¦ ({β
} Γ
{π₯}))βπ¦)(βnβ1o)((π₯ β β β¦ ({β
} Γ
{π₯}))βπ§))))) |
19 | 13, 17, 18 | mp2an 691 |
. . . . . . . 8
β’ ((π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) β ((π₯ β β β¦ ({β
} Γ
{π₯})):ββ1-1-ontoβ(β βm 1o)
β§ βπ¦ β
β βπ§ β
β (π¦((abs β
β ) βΎ (β Γ β))π§) = (((π₯ β β β¦ ({β
} Γ
{π₯}))βπ¦)(βnβ1o)((π₯ β β β¦ ({β
} Γ
{π₯}))βπ§)))) |
20 | 12, 19 | mpbi 229 |
. . . . . . 7
β’ ((π₯ β β β¦
({β
} Γ {π₯})):ββ1-1-ontoβ(β βm 1o)
β§ βπ¦ β
β βπ§ β
β (π¦((abs β
β ) βΎ (β Γ β))π§) = (((π₯ β β β¦ ({β
} Γ
{π₯}))βπ¦)(βnβ1o)((π₯ β β β¦ ({β
} Γ
{π₯}))βπ§))) |
21 | 20 | simpli 485 |
. . . . . 6
β’ (π₯ β β β¦
({β
} Γ {π₯})):ββ1-1-ontoβ(β βm
1o) |
22 | | f1of 6788 |
. . . . . 6
β’ ((π₯ β β β¦
({β
} Γ {π₯})):ββ1-1-ontoβ(β βm 1o)
β (π₯ β β
β¦ ({β
} Γ {π₯})):ββΆ(β
βm 1o)) |
23 | | frn 6679 |
. . . . . 6
β’ ((π₯ β β β¦
({β
} Γ {π₯})):ββΆ(β
βm 1o) β ran (π₯ β β β¦ ({β
} Γ
{π₯})) β (β
βm 1o)) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
β’ ran
(π₯ β β β¦
({β
} Γ {π₯}))
β (β βm 1o) |
25 | 4, 24 | sstri 3957 |
. . . 4
β’ ((π₯ β β β¦
({β
} Γ {π₯}))
β π) β (β
βm 1o) |
26 | 25 | a1i 11 |
. . 3
β’ (π β β β ((π₯ β β β¦
({β
} Γ {π₯}))
β π) β (β
βm 1o)) |
27 | | eqid 2733 |
. . . 4
β’
((βnβ1o) βΎ (((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π))) =
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) |
28 | | eqid 2733 |
. . . 4
β’
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) =
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) |
29 | | eqid 2733 |
. . . 4
β’
(MetOpenβ(βnβ1o)) =
(MetOpenβ(βnβ1o)) |
30 | 14, 27, 28, 29 | rrnheibor 36346 |
. . 3
β’
((1o β Fin β§ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π) β (β
βm 1o)) β
((MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β Comp
β (((π₯ β β
β¦ ({β
} Γ {π₯})) β π) β
(Clsdβ(MetOpenβ(βnβ1o)))
β§ ((βnβ1o) βΎ (((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π))) β
(Bndβ((π₯ β
β β¦ ({β
} Γ {π₯})) β π))))) |
31 | 3, 26, 30 | sylancr 588 |
. 2
β’ (π β β β
((MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β Comp
β (((π₯ β β
β¦ ({β
} Γ {π₯})) β π) β
(Clsdβ(MetOpenβ(βnβ1o)))
β§ ((βnβ1o) βΎ (((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π))) β
(Bndβ((π₯ β
β β¦ ({β
} Γ {π₯})) β π))))) |
32 | | reheibor.2 |
. . . . . . 7
β’ π = ((abs β β )
βΎ (π Γ π)) |
33 | | cnxmet 24159 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
34 | | id 22 |
. . . . . . . . 9
β’ (π β β β π β
β) |
35 | | ax-resscn 11116 |
. . . . . . . . 9
β’ β
β β |
36 | 34, 35 | sstrdi 3960 |
. . . . . . . 8
β’ (π β β β π β
β) |
37 | | xmetres2 23737 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ π β β) β ((abs β
β ) βΎ (π
Γ π)) β
(βMetβπ)) |
38 | 33, 36, 37 | sylancr 588 |
. . . . . . 7
β’ (π β β β ((abs
β β ) βΎ (π Γ π)) β (βMetβπ)) |
39 | 32, 38 | eqeltrid 2838 |
. . . . . 6
β’ (π β β β π β (βMetβπ)) |
40 | | xmetres2 23737 |
. . . . . . 7
β’
(((βnβ1o) β
(βMetβ(β βm 1o)) β§ ((π₯ β β β¦
({β
} Γ {π₯}))
β π) β (β
βm 1o)) β
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β
(βMetβ((π₯
β β β¦ ({β
} Γ {π₯})) β π))) |
41 | 17, 26, 40 | sylancr 588 |
. . . . . 6
β’ (π β β β
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β
(βMetβ((π₯
β β β¦ ({β
} Γ {π₯})) β π))) |
42 | | reheibor.3 |
. . . . . . 7
β’ π = (MetOpenβπ) |
43 | 42, 28 | ismtyhmeo 36314 |
. . . . . 6
β’ ((π β (βMetβπ) β§
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β
(βMetβ((π₯
β β β¦ ({β
} Γ {π₯})) β π))) β (π Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π)))) β (πHomeo(MetOpenβ((βnβ1o)
βΎ (((π₯ β β β¦ ({β
}
Γ {π₯})) β π) Γ ((π₯
β β β¦ ({β
} Γ {π₯}))
β π)))))) |
44 | 39, 41, 43 | syl2anc 585 |
. . . . 5
β’ (π β β β (π Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π)))) β (πHomeo(MetOpenβ((βnβ1o)
βΎ (((π₯ β β β¦ ({β
}
Γ {π₯})) β π) Γ ((π₯
β β β¦ ({β
} Γ {π₯}))
β π)))))) |
45 | 13 | a1i 11 |
. . . . . . 7
β’ (π β β β ((abs
β β ) βΎ (β Γ β)) β
(βMetββ)) |
46 | 17 | a1i 11 |
. . . . . . 7
β’ (π β β β
(βnβ1o) β
(βMetβ(β βm 1o))) |
47 | 12 | a1i 11 |
. . . . . . 7
β’ (π β β β (π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ1o))) |
48 | | eqid 2733 |
. . . . . . . 8
β’ ((π₯ β β β¦
({β
} Γ {π₯}))
β π) = ((π₯ β β β¦
({β
} Γ {π₯}))
β π) |
49 | | eqid 2733 |
. . . . . . . 8
β’ (((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) = (((abs β β ) βΎ
(β Γ β)) βΎ (π Γ π)) |
50 | 48, 49, 27 | ismtyres 36317 |
. . . . . . 7
β’ (((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§
(βnβ1o) β
(βMetβ(β βm 1o))) β§ ((π₯ β β β¦
({β
} Γ {π₯}))
β (((abs β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) β§ π β β)) β ((π₯ β β β¦
({β
} Γ {π₯}))
βΎ π) β ((((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))))) |
51 | 45, 46, 47, 34, 50 | syl22anc 838 |
. . . . . 6
β’ (π β β β ((π₯ β β β¦
({β
} Γ {π₯}))
βΎ π) β ((((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))))) |
52 | | xpss12 5652 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π Γ π) β (β Γ
β)) |
53 | 52 | anidms 568 |
. . . . . . . . 9
β’ (π β β β (π Γ π) β (β Γ
β)) |
54 | 53 | resabs1d 5972 |
. . . . . . . 8
β’ (π β β β (((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) = ((abs β β ) βΎ (π Γ π))) |
55 | 54, 32 | eqtr4di 2791 |
. . . . . . 7
β’ (π β β β (((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) = π) |
56 | 55 | oveq1d 7376 |
. . . . . 6
β’ (π β β β ((((abs
β β ) βΎ (β Γ β)) βΎ (π Γ π)) Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π)))) = (π Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))))) |
57 | 51, 56 | eleqtrd 2836 |
. . . . 5
β’ (π β β β ((π₯ β β β¦
({β
} Γ {π₯}))
βΎ π) β (π Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))))) |
58 | 44, 57 | sseldd 3949 |
. . . 4
β’ (π β β β ((π₯ β β β¦
({β
} Γ {π₯}))
βΎ π) β (πHomeo(MetOpenβ((βnβ1o)
βΎ (((π₯ β β β¦ ({β
}
Γ {π₯})) β π) Γ ((π₯
β β β¦ ({β
} Γ {π₯}))
β π)))))) |
59 | | hmphi 23151 |
. . . 4
β’ (((π₯ β β β¦
({β
} Γ {π₯}))
βΎ π) β (πHomeo(MetOpenβ((βnβ1o)
βΎ (((π₯ β β β¦ ({β
}
Γ {π₯})) β π) Γ ((π₯
β β β¦ ({β
} Γ {π₯}))
β π))))) β π β
(MetOpenβ((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ {π₯})) β π)
Γ ((π₯ β β β¦ ({β
}
Γ {π₯})) β π))))) |
60 | 58, 59 | syl 17 |
. . 3
β’ (π β β β π β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π))))) |
61 | | cmphmph 23162 |
. . . 4
β’ (π β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β (π β Comp β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β
Comp)) |
62 | | hmphsym 23156 |
. . . . 5
β’ (π β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β π) |
63 | | cmphmph 23162 |
. . . . 5
β’
((MetOpenβ((βnβ1o)
βΎ (((π₯ β β
β¦ ({β
} Γ {π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π)))) β π β
((MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β Comp
β π β
Comp)) |
64 | 62, 63 | syl 17 |
. . . 4
β’ (π β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β
((MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β Comp
β π β
Comp)) |
65 | 61, 64 | impbid 211 |
. . 3
β’ (π β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β (π β Comp β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β
Comp)) |
66 | 60, 65 | syl 17 |
. 2
β’ (π β β β (π β Comp β
(MetOpenβ((βnβ1o) βΎ
(((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) β
Comp)) |
67 | | reheibor.4 |
. . . . . . . 8
β’ π = (topGenβran
(,)) |
68 | | eqid 2733 |
. . . . . . . . 9
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
69 | 6, 68 | tgioo 24182 |
. . . . . . . 8
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
70 | 67, 69 | eqtri 2761 |
. . . . . . 7
β’ π = (MetOpenβ((abs β
β ) βΎ (β Γ β))) |
71 | 70, 29 | ismtyhmeo 36314 |
. . . . . 6
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§
(βnβ1o) β
(βMetβ(β βm 1o))) β (((abs
β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) β (πHomeo(MetOpenβ(βnβ1o)))) |
72 | 13, 17, 71 | mp2an 691 |
. . . . 5
β’ (((abs
β β ) βΎ (β Γ β)) Ismty
(βnβ1o)) β (πHomeo(MetOpenβ(βnβ1o))) |
73 | 72, 12 | sselii 3945 |
. . . 4
β’ (π₯ β β β¦
({β
} Γ {π₯}))
β (πHomeo(MetOpenβ(βnβ1o))) |
74 | | retopon 24150 |
. . . . . . 7
β’
(topGenβran (,)) β (TopOnββ) |
75 | 67, 74 | eqeltri 2830 |
. . . . . 6
β’ π β
(TopOnββ) |
76 | 75 | toponunii 22288 |
. . . . 5
β’ β =
βͺ π |
77 | 76 | hmeocld 23141 |
. . . 4
β’ (((π₯ β β β¦
({β
} Γ {π₯}))
β (πHomeo(MetOpenβ(βnβ1o)))
β§ π β β) β (π β (Clsdβπ) β ((π₯
β β β¦ ({β
} Γ {π₯}))
β π) β
(Clsdβ(MetOpenβ(βnβ1o))))) |
78 | 73, 34, 77 | sylancr 588 |
. . 3
β’ (π β β β (π β (Clsdβπ) β ((π₯ β β β¦ ({β
} Γ
{π₯})) β π) β
(Clsdβ(MetOpenβ(βnβ1o))))) |
79 | | ismtybnd 36316 |
. . . 4
β’ ((π β (βMetβπ) β§
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β
(βMetβ((π₯
β β β¦ ({β
} Γ {π₯})) β π)) β§ ((π₯ β β β¦ ({β
} Γ
{π₯})) βΎ π) β (π Ismty
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))))) β (π β (Bndβπ) β
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β (Bndβ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) |
80 | 39, 41, 57, 79 | syl3anc 1372 |
. . 3
β’ (π β β β (π β (Bndβπ) β
((βnβ1o) βΎ (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) Γ ((π₯ β β β¦ ({β
} Γ
{π₯})) β π))) β (Bndβ((π₯ β β β¦
({β
} Γ {π₯}))
β π)))) |
81 | 78, 80 | anbi12d 632 |
. 2
β’ (π β β β ((π β (Clsdβπ) β§ π β (Bndβπ)) β (((π₯ β β β¦ ({β
} Γ
{π₯})) β π) β
(Clsdβ(MetOpenβ(βnβ1o)))
β§ ((βnβ1o) βΎ (((π₯ β β β¦
({β
} Γ {π₯}))
β π) Γ ((π₯ β β β¦
({β
} Γ {π₯}))
β π))) β
(Bndβ((π₯ β
β β¦ ({β
} Γ {π₯})) β π))))) |
82 | 31, 66, 81 | 3bitr4d 311 |
1
β’ (π β β β (π β Comp β (π β (Clsdβπ) β§ π β (Bndβπ)))) |