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 | ¬ 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
heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
heibor.10 φ C G 0
heibor.11 S = seq 0 T m 0 if m = 0 C m 1
Assertion heiborlem4 φ A 0 S A G A

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 heibor.9 φ x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K
9 heibor.10 φ C G 0
10 heibor.11 S = seq 0 T m 0 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 φ S x G x φ 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 φ S x G x φ 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 φ S x G x φ 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 φ S x G x φ S A G A
27 10 fveq1i S 0 = seq 0 T m 0 if m = 0 C m 1 0
28 0z 0
29 seq1 0 seq 0 T m 0 if m = 0 C m 1 0 = m 0 if m = 0 C m 1 0
30 28 29 ax-mp seq 0 T m 0 if m = 0 C m 1 0 = m 0 if m = 0 C m 1 0
31 27 30 eqtri S 0 = m 0 if m = 0 C m 1 0
32 0nn0 0 0
33 3 relopabiv Rel G
34 33 brrelex1i C G 0 C V
35 9 34 syl φ C V
36 iftrue m = 0 if m = 0 C m 1 = C
37 eqid m 0 if m = 0 C m 1 = m 0 if m = 0 C m 1
38 36 37 fvmptg 0 0 C V m 0 if m = 0 C m 1 0 = C
39 32 35 38 sylancr φ m 0 if m = 0 C m 1 0 = C
40 31 39 syl5eq φ S 0 = C
41 40 9 eqbrtrd φ S 0 G 0
42 df-br S k G k S k k 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 V
47 vex k V
48 46 47 op2ndd x = S k k 2 nd x = k
49 48 oveq1d x = S k k 2 nd x + 1 = k + 1
50 45 49 breq12d x = S k k T x G 2 nd 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 2 nd x + 1 = S k T k B k + 1
55 53 54 ineq12d x = S k k B x T x B 2 nd x + 1 = S k B k S k T k B k + 1
56 55 eleq1d x = S k k B x T x B 2 nd x + 1 K S k B k S k T k B k + 1 K
57 50 56 anbi12d x = S k k T x G 2 nd x + 1 B x T x B 2 nd x + 1 K S k T k G k + 1 S k B k S k T k B k + 1 K
58 57 rspccv x G T x G 2 nd x + 1 B x T x B 2 nd x + 1 K S k k G S k T k G k + 1 S k B k S k T k B k + 1 K
59 8 58 syl φ S k k G S k T k G k + 1 S k B k S k T k B k + 1 K
60 42 59 syl5bi φ S k G k S k T k G k + 1 S k B k S k T k B k + 1 K
61 seqp1 k 0 seq 0 T m 0 if m = 0 C m 1 k + 1 = seq 0 T m 0 if m = 0 C m 1 k T m 0 if m = 0 C m 1 k + 1
62 nn0uz 0 = 0
63 61 62 eleq2s k 0 seq 0 T m 0 if m = 0 C m 1 k + 1 = seq 0 T m 0 if m = 0 C m 1 k T m 0 if m = 0 C m 1 k + 1
64 10 fveq1i S k + 1 = seq 0 T m 0 if m = 0 C m 1 k + 1
65 10 fveq1i S k = seq 0 T m 0 if m = 0 C m 1 k
66 65 oveq1i S k T m 0 if m = 0 C m 1 k + 1 = seq 0 T m 0 if m = 0 C m 1 k T m 0 if m = 0 C m 1 k + 1
67 63 64 66 3eqtr4g k 0 S k + 1 = S k T m 0 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 0 k + 1 0
72 nn0p1nn k 0 k + 1
73 nnne0 k + 1 k + 1 0
74 73 neneqd k + 1 ¬ 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 0 if k + 1 = 0 C k + 1 - 1 = k + 1 - 1
77 ovex k + 1 - 1 V
78 76 77 eqeltrdi k 0 if k + 1 = 0 C k + 1 - 1 V
79 37 70 71 78 fvmptd3 k 0 m 0 if m = 0 C m 1 k + 1 = if k + 1 = 0 C k + 1 - 1
80 nn0cn k 0 k
81 ax-1cn 1
82 pncan k 1 k + 1 - 1 = k
83 80 81 82 sylancl k 0 k + 1 - 1 = k
84 79 76 83 3eqtrd k 0 m 0 if m = 0 C m 1 k + 1 = k
85 84 oveq2d k 0 S k T m 0 if m = 0 C m 1 k + 1 = S k T k
86 67 85 eqtrd k 0 S k + 1 = S k T k
87 86 breq1d k 0 S k + 1 G k + 1 S k T k G k + 1
88 87 biimprd k 0 S k T k G k + 1 S k + 1 G k + 1
89 88 adantrd k 0 S k T k G k + 1 S k B k S k T k B k + 1 K S k + 1 G k + 1
90 60 89 syl9r k 0 φ S k G k S k + 1 G k + 1
91 90 a2d k 0 φ S k G k φ S k + 1 G k + 1
92 14 18 22 26 41 91 nn0ind A 0 φ S A G A
93 92 impcom φ A 0 S A G A