Metamath Proof Explorer

Theorem heiborlem5

Description: Lemma for heibor . The function M is a set of point-and-radius pairs suitable for application to caubl . (Contributed by Jeff Madsen, 23-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 ) ) >. )
Assertion heiborlem5 
|- ( ph -> M : NN --> ( X X. RR+ ) )

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 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
13 inss1 
 |-  ( ~P X i^i Fin ) C_ ~P X
14 6 ffvelcdmda 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. ( ~P X i^i Fin ) )
15 13 14 sselid 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. ~P X )
16 15 elpwid 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) C_ X )
17 1 2 3 4 5 6 7 8 9 10 heiborlem4 
 |-  ( ( ph /\ k e. NN0 ) -> ( S ` k ) G k )
18 fvex 
 |-  ( S ` k ) e. _V
19 vex 
 |-  k e. _V
20 1 2 3 18 19 heiborlem2 
 |-  ( ( S ` k ) G k <-> ( k e. NN0 /\ ( S ` k ) e. ( F ` k ) /\ ( ( S ` k ) B k ) e. K ) )
21 20 simp2bi 
 |-  ( ( S ` k ) G k -> ( S ` k ) e. ( F ` k ) )
22 17 21 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( S ` k ) e. ( F ` k ) )
23 16 22 sseldd 
 |-  ( ( ph /\ k e. NN0 ) -> ( S ` k ) e. X )
24 12 23 sylan2 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. X )
25 24 ralrimiva 
 |-  ( ph -> A. k e. NN ( S ` k ) e. X )
26 fveq2 
 |-  ( k = n -> ( S ` k ) = ( S ` n ) )
27 26 eleq1d 
 |-  ( k = n -> ( ( S ` k ) e. X <-> ( S ` n ) e. X ) )
28 27 cbvralvw 
 |-  ( A. k e. NN ( S ` k ) e. X <-> A. n e. NN ( S ` n ) e. X )
29 25 28 sylib 
 |-  ( ph -> A. n e. NN ( S ` n ) e. X )
30 3re 
 |-  3 e. RR
31 3pos 
 |-  0 < 3
32 30 31 elrpii 
 |-  3 e. RR+
33 2nn 
 |-  2 e. NN
34 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
35 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
36 33 34 35 sylancr 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
37 36 nnrpd 
 |-  ( n e. NN -> ( 2 ^ n ) e. RR+ )
38 rpdivcl 
 |-  ( ( 3 e. RR+ /\ ( 2 ^ n ) e. RR+ ) -> ( 3 / ( 2 ^ n ) ) e. RR+ )
39 32 37 38 sylancr 
 |-  ( n e. NN -> ( 3 / ( 2 ^ n ) ) e. RR+ )
40 opelxpi 
 |-  ( ( ( S ` n ) e. X /\ ( 3 / ( 2 ^ n ) ) e. RR+ ) -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) )
41 40 expcom 
 |-  ( ( 3 / ( 2 ^ n ) ) e. RR+ -> ( ( S ` n ) e. X -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) ) )
42 39 41 syl 
 |-  ( n e. NN -> ( ( S ` n ) e. X -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) ) )
43 42 ralimia 
 |-  ( A. n e. NN ( S ` n ) e. X -> A. n e. NN <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) )
44 29 43 syl 
 |-  ( ph -> A. n e. NN <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) )
45 11 fmpt 
 |-  ( A. n e. NN <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. e. ( X X. RR+ ) <-> M : NN --> ( X X. RR+ ) )
46 44 45 sylib 
 |-  ( ph -> M : NN --> ( X X. RR+ ) )