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

Theorem efgsp1 18414
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 18407 . . . . . . 7 (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
87simp1bi 1175 . . . . . 6 (𝐹 ∈ dom 𝑆𝐹 ∈ (Word 𝑊 ∖ {∅}))
98adantr 472 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ (Word 𝑊 ∖ {∅}))
109eldifad 3744 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ∈ Word 𝑊)
111, 2, 3, 4, 5, 6efgsf 18406 . . . . . . . . . . . 12 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
1211fdmi 6233 . . . . . . . . . . . . 13 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
1312feq2i 6215 . . . . . . . . . . . 12 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
1411, 13mpbir 222 . . . . . . . . . . 11 𝑆:dom 𝑆𝑊
1514ffvelrni 6548 . . . . . . . . . 10 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) ∈ 𝑊)
1615adantr 472 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) ∈ 𝑊)
171, 2, 3, 4efgtf 18399 . . . . . . . . 9 ((𝑆𝐹) ∈ 𝑊 → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1816, 17syl 17 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝑇‘(𝑆𝐹)) = (𝑎 ∈ (0...(♯‘(𝑆𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐹) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊))
1918simprd 489 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘(𝑆𝐹)):((0...(♯‘(𝑆𝐹))) × (𝐼 × 2𝑜))⟶𝑊)
2019frnd 6230 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘(𝑆𝐹)) ⊆ 𝑊)
21 simpr 477 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴 ∈ ran (𝑇‘(𝑆𝐹)))
2220, 21sseldd 3762 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐴𝑊)
2322s1cld 13574 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ⟨“𝐴”⟩ ∈ Word 𝑊)
24 ccatcl 13545 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
2510, 23, 24syl2anc 579 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊)
26 ccatlen 13546 . . . . . . 7 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
2710, 23, 26syl2anc 579 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)))
28 s1len 13577 . . . . . . 7 (♯‘⟨“𝐴”⟩) = 1
2928oveq2i 6853 . . . . . 6 ((♯‘𝐹) + (♯‘⟨“𝐴”⟩)) = ((♯‘𝐹) + 1)
3027, 29syl6eq 2815 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) = ((♯‘𝐹) + 1))
31 lencl 13505 . . . . . 6 (𝐹 ∈ Word 𝑊 → (♯‘𝐹) ∈ ℕ0)
32 nn0p1nn 11579 . . . . . 6 ((♯‘𝐹) ∈ ℕ0 → ((♯‘𝐹) + 1) ∈ ℕ)
3310, 31, 323syl 18 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) + 1) ∈ ℕ)
3430, 33eqeltrd 2844 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ)
35 wrdfin 13504 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 → (𝐹 ++ ⟨“𝐴”⟩) ∈ Fin)
36 hashnncl 13359 . . . . 5 ((𝐹 ++ ⟨“𝐴”⟩) ∈ Fin → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3725, 35, 363syl 18 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘(𝐹 ++ ⟨“𝐴”⟩)) ∈ ℕ ↔ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
3834, 37mpbid 223 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅)
39 eldifsn 4472 . . 3 ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ Word 𝑊 ∧ (𝐹 ++ ⟨“𝐴”⟩) ≠ ∅))
4025, 38, 39sylanbrc 578 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}))
41 eldifsni 4476 . . . . . . 7 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ≠ ∅)
429, 41syl 17 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 𝐹 ≠ ∅)
43 wrdfin 13504 . . . . . . 7 (𝐹 ∈ Word 𝑊𝐹 ∈ Fin)
44 hashnncl 13359 . . . . . . 7 (𝐹 ∈ Fin → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4510, 43, 443syl 18 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅))
4642, 45mpbird 248 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ)
47 lbfzo0 12716 . . . . 5 (0 ∈ (0..^(♯‘𝐹)) ↔ (♯‘𝐹) ∈ ℕ)
4846, 47sylibr 225 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘𝐹)))
49 ccatval1 13548 . . . 4 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
5010, 23, 48, 49syl3anc 1490 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) = (𝐹‘0))
517simp2bi 1176 . . . 4 (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷)
5251adantr 472 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹‘0) ∈ 𝐷)
5350, 52eqeltrd 2844 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷)
547simp3bi 1177 . . . . . 6 (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
5554adantr 472 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))
56 fzo0ss1 12706 . . . . . . . . . . 11 (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))
5756sseli 3757 . . . . . . . . . 10 (𝑖 ∈ (1..^(♯‘𝐹)) → 𝑖 ∈ (0..^(♯‘𝐹)))
58 ccatval1 13548 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
5957, 58syl3an3 1205 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = (𝐹𝑖))
60 elfzoel2 12677 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
61 peano2zm 11667 . . . . . . . . . . . . . . . 16 ((♯‘𝐹) ∈ ℤ → ((♯‘𝐹) − 1) ∈ ℤ)
6260, 61syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ∈ ℤ)
6360zred 11729 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℝ)
6463lem1d 11211 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1..^(♯‘𝐹)) → ((♯‘𝐹) − 1) ≤ (♯‘𝐹))
65 eluz2 11892 . . . . . . . . . . . . . . 15 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) ↔ (((♯‘𝐹) − 1) ∈ ℤ ∧ (♯‘𝐹) ∈ ℤ ∧ ((♯‘𝐹) − 1) ≤ (♯‘𝐹)))
6662, 60, 64, 65syl3anbrc 1443 . . . . . . . . . . . . . 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 579 . . . . . . . . . . . . . 14 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 ∈ (1..^(♯‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1))))
7271ibi 258 . . . . . . . . . . . . 13 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^((♯‘𝐹) − 1)))
7368, 72sseldd 3762 . . . . . . . . . . . 12 (𝑖 ∈ (1..^(♯‘𝐹)) → (𝑖 − 1) ∈ (0..^(♯‘𝐹)))
74 ccatval1 13548 . . . . . . . . . . . 12 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ (𝑖 − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7573, 74syl3an3 1205 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1)))
7675fveq2d 6379 . . . . . . . . . 10 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1))))
7776rneqd 5521 . . . . . . . . 9 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1))))
7859, 77eleq12d 2838 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
79783expa 1147 . . . . . . 7 (((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) ∧ 𝑖 ∈ (1..^(♯‘𝐹))) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8079ralbidva 3132 . . . . . 6 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8110, 23, 80syl2anc 579 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
8255, 81mpbird 248 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
8310, 31syl 17 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℕ0)
8483nn0cnd 11600 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ ℂ)
8584addid2d 10491 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (0 + (♯‘𝐹)) = (♯‘𝐹))
8685fveq2d 6379 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
87 1nn 11287 . . . . . . . . . . 11 1 ∈ ℕ
8828, 87eqeltri 2840 . . . . . . . . . 10 (♯‘⟨“𝐴”⟩) ∈ ℕ
8988a1i 11 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘⟨“𝐴”⟩) ∈ ℕ)
90 lbfzo0 12716 . . . . . . . . 9 (0 ∈ (0..^(♯‘⟨“𝐴”⟩)) ↔ (♯‘⟨“𝐴”⟩) ∈ ℕ)
9189, 90sylibr 225 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → 0 ∈ (0..^(♯‘⟨“𝐴”⟩)))
92 ccatval3 13550 . . . . . . . 8 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘⟨“𝐴”⟩))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9310, 23, 91, 92syl3anc 1490 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(0 + (♯‘𝐹))) = (⟨“𝐴”⟩‘0))
9486, 93eqtr3d 2801 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) = (⟨“𝐴”⟩‘0))
95 s1fv 13581 . . . . . . . 8 (𝐴 ∈ ran (𝑇‘(𝑆𝐹)) → (⟨“𝐴”⟩‘0) = 𝐴)
9695adantl 473 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) = 𝐴)
97 fzo0end 12768 . . . . . . . . . . . 12 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
9846, 97syl 17 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
99 ccatval1 13548 . . . . . . . . . . 11 ((𝐹 ∈ Word 𝑊 ∧ ⟨“𝐴”⟩ ∈ Word 𝑊 ∧ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
10010, 23, 98, 99syl3anc 1490 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
1011, 2, 3, 4, 5, 6efgsval 18408 . . . . . . . . . . 11 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
102101adantr 472 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
103100, 102eqtr4d 2802 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)) = (𝑆𝐹))
104103fveq2d 6379 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = (𝑇‘(𝑆𝐹)))
105104rneqd 5521 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))) = ran (𝑇‘(𝑆𝐹)))
10621, 96, 1053eltr4d 2859 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (⟨“𝐴”⟩‘0) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
10794, 106eqeltrd 2844 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
108 fvex 6388 . . . . . 6 (♯‘𝐹) ∈ V
109 fveq2 6375 . . . . . . 7 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) = ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)))
110 fvoveq1 6865 . . . . . . . . 9 (𝑖 = (♯‘𝐹) → ((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)) = ((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))
111110fveq2d 6379 . . . . . . . 8 (𝑖 = (♯‘𝐹) → (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
112111rneqd 5521 . . . . . . 7 (𝑖 = (♯‘𝐹) → ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) = ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
113109, 112eleq12d 2838 . . . . . 6 (𝑖 = (♯‘𝐹) → (((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1)))))
114108, 113ralsn 4379 . . . . 5 (∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ((𝐹 ++ ⟨“𝐴”⟩)‘(♯‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘((♯‘𝐹) − 1))))
115107, 114sylibr 225 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
116 ralunb 3956 . . . 4 (∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ (∀𝑖 ∈ (1..^(♯‘𝐹))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ∧ ∀𝑖 ∈ {(♯‘𝐹)} ((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
11782, 115, 116sylanbrc 578 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
11830oveq2d 6858 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = (1..^((♯‘𝐹) + 1)))
119 nnuz 11923 . . . . . . 7 ℕ = (ℤ‘1)
12046, 119syl6eleq 2854 . . . . . 6 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (♯‘𝐹) ∈ (ℤ‘1))
121 fzosplitsn 12784 . . . . . 6 ((♯‘𝐹) ∈ (ℤ‘1) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
122120, 121syl 17 . . . . 5 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^((♯‘𝐹) + 1)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
123118, 122eqtrd 2799 . . . 4 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩))) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
124123raleqdv 3292 . . 3 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
125117, 124mpbird 248 . 2 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1))))
1261, 2, 3, 4, 5, 6efgsdm 18407 . 2 ((𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆 ↔ ((𝐹 ++ ⟨“𝐴”⟩) ∈ (Word 𝑊 ∖ {∅}) ∧ ((𝐹 ++ ⟨“𝐴”⟩)‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐴”⟩)))((𝐹 ++ ⟨“𝐴”⟩)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ ⟨“𝐴”⟩)‘(𝑖 − 1)))))
12740, 53, 125, 126syl3anbrc 1443 1 ((𝐹 ∈ dom 𝑆𝐴 ∈ ran (𝑇‘(𝑆𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  {crab 3059  cdif 3729  cun 3730  wss 3732  c0 4079  {csn 4334  cop 4340  cotp 4342   ciun 4676   class class class wbr 4809  cmpt 4888   I cid 5184   × cxp 5275  dom cdm 5277  ran crn 5278  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  1𝑜c1o 7757  2𝑜c2o 7758  Fincfn 8160  0cc0 10189  1c1 10190   + caddc 10192  cle 10329  cmin 10520  cn 11274  0cn0 11538  cz 11624  cuz 11886  ...cfz 12533  ..^cfzo 12673  chash 13321  Word cword 13486   ++ cconcat 13541  ⟨“cs1 13566   splice csplice 13763  ⟨“cs2 13870   ~FG cefg 18383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-ot 4343  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13487  df-concat 13542  df-s1 13567  df-substr 13617  df-pfx 13662  df-splice 13765  df-s2 13877
This theorem is referenced by:  efgsfo  18417  efgredlemd  18422  efgrelexlemb  18429
  Copyright terms: Public domain W3C validator