Metamath Proof Explorer

Theorem heiborlem4

Description: Lemma for heibor . Using the function T constructed in heiborlem3 , construct an infinite path in G . (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 ) ) ) )
Assertion heiborlem4 
|- ( ( ph /\ A e. NN0 ) -> ( S ` A ) G A )

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 fveq2 
 |-  ( x = 0 -> ( S ` x ) = ( S ` 0 ) )
12 id 
 |-  ( x = 0 -> x = 0 )
13 11 12 breq12d 
 |-  ( x = 0 -> ( ( S ` x ) G x <-> ( S ` 0 ) G 0 ) )
14 13 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( S ` x ) G x ) <-> ( ph -> ( S ` 0 ) G 0 ) ) )
15 fveq2 
 |-  ( x = k -> ( S ` x ) = ( S ` k ) )
16 id 
 |-  ( x = k -> x = k )
17 15 16 breq12d 
 |-  ( x = k -> ( ( S ` x ) G x <-> ( S ` k ) G k ) )
18 17 imbi2d 
 |-  ( x = k -> ( ( ph -> ( S ` x ) G x ) <-> ( ph -> ( S ` k ) G k ) ) )
19 fveq2 
 |-  ( x = ( k + 1 ) -> ( S ` x ) = ( S ` ( k + 1 ) ) )
20 id 
 |-  ( x = ( k + 1 ) -> x = ( k + 1 ) )
21 19 20 breq12d 
 |-  ( x = ( k + 1 ) -> ( ( S ` x ) G x <-> ( S ` ( k + 1 ) ) G ( k + 1 ) ) )
22 21 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( S ` x ) G x ) <-> ( ph -> ( S ` ( k + 1 ) ) G ( k + 1 ) ) ) )
23 fveq2 
 |-  ( x = A -> ( S ` x ) = ( S ` A ) )
24 id 
 |-  ( x = A -> x = A )
25 23 24 breq12d 
 |-  ( x = A -> ( ( S ` x ) G x <-> ( S ` A ) G A ) )
26 25 imbi2d 
 |-  ( x = A -> ( ( ph -> ( S ` x ) G x ) <-> ( ph -> ( S ` A ) G A ) ) )
27 10 fveq1i 
 |-  ( S ` 0 ) = ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` 0 )
28 0z 
 |-  0 e. ZZ
29 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` 0 ) = ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` 0 ) )
30 28 29 ax-mp 
 |-  ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` 0 ) = ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` 0 )
31 27 30 eqtri 
 |-  ( S ` 0 ) = ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` 0 )
32 0nn0 
 |-  0 e. NN0
33 3 relopabiv 
 |-  Rel G
34 33 brrelex1i 
 |-  ( C G 0 -> C e. _V )
35 9 34 syl 
 |-  ( ph -> C e. _V )
36 iftrue 
 |-  ( m = 0 -> if ( m = 0 , C , ( m - 1 ) ) = C )
37 eqid 
 |-  ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) = ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) )
38 36 37 fvmptg 
 |-  ( ( 0 e. NN0 /\ C e. _V ) -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` 0 ) = C )
39 32 35 38 sylancr 
 |-  ( ph -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` 0 ) = C )
40 31 39 syl5eq 
 |-  ( ph -> ( S ` 0 ) = C )
41 40 9 eqbrtrd 
 |-  ( ph -> ( S ` 0 ) G 0 )
42 df-br 
 |-  ( ( S ` k ) G k <-> <. ( S ` k ) , k >. e. G )
43 fveq2 
 |-  ( x = <. ( S ` k ) , k >. -> ( T ` x ) = ( T ` <. ( S ` k ) , k >. ) )
44 df-ov 
 |-  ( ( S ` k ) T k ) = ( T ` <. ( S ` k ) , k >. )
45 43 44 eqtr4di 
 |-  ( x = <. ( S ` k ) , k >. -> ( T ` x ) = ( ( S ` k ) T k ) )
46 fvex 
 |-  ( S ` k ) e. _V
47 vex 
 |-  k e. _V
48 46 47 op2ndd 
 |-  ( x = <. ( S ` k ) , k >. -> ( 2nd ` x ) = k )
49 48 oveq1d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( 2nd ` x ) + 1 ) = ( k + 1 ) )
50 45 49 breq12d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) <-> ( ( S ` k ) T k ) G ( k + 1 ) ) )
51 fveq2 
 |-  ( x = <. ( S ` k ) , k >. -> ( B ` x ) = ( B ` <. ( S ` k ) , k >. ) )
52 df-ov 
 |-  ( ( S ` k ) B k ) = ( B ` <. ( S ` k ) , k >. )
53 51 52 eqtr4di 
 |-  ( x = <. ( S ` k ) , k >. -> ( B ` x ) = ( ( S ` k ) B k ) )
