Metamath Proof Explorer

Theorem heiborlem9

Description: Lemma for heibor . Discharge the hypotheses of heiborlem8 by applying caubl to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-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 ) )
heibor.9 
|- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
heibor.10 
|- ( ph -> C G 0 )
heibor.11 
|- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )
heibor.12 
|- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
heibor.13 
|- ( ph -> U C_ J )
heiborlem9.14 
|- ( ph -> U. U = X )
Assertion heiborlem9 
|- ( ph -> ps )

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 heibor.9 
 |-  ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
9 heibor.10 
 |-  ( ph -> C G 0 )
10 heibor.11 
 |-  S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )
11 heibor.12 
 |-  M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
12 heibor.13 
 |-  ( ph -> U C_ J )
13 heiborlem9.14 
 |-  ( ph -> U. U = X )
14 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
15 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
16 5 14 15 3syl 
 |-  ( ph -> D e. ( *Met ` X ) )
17 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
18 16 17 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
19 1 2 3 4 5 6 7 8 9 10 11 heiborlem5 
 |-  ( ph -> M : NN --> ( X X. RR+ ) )
20 1 2 3 4 5 6 7 8 9 10 11 heiborlem6 
 |-  ( ph -> A. k e. NN ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( M ` k ) ) )
21 1 2 3 4 5 6 7 8 9 10 11 heiborlem7 
 |-  A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r
22 21 a1i 
 |-  ( ph -> A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r )
23 16 19 20 22 caubl 
 |-  ( ph -> ( 1st o. M ) e. ( Cau ` D ) )
24 1 cmetcau 
 |-  ( ( D e. ( CMet ` X ) /\ ( 1st o. M ) e. ( Cau ` D ) ) -> ( 1st o. M ) e. dom ( ~~>t ` J ) )
25 5 23 24 syl2anc 
 |-  ( ph -> ( 1st o. M ) e. dom ( ~~>t ` J ) )
26 1 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
27 16 26 syl 
 |-  ( ph -> J e. Haus )
28 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
29 funfvbrb 
 |-  ( Fun ( ~~>t ` J ) -> ( ( 1st o. M ) e. dom ( ~~>t ` J ) <-> ( 1st o. M ) ( ~~>t ` J ) ( ( ~~>t ` J ) ` ( 1st o. M ) ) ) )
30 27 28 29 3syl 
 |-  ( ph -> ( ( 1st o. M ) e. dom ( ~~>t ` J ) <-> ( 1st o. M ) ( ~~>t ` J ) ( ( ~~>t ` J ) ` ( 1st o. M ) ) ) )
31 25 30 mpbid 
 |-  ( ph -> ( 1st o. M ) ( ~~>t ` J ) ( ( ~~>t ` J ) ` ( 1st o. M ) ) )
32 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( 1st o. M ) ( ~~>t ` J ) ( ( ~~>t ` J ) ` ( 1st o. M ) ) ) -> ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. X )
33 18 31 32 syl2anc 
 |-  ( ph -> ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. X )
34 33 13 eleqtrrd 
 |-  ( ph -> ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. U. U )
35 eluni2 
 |-  ( ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. U. U <-> E. t e. U ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t )
36 34 35 sylib 
 |-  ( ph -> E. t e. U ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t )
37 5 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> D e. ( CMet ` X ) )
38 6 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> F : NN0 --> ( ~P X i^i Fin ) )
39 7 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
40 8 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
41 9 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> C G 0 )
42 12 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> U C_ J )
43 fvex 
 |-  ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. _V
44 simprr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t )
45 simprl 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> t e. U )
46 31 adantr 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> ( 1st o. M ) ( ~~>t ` J ) ( ( ~~>t ` J ) ` ( 1st o. M ) ) )
47 1 2 3 4 37 38 39 40 41 10 11 42 43 44 45 46 heiborlem8 
 |-  ( ( ph /\ ( t e. U /\ ( ( ~~>t ` J ) ` ( 1st o. M ) ) e. t ) ) -> ps )
48 36 47 rexlimddv 
 |-  ( ph -> ps )