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

Theorem efgcpbllemb 18810
Description: Lemma for efgrelex 18806. Show that 𝐿 is an equivalence relation containing all direct extensions of a word, so is closed under . (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
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)))
efgcpbllem.1 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
Assertion
Ref Expression
efgcpbllemb ((𝐴𝑊𝐵𝑊) → 𝐿)
Distinct variable groups:   𝑖,𝑗,𝐴   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑖,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑗   𝑖,𝑘,𝑇,𝑗,𝑚,𝑡,𝑥   𝑦,𝑖,𝑧,𝑊,𝑗   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑖,𝑗,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑖,𝑗   𝑆,𝑖,𝑗   𝑖,𝐼,𝑗,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑖,𝑗,𝑚,𝑡
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑖,𝑗,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgcpbllemb
Dummy variables 𝑎 𝑏 𝑐 𝑓 𝑔 𝑟 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . 3 𝑊 = ( I ‘Word (𝐼 × 2o))
2 efgval.r . . 3 = ( ~FG𝐼)
3 efgval2.m . . 3 𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
4 efgval2.t . . 3 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
51, 2, 3, 4efgval2 18779 . 2 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)}
6 efgcpbllem.1 . . . . . . 7 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ((𝐴 ++ 𝑗) ++ 𝐵))}
76relopabi 5687 . . . . . 6 Rel 𝐿
87a1i 11 . . . . 5 ((𝐴𝑊𝐵𝑊) → Rel 𝐿)
9 efgred.d . . . . . . . . 9 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
10 efgred.s . . . . . . . . 9 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
111, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . . . 8 (𝑓𝐿𝑔 ↔ (𝑓𝑊𝑔𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵)))
1211simp2bi 1138 . . . . . . 7 (𝑓𝐿𝑔𝑔𝑊)
1312adantl 482 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝑊)
1411simp1bi 1137 . . . . . . 7 (𝑓𝐿𝑔𝑓𝑊)
1514adantl 482 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑓𝑊)
161, 2efger 18773 . . . . . . . 8 Er 𝑊
1716a1i 11 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → Er 𝑊)
1811simp3bi 1139 . . . . . . . 8 (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
1918adantl 482 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
2017, 19ersym 8290 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))
211, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . 6 (𝑔𝐿𝑓 ↔ (𝑔𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
2213, 15, 20, 21syl3anbrc 1335 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓)
2314ad2antrl 724 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑓𝑊)
241, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . . . 8 (𝑔𝐿 ↔ (𝑔𝑊𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵)))
2524simp2bi 1138 . . . . . . 7 (𝑔𝐿𝑊)
2625ad2antll 725 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑊)
2716a1i 11 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → Er 𝑊)
2818ad2antrl 724 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑔) ++ 𝐵))
2924simp3bi 1139 . . . . . . . 8 (𝑔𝐿 → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
3029ad2antll 725 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑔) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
3127, 28, 30ertrd 8294 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵))
321, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . 6 (𝑓𝐿 ↔ (𝑓𝑊𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ ) ++ 𝐵)))
3323, 26, 31, 32syl3anbrc 1335 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ (𝑓𝐿𝑔𝑔𝐿)) → 𝑓𝐿)
3416a1i 11 . . . . . . . . 9 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → Er 𝑊)
35 fviss 6734 . . . . . . . . . . . . . 14 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
361, 35eqsstri 3998 . . . . . . . . . . . . 13 𝑊 ⊆ Word (𝐼 × 2o)
37 simpll 763 . . . . . . . . . . . . 13 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐴𝑊)
3836, 37sseldi 3962 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐴 ∈ Word (𝐼 × 2o))
39 simpr 485 . . . . . . . . . . . . 13 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑓𝑊)
4036, 39sseldi 3962 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑓 ∈ Word (𝐼 × 2o))
41 ccatcl 13914 . . . . . . . . . . . 12 ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
4238, 40, 41syl2anc 584 . . . . . . . . . . 11 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
43 simplr 765 . . . . . . . . . . . 12 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐵𝑊)
4436, 43sseldi 3962 . . . . . . . . . . 11 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝐵 ∈ Word (𝐼 × 2o))
45 ccatcl 13914 . . . . . . . . . . 11 (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
4642, 44, 45syl2anc 584 . . . . . . . . . 10 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o))
471efgrcl 18770 . . . . . . . . . . . 12 (𝐴𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
4847simprd 496 . . . . . . . . . . 11 (𝐴𝑊𝑊 = Word (𝐼 × 2o))
4948ad2antrr 722 . . . . . . . . . 10 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → 𝑊 = Word (𝐼 × 2o))
5046, 49eleqtrrd 2913 . . . . . . . . 9 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
5134, 50erref 8298 . . . . . . . 8 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))
5251ex 413 . . . . . . 7 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5352pm4.71d 562 . . . . . 6 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊 ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵))))
541, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . . 7 (𝑓𝐿𝑓 ↔ (𝑓𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
55 df-3an 1081 . . . . . . 7 ((𝑓𝑊𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓𝑊𝑓𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
56 anidm 565 . . . . . . . 8 ((𝑓𝑊𝑓𝑊) ↔ 𝑓𝑊)
5756anbi1i 623 . . . . . . 7 (((𝑓𝑊𝑓𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5854, 55, 573bitri 298 . . . . . 6 (𝑓𝐿𝑓 ↔ (𝑓𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ 𝑓) ++ 𝐵)))
5953, 58syl6bbr 290 . . . . 5 ((𝐴𝑊𝐵𝑊) → (𝑓𝑊𝑓𝐿𝑓))
608, 22, 33, 59iserd 8304 . . . 4 ((𝐴𝑊𝐵𝑊) → 𝐿 Er 𝑊)
611, 2, 3, 4efgtf 18777 . . . . . . . . . 10 (𝑓𝑊 → ((𝑇𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊))
6261simprd 496 . . . . . . . . 9 (𝑓𝑊 → (𝑇𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
6362adantl 482 . . . . . . . 8 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑇𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
64 ffn 6507 . . . . . . . 8 ((𝑇𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)))
65 ovelrn 7313 . . . . . . . 8 ((𝑇𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇𝑓)𝑢)))
6663, 64, 653syl 18 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑎 ∈ ran (𝑇𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇𝑓)𝑢)))
67 simplr 765 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝑊)
6862ad2antlr 723 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)
69 simprl 767 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ (0...(♯‘𝑓)))
70 simprr 769 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o))
7168, 69, 70fovrnd 7309 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇𝑓)𝑢) ∈ 𝑊)
7250adantr 481 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊)
7337adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴𝑊)
7436, 73sseldi 3962 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o))
7540adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o))
76 pfxcl 14027 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
7775, 76syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o))
78 ccatcl 13914 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
7974, 77, 78syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o))
803efgmf 18768 . . . . . . . . . . . . . . . . . 18 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
8180ffvelrni 6842 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ (𝐼 × 2o) → (𝑀𝑢) ∈ (𝐼 × 2o))
8281ad2antll 725 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀𝑢) ∈ (𝐼 × 2o))
8370, 82s2cld 14221 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2o))
84 ccatcl 13914 . . . . . . . . . . . . . . 15 (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o))
8579, 83, 84syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o))
86 swrdcl 13995 . . . . . . . . . . . . . . 15 (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
8775, 86syl 17 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o))
8844adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐵 ∈ Word (𝐼 × 2o))
89 ccatass 13930 . . . . . . . . . . . . . 14 ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
9085, 87, 88, 89syl3anc 1363 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
91 ccatcl 13914 . . . . . . . . . . . . . . . . 17 (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o))
9277, 83, 91syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o))
93 ccatass 13930 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
9474, 92, 87, 93syl3anc 1363 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
95 ccatass 13930 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩)))
9674, 77, 83, 95syl3anc 1363 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩)))
9796oveq1d 7160 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
981, 2, 3, 4efgtval 18778 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑊𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩))
9967, 69, 70, 98syl3anc 1363 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇𝑓)𝑢) = (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩))
100 splval 14101 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ ⟨“𝑢(𝑀𝑢)”⟩ ∈ Word (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
10167, 69, 69, 83, 100syl13anc 1364 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice ⟨𝑐, 𝑐, ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
10299, 101eqtrd 2853 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
103102oveq2d 7161 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
10494, 97, 1033eqtr4rd 2864 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)))
105104oveq1d 7160 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵))
106 lencl 13871 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ Word (𝐼 × 2o) → (♯‘𝐴) ∈ ℕ0)
10774, 106syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℕ0)
108 nn0uz 12268 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
109107, 108eleqtrdi 2920 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ (ℤ‘0))
110 elfznn0 12988 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ (0...(♯‘𝑓)) → 𝑐 ∈ ℕ0)
111110ad2antrl 724 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℕ0)
112 uzaddcl 12292 . . . . . . . . . . . . . . . . 17 (((♯‘𝐴) ∈ (ℤ‘0) ∧ 𝑐 ∈ ℕ0) → ((♯‘𝐴) + 𝑐) ∈ (ℤ‘0))
113109, 111, 112syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (ℤ‘0))
11442adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o))
115 ccatlen 13915 . . . . . . . . . . . . . . . . . 18 (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
116114, 88, 115syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)))
117 ccatlen 13915 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
11874, 75, 117syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓)))
119 elfzuz3 12893 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ (0...(♯‘𝑓)) → (♯‘𝑓) ∈ (ℤ𝑐))
120119ad2antrl 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ𝑐))
121107nn0zd 12073 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℤ)
122 eluzadd 12261 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑓) ∈ (ℤ𝑐) ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ‘(𝑐 + (♯‘𝐴))))
123120, 121, 122syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) ∈ (ℤ‘(𝑐 + (♯‘𝐴))))
124 lencl 13871 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ Word (𝐼 × 2o) → (♯‘𝑓) ∈ ℕ0)
12575, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℕ0)
126125nn0cnd 11945 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ ℂ)
127107nn0cnd 11945 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐴) ∈ ℂ)
128126, 127addcomd 10830 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝑓) + (♯‘𝐴)) = ((♯‘𝐴) + (♯‘𝑓)))
129111nn0cnd 11945 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈ ℂ)
130129, 127addcomd 10830 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐))
131130fveq2d 6667 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (ℤ‘(𝑐 + (♯‘𝐴))) = (ℤ‘((♯‘𝐴) + 𝑐)))
132123, 128, 1313eltr3d 2924 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘𝑓)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)))
133118, 132eqeltrd 2910 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ 𝑓)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)))
134 lencl 13871 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Word (𝐼 × 2o) → (♯‘𝐵) ∈ ℕ0)
13588, 134syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝐵) ∈ ℕ0)
136 uzaddcl 12292 . . . . . . . . . . . . . . . . . 18 (((♯‘(𝐴 ++ 𝑓)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)))
137133, 135, 136syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)))
138116, 137eqeltrd 2910 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ‘((♯‘𝐴) + 𝑐)))
139 elfzuzb 12890 . . . . . . . . . . . . . . . 16 (((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ‘0) ∧ (♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈ (ℤ‘((♯‘𝐴) + 𝑐))))
140113, 138, 139sylanbrc 583 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))))
1411, 2, 3, 4efgtval 18778 . . . . . . . . . . . . . . 15 ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩))
14272, 140, 70, 141syl3anc 1363 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩))
143 wrd0 13877 . . . . . . . . . . . . . . . 16 ∅ ∈ Word (𝐼 × 2o)
144143a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅ ∈ Word (𝐼 × 2o))
145 ccatcl 13914 . . . . . . . . . . . . . . . 16 (((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
14687, 88, 145syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵) ∈ Word (𝐼 × 2o))
147 ccatrid 13929 . . . . . . . . . . . . . . . . . 18 ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
14879, 147syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐)))
149148oveq1d 7160 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
150 ccatass 13930 . . . . . . . . . . . . . . . . 17 (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
15179, 87, 88, 150syl3anc 1363 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
152 ccatass 13930 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
15374, 77, 87, 152syl3anc 1363 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))))
154125, 108eleqtrdi 2920 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (ℤ‘0))
155 eluzfz2 12903 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑓) ∈ (ℤ‘0) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
156154, 155syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘𝑓) ∈ (0...(♯‘𝑓)))
157 ccatpfx 14051 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ (♯‘𝑓) ∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
15875, 69, 156, 157syl3anc 1363 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝑓 prefix (♯‘𝑓)))
159 pfxid 14034 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
16075, 159syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix (♯‘𝑓)) = 𝑓)
161158, 160eqtrd 2853 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = 𝑓)
162161oveq2d 7161 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩))) = (𝐴 ++ 𝑓))
163153, 162eqtrd 2853 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) = (𝐴 ++ 𝑓))
164163oveq1d 7160 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr ⟨𝑐, (♯‘𝑓)⟩)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵))
165149, 151, 1643eqtr2rd 2860 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
166 ccatlen 13915 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
16774, 77, 166syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))))
168 pfxlen 14033 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈ (0...(♯‘𝑓))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
16975, 69, 168syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (♯‘(𝑓 prefix 𝑐)) = 𝑐)
170169oveq2d 7161 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐))) = ((♯‘𝐴) + 𝑐))
171167, 170eqtr2d 2854 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐))))
172 hash0 13716 . . . . . . . . . . . . . . . . 17 (♯‘∅) = 0
173172oveq2i 7156 . . . . . . . . . . . . . . . 16 (((♯‘𝐴) + 𝑐) + (♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0)
174107, 111nn0addcld 11947 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℕ0)
175174nn0cnd 11945 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) ∈ ℂ)
176175addid1d 10828 . . . . . . . . . . . . . . . 16 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐))
177173, 176syl5req 2866 . . . . . . . . . . . . . . 15 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) + (♯‘∅)))
17879, 144, 146, 83, 165, 171, 177splval2 14107 . . . . . . . . . . . . . 14 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), ⟨“𝑢(𝑀𝑢)”⟩⟩) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
179142, 178eqtrd 2853 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ⟨“𝑢(𝑀𝑢)”⟩) ++ ((𝑓 substr ⟨𝑐, (♯‘𝑓)⟩) ++ 𝐵)))
18090, 105, 1793eqtr4d 2863 . . . . . . . . . . . 12 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) = (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢))
1811, 2, 3, 4efgtf 18777 . . . . . . . . . . . . . . 15 (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊))
182181simprd 496 . . . . . . . . . . . . . 14 (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)
183 ffn 6507 . . . . . . . . . . . . . 14 ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
18472, 182, 1833syl 18 . . . . . . . . . . . . 13 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)))
185 fnovrn 7312 . . . . . . . . . . . . 13 (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
186184, 140, 70, 185syl3anc 1363 . . . . . . . . . . . 12 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
187180, 186eqeltrd 2910 . . . . . . . . . . 11 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)))
1881, 2, 3, 4efgi2 18780 . . . . . . . . . . 11 ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵))
18972, 187, 188syl2anc 584 . . . . . . . . . 10 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵))
1901, 2, 3, 4, 9, 10, 6efgcpbllema 18809 . . . . . . . . . 10 (𝑓𝐿(𝑐(𝑇𝑓)𝑢) ↔ (𝑓𝑊 ∧ (𝑐(𝑇𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ((𝐴 ++ (𝑐(𝑇𝑓)𝑢)) ++ 𝐵)))
19167, 71, 189, 190syl3anbrc 1335 . . . . . . . . 9 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇𝑓)𝑢))
192 vex 3495 . . . . . . . . . . 11 𝑎 ∈ V
193 vex 3495 . . . . . . . . . . 11 𝑓 ∈ V
194192, 193elec 8322 . . . . . . . . . 10 (𝑎 ∈ [𝑓]𝐿𝑓𝐿𝑎)
195 breq2 5061 . . . . . . . . . 10 (𝑎 = (𝑐(𝑇𝑓)𝑢) → (𝑓𝐿𝑎𝑓𝐿(𝑐(𝑇𝑓)𝑢)))
196194, 195syl5bb 284 . . . . . . . . 9 (𝑎 = (𝑐(𝑇𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿𝑓𝐿(𝑐(𝑇𝑓)𝑢)))
197191, 196syl5ibrcom 248 . . . . . . . 8 ((((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
198197rexlimdvva 3291 . . . . . . 7 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿))
19966, 198sylbid 241 . . . . . 6 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → (𝑎 ∈ ran (𝑇𝑓) → 𝑎 ∈ [𝑓]𝐿))
200199ssrdv 3970 . . . . 5 (((𝐴𝑊𝐵𝑊) ∧ 𝑓𝑊) → ran (𝑇𝑓) ⊆ [𝑓]𝐿)
201200ralrimiva 3179 . . . 4 ((𝐴𝑊𝐵𝑊) → ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)
2021fvexi 6677 . . . . . 6 𝑊 ∈ V
203 erex 8302 . . . . . 6 (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V))
20460, 202, 203mpisyl 21 . . . . 5 ((𝐴𝑊𝐵𝑊) → 𝐿 ∈ V)
205 ereq1 8285 . . . . . . 7 (𝑟 = 𝐿 → (𝑟 Er 𝑊𝐿 Er 𝑊))
206 eceq2 8318 . . . . . . . . 9 (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿)
207206sseq2d 3996 . . . . . . . 8 (𝑟 = 𝐿 → (ran (𝑇𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇𝑓) ⊆ [𝑓]𝐿))
208207ralbidv 3194 . . . . . . 7 (𝑟 = 𝐿 → (∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿))
209205, 208anbi12d 630 . . . . . 6 (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
210209elabg 3663 . . . . 5 (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
211204, 210syl 17 . . . 4 ((𝐴𝑊𝐵𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝐿)))
21260, 201, 211mpbir2and 709 . . 3 ((𝐴𝑊𝐵𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)})
213 intss1 4882 . . 3 (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
214212, 213syl 17 . 2 ((𝐴𝑊𝐵𝑊) → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓𝑊 ran (𝑇𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿)
2155, 214eqsstrid 4012 1 ((𝐴𝑊𝐵𝑊) → 𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  {cab 2796  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  wss 3933  c0 4288  {csn 4557  {cpr 4559  cop 4563  cotp 4565   cint 4867   ciun 4910   class class class wbr 5057  {copab 5119  cmpt 5137   I cid 5452   × cxp 5546  ran crn 5549  Rel wrel 5553   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  1oc1o 8084  2oc2o 8085   Er wer 8275  [cec 8276  0cc0 10525  1c1 10526   + caddc 10528  cmin 10858  0cn0 11885  cz 11969  cuz 12231  ...cfz 12880  ..^cfzo 13021  chash 13678  Word cword 13849   ++ cconcat 13910   substr csubstr 13990   prefix cpfx 14020   splice csplice 14099  ⟨“cs2 14191   ~FG cefg 18761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-ot 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-ec 8280  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12881  df-fzo 13022  df-hash 13679  df-word 13850  df-concat 13911  df-s1 13938  df-substr 13991  df-pfx 14021  df-splice 14100  df-s2 14198  df-efg 18764
This theorem is referenced by:  efgcpbl  18811
  Copyright terms: Public domain W3C validator