Metamath Proof Explorer

Theorem efgsp1

Description: If F is an extension sequence and A is an extension of the last element of F , then F + <" A "> is an extension sequence. (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 efgsp1 ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ dom 𝑆 )

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 8 eldifad ⊢ ( 𝐹 ∈ dom 𝑆 → 𝐹 ∈ Word 𝑊 )
10 1 2 3 4 5 6 efgsf ⊢ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊
11 10 fdmi ⊢ dom 𝑆 = { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) }
12 11 feq2i ⊢ ( 𝑆 : dom 𝑆 ⟶ 𝑊 ↔ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊 )
13 10 12 mpbir ⊢ 𝑆 : dom 𝑆 ⟶ 𝑊
14 13 ffvelcdmi ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝑆 ‘ 𝐹 ) ∈ 𝑊 )
15 1 2 3 4 efgtf ⊢ ( ( 𝑆 ‘ 𝐹 ) ∈ 𝑊 → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 ‘ 𝐹 ) ) ) , 𝑖 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝑆 ‘ 𝐹 ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑖 ( 𝑀 ‘ 𝑖 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑆 ‘ 𝐹 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
16 14 15 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( 𝑆 ‘ 𝐹 ) ) ) , 𝑖 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝑆 ‘ 𝐹 ) splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑖 ( 𝑀 ‘ 𝑖 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑆 ‘ 𝐹 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
17 16 simprd ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑆 ‘ 𝐹 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
18 17 frnd ⊢ ( 𝐹 ∈ dom 𝑆 → ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ⊆ 𝑊 )
19 18 sselda ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → 𝐴 ∈ 𝑊 )
20 19 s1cld ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 )
21 ccatcl ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ Word 𝑊 )
22 9 20 21 syl2an2r ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ Word 𝑊 )
23 ccatws1n0 ⊢ ( 𝐹 ∈ Word 𝑊 → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ≠ ∅ )
24 9 23 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ≠ ∅ )
25 24 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ≠ ∅ )
26 eldifsn ⊢ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ Word 𝑊 ∧ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ≠ ∅ ) )
27 22 25 26 sylanbrc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ ( Word 𝑊 ∖ { ∅ } ) )
28 9 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → 𝐹 ∈ Word 𝑊 )
29 eldifsni ⊢ ( 𝐹 ∈ ( Word 𝑊 ∖ { ∅ } ) → 𝐹 ≠ ∅ )
30 8 29 syl ⊢ ( 𝐹 ∈ dom 𝑆 → 𝐹 ≠ ∅ )
31 len0nnbi ⊢ ( 𝐹 ∈ Word 𝑊 → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
32 9 31 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
33 30 32 mpbid ⊢ ( 𝐹 ∈ dom 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ )
34 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ )
35 33 34 sylibr ⊢ ( 𝐹 ∈ dom 𝑆 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
36 35 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
37 ccatval1 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
38 28 20 36 37 syl3anc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
39 7 simp2bi ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝐹 ‘ 0 ) ∈ 𝐷 )
40 39 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 0 ) ∈ 𝐷 )
41 38 40 eqeltrd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) ∈ 𝐷 )
42 7 simp3bi ⊢ ( 𝐹 ∈ dom 𝑆 → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) )
43 42 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) )
44 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
45 44 sseli ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
46 ccatval1 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
47 45 46 syl3an3 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
48 elfzoel2 ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
49 peano2zm ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ )
50 48 49 syl ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ )
51 48 zred ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℝ )
52 51 lem1d ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ≤ ( ♯ ‘ 𝐹 ) )
53 eluz2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ≤ ( ♯ ‘ 𝐹 ) ) )
54 50 48 52 53 syl3anbrc ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
55 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
56 54 55 syl ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
57 elfzo1elm1fzo0 ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
58 56 57 sseldd ⊢ ( 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑖 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
59 ccatval1 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ ( 𝑖 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) = ( 𝐹 ‘ ( 𝑖 − 1 ) ) )
60 58 59 syl3an3 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) = ( 𝐹 ‘ ( 𝑖 − 1 ) ) )
61 60 fveq2d ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) = ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) )
62 61 rneqd ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) )
63 47 62 eleq12d ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) )
64 63 3expa ⊢ ( ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ) ∧ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) )
65 64 ralbidva ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ) → ( ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) )
66 9 20 65 syl2an2r ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐹 ‘ ( 𝑖 − 1 ) ) ) ) )
67 43 66 mpbird ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) )
68 lencl ⊢ ( 𝐹 ∈ Word 𝑊 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
69 9 68 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
70 69 nn0cnd ⊢ ( 𝐹 ∈ dom 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
71 70 addlidd ⊢ ( 𝐹 ∈ dom 𝑆 → ( 0 + ( ♯ ‘ 𝐹 ) ) = ( ♯ ‘ 𝐹 ) )
72 71 fveq2d ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) )
73 72 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) )
74 s1len ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) = 1
75 1nn ⊢ 1 ∈ ℕ
76 74 75 eqeltri ⊢ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ∈ ℕ
77 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ↔ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ∈ ℕ )
78 76 77 mpbir ⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) )
79 78 a1i ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) )
80 ccatval3 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐹 ) ) ) = ( ⟨“ 𝐴 ”⟩ ‘ 0 ) )
81 28 20 79 80 syl3anc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐹 ) ) ) = ( ⟨“ 𝐴 ”⟩ ‘ 0 ) )
82 73 81 eqtr3d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) = ( ⟨“ 𝐴 ”⟩ ‘ 0 ) )
83 simpr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) )
84 s1fv ⊢ ( 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴 )
85 84 adantl ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) = 𝐴 )
86 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
87 33 86 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
88 87 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
89 ccatval1 ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
90 28 20 88 89 syl3anc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
91 1 2 3 4 5 6 efgsval ⊢ ( 𝐹 ∈ dom 𝑆 → ( 𝑆 ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
92 91 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝑆 ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
93 90 92 eqtr4d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝑆 ‘ 𝐹 ) )
94 93 fveq2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) )
95 94 rneqd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) )
96 83 85 95 3eltr4d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ⟨“ 𝐴 ”⟩ ‘ 0 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
97 82 96 eqeltrd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
98 fvex ⊢ ( ♯ ‘ 𝐹 ) ∈ V
99 fveq2 ⊢ ( 𝑖 = ( ♯ ‘ 𝐹 ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) = ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) )
100 fvoveq1 ⊢ ( 𝑖 = ( ♯ ‘ 𝐹 ) → ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) = ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
101 100 fveq2d ⊢ ( 𝑖 = ( ♯ ‘ 𝐹 ) → ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) = ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
102 101 rneqd ⊢ ( 𝑖 = ( ♯ ‘ 𝐹 ) → ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) = ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
103 99 102 eleq12d ⊢ ( 𝑖 = ( ♯ ‘ 𝐹 ) → ( ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
104 98 103 ralsn ⊢ ( ∀ 𝑖 ∈ { ( ♯ ‘ 𝐹 ) } ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ♯ ‘ 𝐹 ) ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
105 97 104 sylibr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ∀ 𝑖 ∈ { ( ♯ ‘ 𝐹 ) } ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) )
106 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ∧ ∀ 𝑖 ∈ { ( ♯ ‘ 𝐹 ) } ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ) )
107 67 105 106 sylanbrc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ∀ 𝑖 ∈ ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) )
108 ccatlen ⊢ ( ( 𝐹 ∈ Word 𝑊 ∧ ⟨“ 𝐴 ”⟩ ∈ Word 𝑊 ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) )
109 9 20 108 syl2an2r ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) )
110 74 oveq2i ⊢ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐴 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 )
111 109 110 eqtrdi ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
112 111 oveq2d ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) ) = ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
113 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
114 33 113 eleqtrdi ⊢ ( 𝐹 ∈ dom 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
115 fzosplitsn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) → ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
116 114 115 syl ⊢ ( 𝐹 ∈ dom 𝑆 → ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
117 116 adantr ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
118 112 117 eqtrd ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) ) = ( ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∪ { ( ♯ ‘ 𝐹 ) } ) )
119 107 118 raleqtrrdv ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) )
120 1 2 3 4 5 6 efgsdm ⊢ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ dom 𝑆 ↔ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ) ) ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ‘ ( 𝑖 − 1 ) ) ) ) )
121 27 41 119 120 syl3anbrc ⊢ ( ( 𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐹 ) ) ) → ( 𝐹 ++ ⟨“ 𝐴 ”⟩ ) ∈ dom 𝑆 )