# 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}=\mathrm{MetOpen}\left({D}\right)$
heibor.3 ${⊢}{K}=\left\{{u}|¬\exists {v}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}\subseteq \bigcup {v}\right\}$
heibor.4 ${⊢}{G}=\left\{⟨{y},{n}⟩|\left({n}\in {ℕ}_{0}\wedge {y}\in {F}\left({n}\right)\wedge {y}{B}{n}\in {K}\right)\right\}$
heibor.5 ${⊢}{B}=\left({z}\in {X},{m}\in {ℕ}_{0}⟼{z}\mathrm{ball}\left({D}\right)\left(\frac{1}{{2}^{{m}}}\right)\right)$
heibor.6 ${⊢}{\phi }\to {D}\in \mathrm{CMet}\left({X}\right)$
heibor.7 ${⊢}{\phi }\to {F}:{ℕ}_{0}⟶𝒫{X}\cap \mathrm{Fin}$
heibor.8 ${⊢}{\phi }\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{X}=\bigcup _{{y}\in {F}\left({n}\right)}\left({y}{B}{n}\right)$
heibor.9 ${⊢}{\phi }\to \forall {x}\in {G}\phantom{\rule{.4em}{0ex}}\left({T}\left({x}\right){G}\left({2}^{nd}\left({x}\right)+1\right)\wedge {B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)\in {K}\right)$
heibor.10 ${⊢}{\phi }\to {C}{G}0$
heibor.11 ${⊢}{S}=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)$
Assertion heiborlem4 ${⊢}\left({\phi }\wedge {A}\in {ℕ}_{0}\right)\to {S}\left({A}\right){G}{A}$

### Proof

