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 relopabiv 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 ) → ( 𝑆𝐴 ) 𝐺 𝐴 )