54 45 49 oveq12d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) = ( ( ( S ` k ) T k ) B ( k + 1 ) ) )
55 53 54 ineq12d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) = ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) )
56 55 eleq1d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K <-> ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) )
57 50 56 anbi12d 
 |-  ( x = <. ( S ` k ) , k >. -> ( ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) <-> ( ( ( S ` k ) T k ) G ( k + 1 ) /\ ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) ) )
58 57 rspccv 
 |-  ( A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) -> ( <. ( S ` k ) , k >. e. G -> ( ( ( S ` k ) T k ) G ( k + 1 ) /\ ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) ) )
59 8 58 syl 
 |-  ( ph -> ( <. ( S ` k ) , k >. e. G -> ( ( ( S ` k ) T k ) G ( k + 1 ) /\ ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) ) )
60 42 59 syl5bi 
 |-  ( ph -> ( ( S ` k ) G k -> ( ( ( S ` k ) T k ) G ( k + 1 ) /\ ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) ) )
61 seqp1 
 |-  ( k e. ( ZZ>= ` 0 ) -> ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` ( k + 1 ) ) = ( ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) )
62 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
63 61 62 eleq2s 
 |-  ( k e. NN0 -> ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` ( k + 1 ) ) = ( ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) )
64 10 fveq1i 
 |-  ( S ` ( k + 1 ) ) = ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` ( k + 1 ) )
65 10 fveq1i 
 |-  ( S ` k ) = ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` k )
66 65 oveq1i 
 |-  ( ( S ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) = ( ( seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) )
67 63 64 66 3eqtr4g 
 |-  ( k e. NN0 -> ( S ` ( k + 1 ) ) = ( ( S ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) )
68 eqeq1 
 |-  ( m = ( k + 1 ) -> ( m = 0 <-> ( k + 1 ) = 0 ) )
69 oveq1 
 |-  ( m = ( k + 1 ) -> ( m - 1 ) = ( ( k + 1 ) - 1 ) )
70 68 69 ifbieq2d 
 |-  ( m = ( k + 1 ) -> if ( m = 0 , C , ( m - 1 ) ) = if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) )
71 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
72 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
73 nnne0 
 |-  ( ( k + 1 ) e. NN -> ( k + 1 ) =/= 0 )
74 73 neneqd 
 |-  ( ( k + 1 ) e. NN -> -. ( k + 1 ) = 0 )
75 iffalse 
 |-  ( -. ( k + 1 ) = 0 -> if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) = ( ( k + 1 ) - 1 ) )
76 72 74 75 3syl 
 |-  ( k e. NN0 -> if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) = ( ( k + 1 ) - 1 ) )
77 ovex 
 |-  ( ( k + 1 ) - 1 ) e. _V
78 76 77 eqeltrdi 
 |-  ( k e. NN0 -> if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) e. _V )
79 37 70 71 78 fvmptd3 
 |-  ( k e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) = if ( ( k + 1 ) = 0 , C , ( ( k + 1 ) - 1 ) ) )
80 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
81 ax-1cn 
 |-  1 e. CC
82 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
83 80 81 82 sylancl 
 |-  ( k e. NN0 -> ( ( k + 1 ) - 1 ) = k )
84 79 76 83 3eqtrd 
 |-  ( k e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) = k )
85 84 oveq2d 
 |-  ( k e. NN0 -> ( ( S ` k ) T ( ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ` ( k + 1 ) ) ) = ( ( S ` k ) T k ) )
86 67 85 eqtrd 
 |-  ( k e. NN0 -> ( S ` ( k + 1 ) ) = ( ( S ` k ) T k ) )
87 86 breq1d 
 |-  ( k e. NN0 -> ( ( S ` ( k + 1 ) ) G ( k + 1 ) <-> ( ( S ` k ) T k ) G ( k + 1 ) ) )
88 87 biimprd 
 |-  ( k e. NN0 -> ( ( ( S ` k ) T k ) G ( k + 1 ) -> ( S ` ( k + 1 ) ) G ( k + 1 ) ) )
89 88 adantrd 
 |-  ( k e. NN0 -> ( ( ( ( S ` k ) T k ) G ( k + 1 ) /\ ( ( ( S ` k ) B k ) i^i ( ( ( S ` k ) T k ) B ( k + 1 ) ) ) e. K ) -> ( S ` ( k + 1 ) ) G ( k + 1 ) ) )
90 60 89 syl9r 
 |-  ( k e. NN0 -> ( ph -> ( ( S ` k ) G k -> ( S ` ( k + 1 ) ) G ( k + 1 ) ) ) )
91 90 a2d 
 |-  ( k e. NN0 -> ( ( ph -> ( S ` k ) G k ) -> ( ph -> ( S ` ( k + 1 ) ) G ( k + 1 ) ) ) )
92 14 18 22 26 41 91 nn0ind 
 |-  ( A e. NN0 -> ( ph -> ( S ` A ) G A ) )
93 92 impcom 
 |-  ( ( ph /\ A e. NN0 ) -> ( S ` A ) G A )