Metamath Proof Explorer


Theorem reheibor

Description: Heine-Borel theorem for real numbers. A subset of RR is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses reheibor.2 M = abs Y × Y
reheibor.3 T = MetOpen M
reheibor.4 U = topGen ran .
Assertion reheibor Y T Comp Y Clsd U M Bnd Y

Proof

Step Hyp Ref Expression
1 reheibor.2 M = abs Y × Y
2 reheibor.3 T = MetOpen M
3 reheibor.4 U = topGen ran .
4 df1o2 1 𝑜 =
5 snfi Fin
6 4 5 eqeltri 1 𝑜 Fin
7 imassrn x × x Y ran x × x
8 0ex V
9 eqid abs 2 = abs 2
10 eqid x × x = x × x
11 9 10 ismrer1 V x × x abs 2 Ismty n
12 8 11 ax-mp x × x abs 2 Ismty n
13 4 fveq2i n 1 𝑜 = n
14 13 oveq2i abs 2 Ismty n 1 𝑜 = abs 2 Ismty n
15 12 14 eleqtrri x × x abs 2 Ismty n 1 𝑜
16 9 rexmet abs 2 ∞Met
17 eqid 1 𝑜 = 1 𝑜
18 17 rrnmet 1 𝑜 Fin n 1 𝑜 Met 1 𝑜
19 metxmet n 1 𝑜 Met 1 𝑜 n 1 𝑜 ∞Met 1 𝑜
20 6 18 19 mp2b n 1 𝑜 ∞Met 1 𝑜
21 isismty abs 2 ∞Met n 1 𝑜 ∞Met 1 𝑜 x × x abs 2 Ismty n 1 𝑜 x × x : 1-1 onto 1 𝑜 y z y abs 2 z = x × x y n 1 𝑜 x × x z
22 16 20 21 mp2an x × x abs 2 Ismty n 1 𝑜 x × x : 1-1 onto 1 𝑜 y z y abs 2 z = x × x y n 1 𝑜 x × x z
23 15 22 mpbi x × x : 1-1 onto 1 𝑜 y z y abs 2 z = x × x y n 1 𝑜 x × x z
24 23 simpli x × x : 1-1 onto 1 𝑜
25 f1of x × x : 1-1 onto 1 𝑜 x × x : 1 𝑜
26 frn x × x : 1 𝑜 ran x × x 1 𝑜
27 24 25 26 mp2b ran x × x 1 𝑜
28 7 27 sstri x × x Y 1 𝑜
29 28 a1i Y x × x Y 1 𝑜
30 eqid n 1 𝑜 x × x Y × x × x Y = n 1 𝑜 x × x Y × x × x Y
31 eqid MetOpen n 1 𝑜 x × x Y × x × x Y = MetOpen n 1 𝑜 x × x Y × x × x Y
32 eqid MetOpen n 1 𝑜 = MetOpen n 1 𝑜
33 17 30 31 32 rrnheibor 1 𝑜 Fin x × x Y 1 𝑜 MetOpen n 1 𝑜 x × x Y × x × x Y Comp x × x Y Clsd MetOpen n 1 𝑜 n 1 𝑜 x × x Y × x × x Y Bnd x × x Y
34 6 29 33 sylancr Y MetOpen n 1 𝑜 x × x Y × x × x Y Comp x × x Y Clsd MetOpen n 1 𝑜 n 1 𝑜 x × x Y × x × x Y Bnd x × x Y
35 cnxmet abs ∞Met
36 id Y Y
37 ax-resscn
38 36 37 sstrdi Y Y
39 xmetres2 abs ∞Met Y abs Y × Y ∞Met Y
40 35 38 39 sylancr Y abs Y × Y ∞Met Y
41 1 40 eqeltrid Y M ∞Met Y
42 xmetres2 n 1 𝑜 ∞Met 1 𝑜 x × x Y 1 𝑜 n 1 𝑜 x × x Y × x × x Y ∞Met x × x Y
43 20 29 42 sylancr Y n 1 𝑜 x × x Y × x × x Y ∞Met x × x Y
44 2 31 ismtyhmeo M ∞Met Y n 1 𝑜 x × x Y × x × x Y ∞Met x × x Y M Ismty n 1 𝑜 x × x Y × x × x Y T Homeo MetOpen n 1 𝑜 x × x Y × x × x Y
45 41 43 44 syl2anc Y M Ismty n 1 𝑜 x × x Y × x × x Y T Homeo MetOpen n 1 𝑜 x × x Y × x × x Y
46 16 a1i Y abs 2 ∞Met
47 20 a1i Y n 1 𝑜 ∞Met 1 𝑜
48 15 a1i Y x × x abs 2 Ismty n 1 𝑜
49 eqid x × x Y = x × x Y
50 eqid abs 2 Y × Y = abs 2 Y × Y
51 49 50 30 ismtyres abs 2 ∞Met n 1 𝑜 ∞Met 1 𝑜 x × x abs 2 Ismty n 1 𝑜 Y x × x Y abs 2 Y × Y Ismty n 1 𝑜 x × x Y × x × x Y
52 46 47 48 36 51 syl22anc Y x × x Y abs 2 Y × Y Ismty n 1 𝑜 x × x Y × x × x Y
53 xpss12 Y Y Y × Y 2
54 53 anidms Y Y × Y 2
55 54 resabs1d Y abs 2 Y × Y = abs Y × Y
56 55 1 eqtr4di Y abs 2 Y × Y = M
57 56 oveq1d Y abs 2 Y × Y Ismty n 1 𝑜 x × x Y × x × x Y = M Ismty n 1 𝑜 x × x Y × x × x Y
58 52 57 eleqtrd Y x × x Y M Ismty n 1 𝑜 x × x Y × x × x Y
59 45 58 sseldd Y x × x Y T Homeo MetOpen n 1 𝑜 x × x Y × x × x Y
60 hmphi x × x Y T Homeo MetOpen n 1 𝑜 x × x Y × x × x Y T MetOpen n 1 𝑜 x × x Y × x × x Y
61 59 60 syl Y T MetOpen n 1 𝑜 x × x Y × x × x Y
62 cmphmph T MetOpen n 1 𝑜 x × x Y × x × x Y T Comp MetOpen n 1 𝑜 x × x Y × x × x Y Comp
63 hmphsym T MetOpen n 1 𝑜 x × x Y × x × x Y MetOpen n 1 𝑜 x × x Y × x × x Y T
64 cmphmph MetOpen n 1 𝑜 x × x Y × x × x Y T MetOpen n 1 𝑜 x × x Y × x × x Y Comp T Comp
65 63 64 syl T MetOpen n 1 𝑜 x × x Y × x × x Y MetOpen n 1 𝑜 x × x Y × x × x Y Comp T Comp
66 62 65 impbid T MetOpen n 1 𝑜 x × x Y × x × x Y T Comp MetOpen n 1 𝑜 x × x Y × x × x Y Comp
67 61 66 syl Y T Comp MetOpen n 1 𝑜 x × x Y × x × x Y Comp
68 eqid MetOpen abs 2 = MetOpen abs 2
69 9 68 tgioo topGen ran . = MetOpen abs 2
70 3 69 eqtri U = MetOpen abs 2
71 70 32 ismtyhmeo abs 2 ∞Met n 1 𝑜 ∞Met 1 𝑜 abs 2 Ismty n 1 𝑜 U Homeo MetOpen n 1 𝑜
72 16 20 71 mp2an abs 2 Ismty n 1 𝑜 U Homeo MetOpen n 1 𝑜
73 72 15 sselii x × x U Homeo MetOpen n 1 𝑜
74 retopon topGen ran . TopOn
75 3 74 eqeltri U TopOn
76 75 toponunii = U
77 76 hmeocld x × x U Homeo MetOpen n 1 𝑜 Y Y Clsd U x × x Y Clsd MetOpen n 1 𝑜
78 73 36 77 sylancr Y Y Clsd U x × x Y Clsd MetOpen n 1 𝑜
79 ismtybnd M ∞Met Y n 1 𝑜 x × x Y × x × x Y ∞Met x × x Y x × x Y M Ismty n 1 𝑜 x × x Y × x × x Y M Bnd Y n 1 𝑜 x × x Y × x × x Y Bnd x × x Y
80 41 43 58 79 syl3anc Y M Bnd Y n 1 𝑜 x × x Y × x × x Y Bnd x × x Y
81 78 80 anbi12d Y Y Clsd U M Bnd Y x × x Y Clsd MetOpen n 1 𝑜 n 1 𝑜 x × x Y × x × x Y Bnd x × x Y
82 34 67 81 3bitr4d Y T Comp Y Clsd U M Bnd Y