MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgsp1 Structured version   Visualization version   GIF version

Theorem efgsp1 18350
Description: If 𝐹 is an extension sequence and 𝐴 is an extension of the last element of 𝐹, then 𝐹 + ⟨“𝐴”⟩ is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
efgred.d 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
efgred.s 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
Assertion
Ref Expression
efgsp1 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Distinct variable groups:   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥   𝑚,𝑀   𝑥,𝑛,𝑀,𝑡,𝑣,𝑤   𝑘,𝑚,𝑡,𝑥,𝑇   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑚,𝑡,𝑥,𝑦,𝑧   𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑚,𝑡
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐼(𝑘)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgsp1
Dummy variables 𝑎 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . 8 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 efgval.r . . . . . . . 8 = ( ~FG𝐼)
3 efgval2.m . . . . . . . 8 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
4 efgval2.t . . . . . . . 8 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
5 efgred.d . . . . . . . 8 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
6 efgred.s . . . . . . . 8 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
71, 2, 3, 4, 5, 6efgsdm 18343 . . . . . . 7 (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
87simp1bi 1139 . . . . . 6 (𝐹 ∈ dom 𝑆𝐹 ∈ (Word 𝑊 ∖ {∅}))
98adantr 466 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ (Word 𝑊 ∖ {∅}))
109eldifad 3735 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ Word 𝑊)
111, 2, 3, 4, 5, 6efgsf 18342 . . . . . . . . . . . 12 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
1211fdmi 6190 . . . . . . . . . . . . 13 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
1312feq2i 6175 . . . . . . . . . . . 12 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
1411, 13mpbir 221 . . . . . . . . . . 11 𝑆:dom 𝑆𝑊
1514ffvelrni 6499 . . . . . . . . . 10 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) ∈ 𝑊)
1615adantr 466 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) ∈ 𝑊)
171, 2, 3, 4efgtf 18335 . . . . . . . . 9 ((𝑆𝐹) ∈ 𝑊 → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1816, 17syl 17 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1918simprd 483 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊)
20 frn 6191 . . . . . . 7 ((𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊 → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
2119, 20syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
22 simpr 471 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴 ∈ ran (𝑇‘(𝑆𝐹)))
2321, 22sseldd 3753 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴𝑊)
2423s1cld 13576 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ⟨“𝐴”⟩ ∈ Word 𝑊)
25 ccatcl 13549 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
2610, 24, 25syl2anc 573 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
27 ccatlen 13550 . . . . . . 7 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
2810, 24, 27syl2anc 573 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
29 s1len 13579 . . . . . . 7 (♯‘⟨“𝐴”⟩) = 1
3029oveq2i 6802 . . . . . 6 ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)) = ((♯‘𝐹) + 1)
3128, 30syl6eq 2821 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + 1))
32 lencl 13513 . . . . . 6 (𝐹 ∈ Word 𝑊 → (♯‘𝐹) ∈ ℕ0)
33 nn0p1nn 11532 . . . . . 6 ((♯‘𝐹) ∈ ℕ0 → ((♯‘𝐹) + 1) ∈ ℕ)
3410, 32, 333syl 18 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) + 1) ∈ ℕ)
3531, 34eqeltrd 2850 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ)
36 wrdfin 13512 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 → (𝐹 ++ ⟨“𝐴”⟩) ∈ Fin)
37 hashnncl 13352 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Fin → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3826, 36, 373syl 18 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3935, 38mpbid 222 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅)
40 eldifsn 4453 . . 3 ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 ∧ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
4126, 39, 40sylanbrc 572 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}))
42 eldifsni 4457 . . . . . . 7 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ≠ ∅)
439, 42syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ≠ ∅)
44 wrdfin 13512 . . . . . . 7 (𝐹 ∈ Word 𝑊𝐹 ∈ Fin)
45 hashnncl 13352 . . . . . . 7 (𝐹 ∈ Fin → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4610, 44, 453syl 18 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4743, 46mpbird 247 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ)
48 lbfzo0 12709 . . . . 5 (0 ∈ (0..^(♯‘𝐹)) ↔ (♯‘𝐹) ∈ ℕ)
4947, 48sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘𝐹)))
50 ccatval1 13552 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
5110, 24, 49, 50syl3anc 1476 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
527simp2bi 1140 . . . 4 (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷)
5352adantr 466 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹‘0) ∈ 𝐷)
5451, 53eqeltrd 2850 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷)
557simp3bi 1141 . . . . . 6 (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
5655adantr 466 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
57 fzo0ss1 12699 . . . . . . . . . . 11 (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))
5857sseli 3748 . . . . . . . . . 10 (𝑖 ∈ (1..^(♯‘𝐹)) → 𝑖 ∈ (0..^(♯‘𝐹)))
59 ccatval1 13552 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
6058, 59syl3an3 1169 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
61 elfzoel2 12670 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
62 peano2zm 11620 . . . . . . . . . . . . . . . 16 ((♯‘𝐹) ∈ ℤ → ((♯‘𝐹) − 1) ∈ ℤ)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ∈ ℤ)
6461zred 11682 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6564lem1d 11157 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ≤ (♯‘𝐹))
66 eluz2 11892 . . . . . . . . . . . . . . 15 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) ↔ (((♯‘𝐹) − 1) ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ ∧ ((♯‘𝐹) − 1) ≤ (♯‘𝐹)))
6763, 61, 65, 66syl3anbrc 1428 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)))
68 fzoss2 12697 . . . . . . . . . . . . . 14 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
6967, 68syl 17 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(♯‘𝐹)) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
70 elfzoelz 12671 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → 𝑖 ∈ ℤ)
71 elfzom1b 12768 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) → (𝑖 ∈ (1..^(♯‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1))))
7270, 61, 71syl2anc 573 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 ∈ (1..^(♯‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1))))
7372ibi 256 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1)))
7469, 73sseldd 3753 . . . . . . . . . . . 12 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^(♯‘𝐹)))
75 ccatval1 13552 . . . . . . . . . . . 12 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ (𝑖 − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7674, 75syl3an3 1169 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7776fveq2d 6334 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1))))
7877rneqd 5489 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1))))
7960, 78eleq12d 2844 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
80793expa 1111 . . . . . . 7 (((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) ∧ 𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8180ralbidva 3134 . . . . . 6 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8210, 24, 81syl2anc 573 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8356, 82mpbird 247 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
8410, 32syl 17 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ0)
8584nn0cnd 11553 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℂ)
8685addid2d 10437 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (0 + (♯‘𝐹)) = (♯‘𝐹))
8786fveq2d 6334 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
88 1nn 11231 . . . . . . . . . . 11 1 ∈ ℕ
8929, 88eqeltri 2846 . . . . . . . . . 10 (♯‘⟨“𝐴”⟩) ∈ ℕ
9089a1i 11 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘⟨“𝐴”⟩) ∈ ℕ)
91 lbfzo0 12709 . . . . . . . . 9 (0 ∈ (0..^(♯‘⟨“𝐴”⟩)) ↔ (♯‘⟨“𝐴”⟩) ∈ ℕ)
9290, 91sylibr 224 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘⟨“𝐴”⟩)))
93 ccatval3 13554 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘⟨“𝐴”⟩))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9410, 24, 92, 93syl3anc 1476 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9587, 94eqtr3d 2807 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) = (⟨“𝐴”⟩‘0))
96 s1fv 13583 . . . . . . . 8 (𝐴 ∈ ran (𝑇‘(𝑆𝐹)) → (⟨“𝐴”⟩‘0) = 𝐴)
9796adantl 467 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) = 𝐴)
98 fzo0end 12761 . . . . . . . . . . . 12 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
9947, 98syl 17 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
100 ccatval1 13552 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
10110, 24, 99, 100syl3anc 1476 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
1021, 2, 3, 4, 5, 6efgsval 18344 . . . . . . . . . . 11 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
103102adantr 466 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
104101, 103eqtr4d 2808 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝑆𝐹))
105104fveq2d 6334 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = (𝑇‘(𝑆𝐹)))
106105rneqd 5489 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = ran (𝑇‘(𝑆𝐹)))
10722, 97, 1063eltr4d 2865 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
10895, 107eqeltrd 2850 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
109 fvex 6340 . . . . . 6 (♯‘𝐹) ∈ V
110 fveq2 6330 . . . . . . 7 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
111 fvoveq1 6814 . . . . . . . . 9 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))
112111fveq2d 6334 . . . . . . . 8 (𝑖 = (♯‘𝐹) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
113112rneqd 5489 . . . . . . 7 (𝑖 = (♯‘𝐹) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
114110, 113eleq12d 2844 . . . . . 6 (𝑖 = (♯‘𝐹) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))))
115109, 114ralsn 4360 . . . . 5 (∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
116108, 115sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
117 ralunb 3945 . . . 4 (∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ∧ ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
11883, 116, 117sylanbrc 572 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
11931oveq2d 6807 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = (1..^((♯‘𝐹) + 1)))
120 nnuz 11923 . . . . . . 7 ℕ = (ℤ‘1)
12147, 120syl6eleq 2860 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ (ℤ‘1))
122 fzosplitsn 12777 . . . . . 6 ((♯‘𝐹) ∈ (ℤ‘1) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
123121, 122syl 17 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
124119, 123eqtrd 2805 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
125124raleqdv 3293 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
126118, 125mpbird 247 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
1271, 2, 3, 4, 5, 6efgsdm 18343 . 2 ((𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆 ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ∧ ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
12841, 54, 126, 127syl3anbrc 1428 1 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  {crab 3065  cdif 3720  cun 3721  wss 3723  c0 4063  {csn 4316  cop 4322  cotp 4324   ciun 4654   class class class wbr 4786  cmpt 4863   I cid 5156   × cxp 5247  dom cdm 5249  ran crn 5250  wf 6025  cfv 6029  (class class class)co 6791  cmpt2 6793  1𝑜c1o 7704  2𝑜c2o 7705  Fincfn 8107  0cc0 10136  1c1 10137   + caddc 10139  cle 10275  cmin 10466  cn 11220  0cn0 11492  cz 11577  cuz 11886  ...cfz 12526  ..^cfzo 12666  chash 13314  Word cword 13480   ++ cconcat 13482  ⟨“cs1 13483   splice csplice 13485  ⟨“cs2 13788   ~FG cefg 18319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-cnex 10192  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-ot 4325  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5821  df-ord 5867  df-on 5868  df-lim 5869  df-suc 5870  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-1st 7313  df-2nd 7314  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-1o 7711  df-2o 7712  df-oadd 7715  df-er 7894  df-map 8009  df-pm 8010  df-en 8108  df-dom 8109  df-sdom 8110  df-fin 8111  df-card 8963  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-nn 11221  df-n0 11493  df-z 11578  df-uz 11887  df-fz 12527  df-fzo 12667  df-hash 13315  df-word 13488  df-concat 13490  df-s1 13491  df-substr 13492  df-splice 13493  df-s2 13795
This theorem is referenced by:  efgsfo  18352  efgredlemd  18357  efgrelexlemb  18363
  Copyright terms: Public domain W3C validator