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 | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heibor.4 
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
heibor.5 
|- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
heibor.6 
|- ( ph -> D e. ( CMet ` X ) )
heibor.7 
|- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
heibor.8 
|- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
Assertion heiborlem10 
|- ( ( ph /\ ( U C_ J /\ U. J = U. U ) ) -> E. v e. ( ~P U i^i Fin ) U. J = U. v )

Proof

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