Step Hyp Ref Expression
1 heibor.1 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 heibor.3 ${⊢}{K}=\left\{{u}|¬\exists {v}\in \left(𝒫{U}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{u}\subseteq \bigcup {v}\right\}$
3 heibor.4 ${⊢}{G}=\left\{⟨{y},{n}⟩|\left({n}\in {ℕ}_{0}\wedge {y}\in {F}\left({n}\right)\wedge {y}{B}{n}\in {K}\right)\right\}$
4 heibor.5 ${⊢}{B}=\left({z}\in {X},{m}\in {ℕ}_{0}⟼{z}\mathrm{ball}\left({D}\right)\left(\frac{1}{{2}^{{m}}}\right)\right)$
5 heibor.6 ${⊢}{\phi }\to {D}\in \mathrm{CMet}\left({X}\right)$
6 heibor.7 ${⊢}{\phi }\to {F}:{ℕ}_{0}⟶𝒫{X}\cap \mathrm{Fin}$
7 heibor.8 ${⊢}{\phi }\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{X}=\bigcup _{{y}\in {F}\left({n}\right)}\left({y}{B}{n}\right)$
8 heibor.9 ${⊢}{\phi }\to \forall {x}\in {G}\phantom{\rule{.4em}{0ex}}\left({T}\left({x}\right){G}\left({2}^{nd}\left({x}\right)+1\right)\wedge {B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)\in {K}\right)$
9 heibor.10 ${⊢}{\phi }\to {C}{G}0$
10 heibor.11 ${⊢}{S}=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)$
11 fveq2 ${⊢}{x}=0\to {S}\left({x}\right)={S}\left(0\right)$
12 id ${⊢}{x}=0\to {x}=0$
13 11 12 breq12d ${⊢}{x}=0\to \left({S}\left({x}\right){G}{x}↔{S}\left(0\right){G}0\right)$
14 13 imbi2d ${⊢}{x}=0\to \left(\left({\phi }\to {S}\left({x}\right){G}{x}\right)↔\left({\phi }\to {S}\left(0\right){G}0\right)\right)$
15 fveq2 ${⊢}{x}={k}\to {S}\left({x}\right)={S}\left({k}\right)$
16 id ${⊢}{x}={k}\to {x}={k}$
17 15 16 breq12d ${⊢}{x}={k}\to \left({S}\left({x}\right){G}{x}↔{S}\left({k}\right){G}{k}\right)$
18 17 imbi2d ${⊢}{x}={k}\to \left(\left({\phi }\to {S}\left({x}\right){G}{x}\right)↔\left({\phi }\to {S}\left({k}\right){G}{k}\right)\right)$
19 fveq2 ${⊢}{x}={k}+1\to {S}\left({x}\right)={S}\left({k}+1\right)$
20 id ${⊢}{x}={k}+1\to {x}={k}+1$
21 19 20 breq12d ${⊢}{x}={k}+1\to \left({S}\left({x}\right){G}{x}↔{S}\left({k}+1\right){G}\left({k}+1\right)\right)$
22 21 imbi2d ${⊢}{x}={k}+1\to \left(\left({\phi }\to {S}\left({x}\right){G}{x}\right)↔\left({\phi }\to {S}\left({k}+1\right){G}\left({k}+1\right)\right)\right)$
23 fveq2 ${⊢}{x}={A}\to {S}\left({x}\right)={S}\left({A}\right)$
24 id ${⊢}{x}={A}\to {x}={A}$
25 23 24 breq12d ${⊢}{x}={A}\to \left({S}\left({x}\right){G}{x}↔{S}\left({A}\right){G}{A}\right)$
26 25 imbi2d ${⊢}{x}={A}\to \left(\left({\phi }\to {S}\left({x}\right){G}{x}\right)↔\left({\phi }\to {S}\left({A}\right){G}{A}\right)\right)$
27 10 fveq1i ${⊢}{S}\left(0\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left(0\right)$
28 0z ${⊢}0\in ℤ$
29 seq1 ${⊢}0\in ℤ\to seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left(0\right)=\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left(0\right)$
30 28 29 ax-mp ${⊢}seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left(0\right)=\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left(0\right)$
31 27 30 eqtri ${⊢}{S}\left(0\right)=\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left(0\right)$
32 0nn0 ${⊢}0\in {ℕ}_{0}$
33 3 relopabi ${⊢}\mathrm{Rel}{G}$
34 33 brrelex1i ${⊢}{C}{G}0\to {C}\in \mathrm{V}$
35 9 34 syl ${⊢}{\phi }\to {C}\in \mathrm{V}$
36 iftrue ${⊢}{m}=0\to if\left({m}=0,{C},{m}-1\right)={C}$
37 eqid ${⊢}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)=\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)$
38 36 37 fvmptg ${⊢}\left(0\in {ℕ}_{0}\wedge {C}\in \mathrm{V}\right)\to \left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left(0\right)={C}$
39 32 35 38 sylancr ${⊢}{\phi }\to \left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left(0\right)={C}$
40 31 39 syl5eq ${⊢}{\phi }\to {S}\left(0\right)={C}$
41 40 9 eqbrtrd ${⊢}{\phi }\to {S}\left(0\right){G}0$
42 df-br ${⊢}{S}\left({k}\right){G}{k}↔⟨{S}\left({k}\right),{k}⟩\in {G}$
43 fveq2 ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {T}\left({x}\right)={T}\left(⟨{S}\left({k}\right),{k}⟩\right)$
44 df-ov ${⊢}{S}\left({k}\right){T}{k}={T}\left(⟨{S}\left({k}\right),{k}⟩\right)$
45 43 44 syl6eqr ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {T}\left({x}\right)={S}\left({k}\right){T}{k}$
46 fvex ${⊢}{S}\left({k}\right)\in \mathrm{V}$
47 vex ${⊢}{k}\in \mathrm{V}$
48 46 47 op2ndd ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {2}^{nd}\left({x}\right)={k}$
49 48 oveq1d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {2}^{nd}\left({x}\right)+1={k}+1$
50 45 49 breq12d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to \left({T}\left({x}\right){G}\left({2}^{nd}\left({x}\right)+1\right)↔\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\right)$
51 fveq2 ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {B}\left({x}\right)={B}\left(⟨{S}\left({k}\right),{k}⟩\right)$
52 df-ov ${⊢}{S}\left({k}\right){B}{k}={B}\left(⟨{S}\left({k}\right),{k}⟩\right)$
53 51 52 syl6eqr ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {B}\left({x}\right)={S}\left({k}\right){B}{k}$
54 45 49 oveq12d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)=\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)$
55 53 54 ineq12d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to {B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)=\left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)$
56 55 eleq1d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to \left({B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)\in {K}↔\left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)$
57 50 56 anbi12d ${⊢}{x}=⟨{S}\left({k}\right),{k}⟩\to \left(\left({T}\left({x}\right){G}\left({2}^{nd}\left({x}\right)+1\right)\wedge {B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)\in {K}\right)↔\left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\wedge \left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)\right)$
58 57 rspccv ${⊢}\forall {x}\in {G}\phantom{\rule{.4em}{0ex}}\left({T}\left({x}\right){G}\left({2}^{nd}\left({x}\right)+1\right)\wedge {B}\left({x}\right)\cap \left({T}\left({x}\right){B}\left({2}^{nd}\left({x}\right)+1\right)\right)\in {K}\right)\to \left(⟨{S}\left({k}\right),{k}⟩\in {G}\to \left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\wedge \left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)\right)$
59 8 58 syl ${⊢}{\phi }\to \left(⟨{S}\left({k}\right),{k}⟩\in {G}\to \left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\wedge \left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)\right)$
60 42 59 syl5bi ${⊢}{\phi }\to \left({S}\left({k}\right){G}{k}\to \left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\wedge \left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)\right)$
61 seqp1 ${⊢}{k}\in {ℤ}_{\ge 0}\to seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}+1\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)$
62 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
63 61 62 eleq2s ${⊢}{k}\in {ℕ}_{0}\to seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}+1\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)$
64 10 fveq1i ${⊢}{S}\left({k}+1\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}+1\right)$
65 10 fveq1i ${⊢}{S}\left({k}\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}\right)$
66 65 oveq1i ${⊢}{S}\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)=seq0\left({T},\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\right)\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)$
67 63 64 66 3eqtr4g ${⊢}{k}\in {ℕ}_{0}\to {S}\left({k}+1\right)={S}\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)$
68 eqeq1 ${⊢}{m}={k}+1\to \left({m}=0↔{k}+1=0\right)$
69 oveq1 ${⊢}{m}={k}+1\to {m}-1={k}+1-1$
70 68 69 ifbieq2d ${⊢}{m}={k}+1\to if\left({m}=0,{C},{m}-1\right)=if\left({k}+1=0,{C},{k}+1-1\right)$
71 peano2nn0 ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in {ℕ}_{0}$
72 nn0p1nn ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in ℕ$
73 nnne0 ${⊢}{k}+1\in ℕ\to {k}+1\ne 0$
74 73 neneqd ${⊢}{k}+1\in ℕ\to ¬{k}+1=0$
75 iffalse ${⊢}¬{k}+1=0\to if\left({k}+1=0,{C},{k}+1-1\right)={k}+1-1$
76 72 74 75 3syl ${⊢}{k}\in {ℕ}_{0}\to if\left({k}+1=0,{C},{k}+1-1\right)={k}+1-1$
77 ovex ${⊢}{k}+1-1\in \mathrm{V}$
78 76 77 syl6eqel ${⊢}{k}\in {ℕ}_{0}\to if\left({k}+1=0,{C},{k}+1-1\right)\in \mathrm{V}$
79 37 70 71 78 fvmptd3 ${⊢}{k}\in {ℕ}_{0}\to \left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)=if\left({k}+1=0,{C},{k}+1-1\right)$
80 nn0cn ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℂ$
81 ax-1cn ${⊢}1\in ℂ$
82 pncan ${⊢}\left({k}\in ℂ\wedge 1\in ℂ\right)\to {k}+1-1={k}$
83 80 81 82 sylancl ${⊢}{k}\in {ℕ}_{0}\to {k}+1-1={k}$
84 79 76 83 3eqtrd ${⊢}{k}\in {ℕ}_{0}\to \left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)={k}$
85 84 oveq2d ${⊢}{k}\in {ℕ}_{0}\to {S}\left({k}\right){T}\left({m}\in {ℕ}_{0}⟼if\left({m}=0,{C},{m}-1\right)\right)\left({k}+1\right)={S}\left({k}\right){T}{k}$
86 67 85 eqtrd ${⊢}{k}\in {ℕ}_{0}\to {S}\left({k}+1\right)={S}\left({k}\right){T}{k}$
87 86 breq1d ${⊢}{k}\in {ℕ}_{0}\to \left({S}\left({k}+1\right){G}\left({k}+1\right)↔\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\right)$
88 87 biimprd ${⊢}{k}\in {ℕ}_{0}\to \left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\to {S}\left({k}+1\right){G}\left({k}+1\right)\right)$
89 88 adantrd ${⊢}{k}\in {ℕ}_{0}\to \left(\left(\left({S}\left({k}\right){T}{k}\right){G}\left({k}+1\right)\wedge \left({S}\left({k}\right){B}{k}\right)\cap \left(\left({S}\left({k}\right){T}{k}\right){B}\left({k}+1\right)\right)\in {K}\right)\to {S}\left({k}+1\right){G}\left({k}+1\right)\right)$
90 60 89 syl9r ${⊢}{k}\in {ℕ}_{0}\to \left({\phi }\to \left({S}\left({k}\right){G}{k}\to {S}\left({k}+1\right){G}\left({k}+1\right)\right)\right)$
91 90 a2d ${⊢}{k}\in {ℕ}_{0}\to \left(\left({\phi }\to {S}\left({k}\right){G}{k}\right)\to \left({\phi }\to {S}\left({k}+1\right){G}\left({k}+1\right)\right)\right)$
92 14 18 22 26 41 91 nn0ind ${⊢}{A}\in {ℕ}_{0}\to \left({\phi }\to {S}\left({A}\right){G}{A}\right)$
93 92 impcom ${⊢}\left({\phi }\wedge {A}\in {ℕ}_{0}\right)\to {S}\left({A}\right){G}{A}$