Metamath Proof Explorer

Theorem efgsrel

Description: The start and end of any extension sequence are related (i.e. evaluate to the same element of the quotient group to be created). (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
Assertion efgsrel ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ‘ 0 ) ∼ ( 𝑆 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 1 2 3 4 5 6 efgsdm ⊢ ( 𝐹 ∈ dom 𝑆 ↔ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑎 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑎 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) ) )
8 7 simp1bi ⊢ ( 𝐹 ∈ dom 𝑆 → 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) )
9 eldifsn ⊢ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( 𝐹 ∈ Word 𝑊 ∧ 𝐹 ≠ ∅ ) )
10 lennncl ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
11 9 10 sylbi ⊢ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
12 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
13 8 11 12 3syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
14 nnm1nn0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 )
15 8 11 14 3syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 )
16 eleq1 ⊢ ( 𝑎 = 0 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
17 fveq2 ⊢ ( 𝑎 = 0 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 0 ) )
18 17 breq2d ⊢ ( 𝑎 = 0 → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 0 ) ) )
19 16 18 imbi12d ⊢ ( 𝑎 = 0 → ( ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ↔ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 0 ) ) ) )
20 19 imbi2d ⊢ ( 𝑎 = 0 → ( ( 𝐹 ∈ dom 𝑆 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ) ↔ ( 𝐹 ∈ dom 𝑆 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 0 ) ) ) ) )
21 eleq1 ⊢ ( 𝑎 = 𝑖 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
22 fveq2 ⊢ ( 𝑎 = 𝑖 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑖 ) )
23 22 breq2d ⊢ ( 𝑎 = 𝑖 → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) )
24 21 23 imbi12d ⊢ ( 𝑎 = 𝑖 → ( ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ↔ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) ) )
25 24 imbi2d ⊢ ( 𝑎 = 𝑖 → ( ( 𝐹 ∈ dom 𝑆 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ) ↔ ( 𝐹 ∈ dom 𝑆 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) ) ) )
26 eleq1 ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
27 fveq2 ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
28 27 breq2d ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
29 26 28 imbi12d ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) )
30 29 imbi2d ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( ( 𝐹 ∈ dom 𝑆 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ) ↔ ( 𝐹 ∈ dom 𝑆 → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) ) )
31 eleq1 ⊢ ( 𝑎 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
32 fveq2 ⊢ ( 𝑎 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
33 32 breq2d ⊢ ( 𝑎 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
34 31 33 imbi12d ⊢ ( 𝑎 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
35 34 imbi2d ⊢ ( 𝑎 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ( 𝐹 ∈ dom 𝑆 → ( 𝑎 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑎 ) ) ) ↔ ( 𝐹 ∈ dom 𝑆 → ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) )
36 1 2 efger ⊢ ∼ Er 𝑊
37 36 a1i ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ∼ Er 𝑊 )
38 eldifi ⊢ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) → 𝐹 ∈ Word 𝑊 )
39 wrdf ⊢ ( 𝐹 ∈ Word 𝑊 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑊 )
40 8 38 39 3syl ⊢ ( 𝐹 ∈ dom 𝑆 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑊 )
41 40 ffvelrnda ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 0 ) ∈ 𝑊 )
42 37 41 erref ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 0 ) )
43 42 ex ⊢ ( 𝐹 ∈ dom 𝑆 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 0 ) ) )
44 elnn0uz ⊢ ( 𝑖 ∈ ℕ0 ↔ 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
45 peano2fzor ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
46 44 45 sylanb ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
47 46 3adant1 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
48 47 3expia ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
49 48 imim1d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) ) )
50 40 3ad2ant1 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑊 )
51 50 47 ffvelrnd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑊 )
52 fvoveq1 ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( 𝐹 ‘ ( 𝑎 − 1 ) ) = ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) )
53 52 fveq2d ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) = ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) )
54 53 rneqd ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) )
55 27 54 eleq12d ⊢ ( 𝑎 = ( 𝑖 + 1 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) ↔ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) ) )
56 7 simp3bi ⊢ ( 𝐹 ∈ dom 𝑆 → ∀ 𝑎 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑎 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ∀ 𝑎 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑎 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑎 − 1 ) ) ) )
58 nn0p1nn ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℕ )
59 58 3ad2ant2 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑖 + 1 ) ∈ ℕ )
60 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
61 59 60 eleqtrdi ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
62 elfzolt2b ⊢ ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑖 + 1 ) ∈ ( ( 𝑖 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) )
63 62 3ad2ant3 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑖 + 1 ) ∈ ( ( 𝑖 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) )
64 elfzo3 ⊢ ( ( 𝑖 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑖 + 1 ) ∈ ( ( 𝑖 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) ) )
65 61 63 64 sylanbrc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑖 + 1 ) ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
66 55 57 65 rspcdva ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑖 + 1 ) ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) )
67 nn0cn ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℂ )
68 67 3ad2ant2 ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑖 ∈ ℂ )
69 ax-1cn ⊢ 1 ∈ ℂ
70 pncan ⊢ ( ( 𝑖 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑖 + 1 ) − 1 ) = 𝑖 )
71 68 69 70 sylancl ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 1 ) − 1 ) = 𝑖 )
72 71 fveq2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) = ( 𝐹 ‘ 𝑖 ) )
73 72 fveq2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) = ( 𝑇 ‘ ( 𝐹 ‘ 𝑖 ) ) )
74 73 rneqd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ran ( 𝑇 ‘ ( 𝐹 ‘ ( ( 𝑖 + 1 ) − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝐹 ‘ 𝑖 ) ) )
75 66 74 eleqtrd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑖 + 1 ) ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ 𝑖 ) ) )
76 1 2 3 4 efgi2 ⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ 𝑊 ∧ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
77 51 75 76 syl2anc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
78 36 a1i ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ∼ Er 𝑊 )
79 78 ertr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ∧ ( 𝐹 ‘ 𝑖 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
80 77 79 mpan2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) )
81 80 3expia ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) )
82 81 a2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ) → ( ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) )
83 49 82 syld ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) )
84 83 expcom ⊢ ( 𝑖 ∈ ℕ0 → ( 𝐹 ∈ dom 𝑆 → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) ) )
85 84 a2d ⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝐹 ∈ dom 𝑆 → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ 𝑖 ) ) ) → ( 𝐹 ∈ dom 𝑆 → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( 𝑖 + 1 ) ) ) ) ) )
86 20 25 30 35 43 85 nn0ind ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → ( 𝐹 ∈ dom 𝑆 → ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
87 15 86 mpcom ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
88 13 87 mpd ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ‘ 0 ) ∼ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
89 1 2 3 4 5 6 efgsval ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝑆 ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
90 88 89 breqtrrd ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ‘ 0 ) ∼ ( 𝑆 ‘ 𝐹 ) )