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 eqtrid ⊢ φ → 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 biimtrid ⊢ φ → 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