Metamath Proof Explorer


Theorem heiborlem10

Description: Lemma for heibor . The last remaining piece of the proof is to find an element C such that C G 0 , i.e. C is an element of ( F0 ) that has no finite subcover, which is true by heiborlem1 , since ( F0 ) is a finite cover of X , which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of U that covers X , i.e. X is compact. (Contributed by Jeff Madsen, 22-Jan-2014)

Ref Expression
Hypotheses heibor.1 J = MetOpen D
heibor.3 K = u | ¬ v 𝒫 U Fin u v
heibor.4 G = y n | n 0 y F n y B n K
heibor.5 B = z X , m 0 z ball D 1 2 m
heibor.6 φ D CMet X
heibor.7 φ F : 0 𝒫 X Fin
heibor.8 φ n 0 X = y F n y B n
Assertion heiborlem10 φ U J J = U v 𝒫 U Fin J = v

Proof

Step Hyp Ref Expression
1 heibor.1 J = MetOpen D
2 heibor.3 K = u | ¬ v 𝒫 U Fin u v
3 heibor.4 G = y n | n 0 y F n y B n K
4 heibor.5 B = z X , m 0 z ball D 1 2 m
5 heibor.6 φ D CMet X
6 heibor.7 φ F : 0 𝒫 X Fin
7 heibor.8 φ n 0 X = y F n y B n
8 0nn0 0 0
9 inss2 𝒫 X Fin Fin
10 ffvelrn F : 0 𝒫 X Fin 0 0 F 0 𝒫 X Fin
11 9 10 sseldi F : 0 𝒫 X Fin 0 0 F 0 Fin
12 6 8 11 sylancl φ F 0 Fin
13 fveq2 n = 0 F n = F 0
14 oveq2 n = 0 y B n = y B 0
15 13 14 iuneq12d n = 0 y F n y B n = y F 0 y B 0
16 15 eqeq2d n = 0 X = y F n y B n X = y F 0 y B 0
17 16 rspccva n 0 X = y F n y B n 0 0 X = y F 0 y B 0
18 7 8 17 sylancl φ X = y F 0 y B 0
19 eqimss X = y F 0 y B 0 X y F 0 y B 0
20 18 19 syl φ X y F 0 y B 0
21 ovex y B 0 V
22 1 2 21 heiborlem1 F 0 Fin X y F 0 y B 0 X K y F 0 y B 0 K
23 oveq1 y = x y B 0 = x B 0
24 23 eleq1d y = x y B 0 K x B 0 K
25 24 cbvrexvw y F 0 y B 0 K x F 0 x B 0 K
26 22 25 sylib F 0 Fin X y F 0 y B 0 X K x F 0 x B 0 K
27 26 3expia F 0 Fin X y F 0 y B 0 X K x F 0 x B 0 K
28 12 20 27 syl2anc φ X K x F 0 x B 0 K
29 28 adantr φ U J J = U X K x F 0 x B 0 K
30 vex x V
31 c0ex 0 V
32 1 2 3 30 31 heiborlem2 x G 0 0 0 x F 0 x B 0 K
33 1 2 3 4 5 6 7 heiborlem3 φ g x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K
34 33 ad2antrr φ U J J = U x G 0 g x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K
35 5 ad2antrr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K D CMet X
36 6 ad2antrr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K F : 0 𝒫 X Fin
37 7 ad2antrr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K n 0 X = y F n y B n
38 simprr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K
39 fveq2 x = t g x = g t
40 fveq2 x = t 2 nd x = 2 nd t
41 40 oveq1d x = t 2 nd x + 1 = 2 nd t + 1
42 39 41 breq12d x = t g x G 2 nd x + 1 g t G 2 nd t + 1
43 fveq2 x = t B x = B t
44 39 41 oveq12d x = t g x B 2 nd x + 1 = g t B 2 nd t + 1
45 43 44 ineq12d x = t B x g x B 2 nd x + 1 = B t g t B 2 nd t + 1
46 45 eleq1d x = t B x g x B 2 nd x + 1 K B t g t B 2 nd t + 1 K
47 42 46 anbi12d x = t g x G 2 nd x + 1 B x g x B 2 nd x + 1 K g t G 2 nd t + 1 B t g t B 2 nd t + 1 K
48 47 cbvralvw x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K t G g t G 2 nd t + 1 B t g t B 2 nd t + 1 K
49 38 48 sylib φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K t G g t G 2 nd t + 1 B t g t B 2 nd t + 1 K
50 simprl φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K x G 0
51 eqeq1 g = m g = 0 m = 0
52 oveq1 g = m g 1 = m 1
53 51 52 ifbieq2d g = m if g = 0 x g 1 = if m = 0 x m 1
54 53 cbvmptv g 0 if g = 0 x g 1 = m 0 if m = 0 x m 1
55 seqeq3 g 0 if g = 0 x g 1 = m 0 if m = 0 x m 1 seq 0 g g 0 if g = 0 x g 1 = seq 0 g m 0 if m = 0 x m 1
56 54 55 ax-mp seq 0 g g 0 if g = 0 x g 1 = seq 0 g m 0 if m = 0 x m 1
57 eqid n seq 0 g g 0 if g = 0 x g 1 n 3 2 n = n seq 0 g g 0 if g = 0 x g 1 n 3 2 n
58 simplrl φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K U J
59 cmetmet D CMet X D Met X
60 metxmet D Met X D ∞Met X
61 1 mopnuni D ∞Met X X = J
62 5 59 60 61 4syl φ X = J
63 62 adantr φ U J J = U X = J
64 simprr φ U J J = U J = U
65 63 64 eqtr2d φ U J J = U U = X
66 65 adantr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K U = X
67 1 2 3 4 35 36 37 49 50 56 57 58 66 heiborlem9 φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K ¬ X K
68 67 expr φ U J J = U x G 0 x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K ¬ X K
69 68 exlimdv φ U J J = U x G 0 g x G g x G 2 nd x + 1 B x g x B 2 nd x + 1 K ¬ X K
70 34 69 mpd φ U J J = U x G 0 ¬ X K
71 32 70 sylan2br φ U J J = U 0 0 x F 0 x B 0 K ¬ X K
72 71 3exp2 φ U J J = U 0 0 x F 0 x B 0 K ¬ X K
73 8 72 mpi φ U J J = U x F 0 x B 0 K ¬ X K
74 73 rexlimdv φ U J J = U x F 0 x B 0 K ¬ X K
75 29 74 syld φ U J J = U X K ¬ X K
76 75 pm2.01d φ U J J = U ¬ X K
77 elfvdm D CMet X X dom CMet
78 sseq1 u = X u v X v
79 78 rexbidv u = X v 𝒫 U Fin u v v 𝒫 U Fin X v
80 79 notbid u = X ¬ v 𝒫 U Fin u v ¬ v 𝒫 U Fin X v
81 80 2 elab2g X dom CMet X K ¬ v 𝒫 U Fin X v
82 5 77 81 3syl φ X K ¬ v 𝒫 U Fin X v
83 82 adantr φ U J J = U X K ¬ v 𝒫 U Fin X v
84 83 con2bid φ U J J = U v 𝒫 U Fin X v ¬ X K
85 76 84 mpbird φ U J J = U v 𝒫 U Fin X v
86 62 ad2antrr φ U J J = U v 𝒫 U Fin X = J
87 86 sseq1d φ U J J = U v 𝒫 U Fin X v J v
88 inss1 𝒫 U Fin 𝒫 U
89 88 sseli v 𝒫 U Fin v 𝒫 U
90 89 elpwid v 𝒫 U Fin v U
91 simprl φ U J J = U U J
92 sstr v U U J v J
93 92 unissd v U U J v J
94 90 91 93 syl2anr φ U J J = U v 𝒫 U Fin v J
95 94 biantrud φ U J J = U v 𝒫 U Fin J v J v v J
96 eqss J = v J v v J
97 95 96 bitr4di φ U J J = U v 𝒫 U Fin J v J = v
98 87 97 bitrd φ U J J = U v 𝒫 U Fin X v J = v
99 98 rexbidva φ U J J = U v 𝒫 U Fin X v v 𝒫 U Fin J = v
100 85 99 mpbid φ U J J = U v 𝒫 U Fin J = v