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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
heibor.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
heibor.10 ⊢ ( 𝜑 → 𝐶 𝐺 0 )
heibor.11 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
Assertion heiborlem4 ( ( 𝜑 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑆 ‘ 𝐴 ) 𝐺 𝐴 )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3 heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4 heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5 heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6 heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7 heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8 heibor.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9 heibor.10 ⊢ ( 𝜑 → 𝐶 𝐺 0 )
10 heibor.11 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 0 ) )
12 id ⊢ ( 𝑥 = 0 → 𝑥 = 0 )
13 11 12 breq12d ⊢ ( 𝑥 = 0 → ( ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ↔ ( 𝑆 ‘ 0 ) 𝐺 0 ) )
14 13 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ) ↔ ( 𝜑 → ( 𝑆 ‘ 0 ) 𝐺 0 ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑘 ) )
16 id ⊢ ( 𝑥 = 𝑘 → 𝑥 = 𝑘 )
17 15 16 breq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ↔ ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ) )
18 17 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ) ↔ ( 𝜑 → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ) ) )
19 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑘 + 1 ) ) )
20 id ⊢ ( 𝑥 = ( 𝑘 + 1 ) → 𝑥 = ( 𝑘 + 1 ) )
21 19 20 breq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ↔ ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) )
22 21 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ) ↔ ( 𝜑 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐴 ) )
24 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
25 23 24 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ↔ ( 𝑆 ‘ 𝐴 ) 𝐺 𝐴 ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → ( 𝑆 ‘ 𝑥 ) 𝐺 𝑥 ) ↔ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) 𝐺 𝐴 ) ) )
27 10 fveq1i ⊢ ( 𝑆 ‘ 0 ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 0 )
28 0z ⊢ 0 ∈ ℤ
29 seq1 ⊢ ( 0 ∈ ℤ → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 0 ) = ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ 0 ) )
30 28 29 ax-mp ⊢ ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 0 ) = ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ 0 )
31 27 30 eqtri ⊢ ( 𝑆 ‘ 0 ) = ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ 0 )
32 0nn0 ⊢ 0 ∈ ℕ0
33 3 relopabi ⊢ Rel 𝐺
34 33 brrelex1i ⊢ ( 𝐶 𝐺 0 → 𝐶 ∈ V )
35 9 34 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
36 iftrue ⊢ ( 𝑚 = 0 → if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) = 𝐶 )
37 eqid ⊢ ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) )
38 36 37 fvmptg ⊢ ( ( 0 ∈ ℕ0 ∧ 𝐶 ∈ V ) → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ 0 ) = 𝐶 )
39 32 35 38 sylancr ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ 0 ) = 𝐶 )
40 31 39 syl5eq ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝐶 )
41 40 9 eqbrtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) 𝐺 0 )
42 df-br ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 )
43 fveq2 ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ) )
44 df-ov ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) = ( 𝑇 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ )
45 43 44 eqtr4di ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝑇 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
46 fvex ⊢ ( 𝑆 ‘ 𝑘 ) ∈ V
47 vex ⊢ 𝑘 ∈ V
48 46 47 op2ndd ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑘 )
49 48 oveq1d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 2nd ‘ 𝑥 ) + 1 ) = ( 𝑘 + 1 ) )
50 45 49 breq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ↔ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ) )
51 fveq2 ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ) )
52 df-ov ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( 𝐵 ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ )
53 51 52 eqtr4di ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( 𝐵 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) )
54 45 49 oveq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) )
55 53 54 ineq12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) )
56 55 eleq1d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) )
57 50 56 anbi12d ⊢ ( 𝑥 = ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ → ( ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
58 57 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ( ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
59 8 58 syl ⊢ ( 𝜑 → ( ⟨ ( 𝑆 ‘ 𝑘 ) , 𝑘 ⟩ ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
60 42 59 syl5bi ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) )
61 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
62 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
63 61 62 eleq2s ⊢ ( 𝑘 ∈ ℕ0 → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
64 10 fveq1i ⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) )
65 10 fveq1i ⊢ ( 𝑆 ‘ 𝑘 ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 )
66 65 oveq1i ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) )
67 63 64 66 3eqtr4g ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
68 eqeq1 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 = 0 ↔ ( 𝑘 + 1 ) = 0 ) )
69 oveq1 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
70 68 69 ifbieq2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) )
71 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
72 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
73 nnne0 ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑘 + 1 ) ≠ 0 )
74 73 neneqd ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ¬ ( 𝑘 + 1 ) = 0 )
75 iffalse ⊢ ( ¬ ( 𝑘 + 1 ) = 0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑘 + 1 ) − 1 ) )
76 72 74 75 3syl ⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑘 + 1 ) − 1 ) )
77 ovex ⊢ ( ( 𝑘 + 1 ) − 1 ) ∈ V
78 76 77 eqeltrdi ⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) ∈ V )
79 37 70 71 78 fvmptd3 ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) )
80 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
81 ax-1cn ⊢ 1 ∈ ℂ
82 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
83 80 81 82 sylancl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
84 79 76 83 3eqtrd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = 𝑘 )
85 84 oveq2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
86 67 85 eqtrd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) )
87 86 breq1d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ↔ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ) )
88 87 biimprd ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) )
89 88 adantrd ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) )
90 60 89 syl9r ⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) ) )
91 90 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝜑 → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ) → ( 𝜑 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) ) )
92 14 18 22 26 41 91 nn0ind ⊢ ( 𝐴 ∈ ℕ0 → ( 𝜑 → ( 𝑆 ‘ 𝐴 ) 𝐺 𝐴 ) )
93 92 impcom ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ0 ) → ( 𝑆 ‘ 𝐴 ) 𝐺 𝐴 )