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

Theorem efgsp1 18357
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 18350 . . . . . . 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 18349 . . . . . . . . . . . 12 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
1211fdmi 6194 . . . . . . . . . . . . 13 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
1312feq2i 6176 . . . . . . . . . . . 12 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
1411, 13mpbir 221 . . . . . . . . . . 11 𝑆:dom 𝑆𝑊
1514ffvelrni 6503 . . . . . . . . . 10 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) ∈ 𝑊)
1615adantr 466 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) ∈ 𝑊)
171, 2, 3, 4efgtf 18342 . . . . . . . . 9 ((𝑆𝐹) ∈ 𝑊 → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1816, 17syl 17 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1918simprd 483 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊)
2019frnd 6191 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
21 simpr 471 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴 ∈ ran (𝑇‘(𝑆𝐹)))
2220, 21sseldd 3753 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴𝑊)
2322s1cld 13583 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ⟨“𝐴”⟩ ∈ Word 𝑊)
24 ccatcl 13556 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
2510, 23, 24syl2anc 573 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
26 ccatlen 13557 . . . . . . 7 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
2710, 23, 26syl2anc 573 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
28 s1len 13586 . . . . . . 7 (♯‘⟨“𝐴”⟩) = 1
2928oveq2i 6807 . . . . . 6 ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)) = ((♯‘𝐹) + 1)
3027, 29syl6eq 2821 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + 1))
31 lencl 13520 . . . . . 6 (𝐹 ∈ Word 𝑊 → (♯‘𝐹) ∈ ℕ0)
32 nn0p1nn 11539 . . . . . 6 ((♯‘𝐹) ∈ ℕ0 → ((♯‘𝐹) + 1) ∈ ℕ)
3310, 31, 323syl 18 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) + 1) ∈ ℕ)
3430, 33eqeltrd 2850 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ)
35 wrdfin 13519 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 → (𝐹 ++ ⟨“𝐴”⟩) ∈ Fin)
36 hashnncl 13359 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Fin → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3725, 35, 363syl 18 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3834, 37mpbid 222 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅)
39 eldifsn 4454 . . 3 ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 ∧ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
4025, 38, 39sylanbrc 572 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}))
41 eldifsni 4458 . . . . . . 7 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ≠ ∅)
429, 41syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ≠ ∅)
43 wrdfin 13519 . . . . . . 7 (𝐹 ∈ Word 𝑊𝐹 ∈ Fin)
44 hashnncl 13359 . . . . . . 7 (𝐹 ∈ Fin → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4510, 43, 443syl 18 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4642, 45mpbird 247 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ)
47 lbfzo0 12716 . . . . 5 (0 ∈ (0..^(♯‘𝐹)) ↔ (♯‘𝐹) ∈ ℕ)
4846, 47sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘𝐹)))
49 ccatval1 13559 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
5010, 23, 48, 49syl3anc 1476 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
517simp2bi 1140 . . . 4 (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷)
5251adantr 466 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹‘0) ∈ 𝐷)
5350, 52eqeltrd 2850 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷)
547simp3bi 1141 . . . . . 6 (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
5554adantr 466 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
56 fzo0ss1 12706 . . . . . . . . . . 11 (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))
5756sseli 3748 . . . . . . . . . 10 (𝑖 ∈ (1..^(♯‘𝐹)) → 𝑖 ∈ (0..^(♯‘𝐹)))
58 ccatval1 13559 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
5957, 58syl3an3 1169 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
60 elfzoel2 12677 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
61 peano2zm 11627 . . . . . . . . . . . . . . . 16 ((♯‘𝐹) ∈ ℤ → ((♯‘𝐹) − 1) ∈ ℤ)
6260, 61syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ∈ ℤ)
6360zred 11689 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6463lem1d 11163 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ≤ (♯‘𝐹))
65 eluz2 11899 . . . . . . . . . . . . . . 15 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) ↔ (((♯‘𝐹) − 1) ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ ∧ ((♯‘𝐹) − 1) ≤ (♯‘𝐹)))
6662, 60, 64, 65syl3anbrc 1428 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)))
67 fzoss2 12704 . . . . . . . . . . . . . 14 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
6866, 67syl 17 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(♯‘𝐹)) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
69 elfzoelz 12678 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → 𝑖 ∈ ℤ)
70 elfzom1b 12775 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ) → (𝑖 ∈ (1..^(♯‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1))))
7169, 60, 70syl2anc 573 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 ∈ (1..^(♯‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1))))
7271ibi 256 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1)))
7368, 72sseldd 3753 . . . . . . . . . . . 12 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^(♯‘𝐹)))
74 ccatval1 13559 . . . . . . . . . . . 12 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ (𝑖 − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7573, 74syl3an3 1169 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7675fveq2d 6337 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1))))
7776rneqd 5490 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1))))
7859, 77eleq12d 2844 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
79783expa 1111 . . . . . . 7 (((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) ∧ 𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8079ralbidva 3134 . . . . . 6 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8110, 23, 80syl2anc 573 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8255, 81mpbird 247 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
8310, 31syl 17 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ0)
8483nn0cnd 11560 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℂ)
8584addid2d 10443 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (0 + (♯‘𝐹)) = (♯‘𝐹))
8685fveq2d 6337 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
87 1nn 11237 . . . . . . . . . . 11 1 ∈ ℕ
8828, 87eqeltri 2846 . . . . . . . . . 10 (♯‘⟨“𝐴”⟩) ∈ ℕ
8988a1i 11 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘⟨“𝐴”⟩) ∈ ℕ)
90 lbfzo0 12716 . . . . . . . . 9 (0 ∈ (0..^(♯‘⟨“𝐴”⟩)) ↔ (♯‘⟨“𝐴”⟩) ∈ ℕ)
9189, 90sylibr 224 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘⟨“𝐴”⟩)))
92 ccatval3 13561 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘⟨“𝐴”⟩))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9310, 23, 91, 92syl3anc 1476 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9486, 93eqtr3d 2807 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) = (⟨“𝐴”⟩‘0))
95 s1fv 13590 . . . . . . . 8 (𝐴 ∈ ran (𝑇‘(𝑆𝐹)) → (⟨“𝐴”⟩‘0) = 𝐴)
9695adantl 467 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) = 𝐴)
97 fzo0end 12768 . . . . . . . . . . . 12 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
9846, 97syl 17 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
99 ccatval1 13559 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
10010, 23, 98, 99syl3anc 1476 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
1011, 2, 3, 4, 5, 6efgsval 18351 . . . . . . . . . . 11 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
102101adantr 466 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
103100, 102eqtr4d 2808 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝑆𝐹))
104103fveq2d 6337 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = (𝑇‘(𝑆𝐹)))
105104rneqd 5490 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = ran (𝑇‘(𝑆𝐹)))
10621, 96, 1053eltr4d 2865 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
10794, 106eqeltrd 2850 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
108 fvex 6344 . . . . . 6 (♯‘𝐹) ∈ V
109 fveq2 6333 . . . . . . 7 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
110 fvoveq1 6819 . . . . . . . . 9 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))
111110fveq2d 6337 . . . . . . . 8 (𝑖 = (♯‘𝐹) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
112111rneqd 5490 . . . . . . 7 (𝑖 = (♯‘𝐹) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
113109, 112eleq12d 2844 . . . . . 6 (𝑖 = (♯‘𝐹) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))))
114108, 113ralsn 4361 . . . . 5 (∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
115107, 114sylibr 224 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
116 ralunb 3945 . . . 4 (∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ∧ ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
11782, 115, 116sylanbrc 572 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
11830oveq2d 6812 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = (1..^((♯‘𝐹) + 1)))
119 nnuz 11930 . . . . . . 7 ℕ = (ℤ‘1)
12046, 119syl6eleq 2860 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ (ℤ‘1))
121 fzosplitsn 12784 . . . . . 6 ((♯‘𝐹) ∈ (ℤ‘1) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
122120, 121syl 17 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
123118, 122eqtrd 2805 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
124123raleqdv 3293 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
125117, 124mpbird 247 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
1261, 2, 3, 4, 5, 6efgsdm 18350 . 2 ((𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆 ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ∧ ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
12740, 53, 125, 126syl3anbrc 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 4317  cop 4323  cotp 4325   ciun 4655   class class class wbr 4787  cmpt 4864   I cid 5157   × cxp 5248  dom cdm 5250  ran crn 5251  wf 6026  cfv 6030  (class class class)co 6796  cmpt2 6798  1𝑜c1o 7710  2𝑜c2o 7711  Fincfn 8113  0cc0 10142  1c1 10143   + caddc 10145  cle 10281  cmin 10472  cn 11226  0cn0 11499  cz 11584  cuz 11893  ...cfz 12533  ..^cfzo 12673  chash 13321  Word cword 13487   ++ cconcat 13489  ⟨“cs1 13490   splice csplice 13492  ⟨“cs2 13795   ~FG cefg 18326
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 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100  ax-cnex 10198  ax-resscn 10199  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-addrcl 10203  ax-mulcl 10204  ax-mulrcl 10205  ax-mulcom 10206  ax-addass 10207  ax-mulass 10208  ax-distr 10209  ax-i2m1 10210  ax-1ne0 10211  ax-1rid 10212  ax-rnegex 10213  ax-rrecex 10214  ax-cnre 10215  ax-pre-lttri 10216  ax-pre-lttrn 10217  ax-pre-ltadd 10218  ax-pre-mulgt0 10219
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 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-ot 4326  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-om 7217  df-1st 7319  df-2nd 7320  df-wrecs 7563  df-recs 7625  df-rdg 7663  df-1o 7717  df-2o 7718  df-oadd 7721  df-er 7900  df-map 8015  df-pm 8016  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-card 8969  df-pnf 10282  df-mnf 10283  df-xr 10284  df-ltxr 10285  df-le 10286  df-sub 10474  df-neg 10475  df-nn 11227  df-n0 11500  df-z 11585  df-uz 11894  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13495  df-concat 13497  df-s1 13498  df-substr 13499  df-splice 13500  df-s2 13802
This theorem is referenced by:  efgsfo  18359  efgredlemd  18364  efgrelexlemb  18370
  Copyright terms: Public domain W3C validator