Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sseqval Structured version   Visualization version   GIF version

Theorem sseqval 31867
 Description: Value of the strong sequence builder function. The set 𝑊 represents here the words of length greater than or equal to the lenght of the initial sequence 𝑀. (Contributed by Thierry Arnoux, 21-Apr-2019.)
Hypotheses
Ref Expression
sseqval.1 (𝜑𝑆 ∈ V)
sseqval.2 (𝜑𝑀 ∈ Word 𝑆)
sseqval.3 𝑊 = (Word 𝑆 ∩ (♯ “ (ℤ‘(♯‘𝑀))))
sseqval.4 (𝜑𝐹:𝑊𝑆)
Assertion
Ref Expression
sseqval (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝑀,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem sseqval
Dummy variables 𝑓 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sseq 31863 . . 3 seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))))
21a1i 11 . 2 (𝜑 → seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))))))
3 simprl 771 . . 3 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → 𝑚 = 𝑀)
43fveq2d 6663 . . . . 5 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (♯‘𝑚) = (♯‘𝑀))
5 simp1rr 1237 . . . . . . . . 9 (((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝑓 = 𝐹)
65fveq1d 6661 . . . . . . . 8 (((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑓𝑥) = (𝐹𝑥))
76s1eqd 13995 . . . . . . 7 (((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → ⟨“(𝑓𝑥)”⟩ = ⟨“(𝐹𝑥)”⟩)
87oveq2d 7167 . . . . . 6 (((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ++ ⟨“(𝑓𝑥)”⟩) = (𝑥 ++ ⟨“(𝐹𝑥)”⟩))
98mpoeq3dva 7226 . . . . 5 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)))
10 simprr 773 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → 𝑓 = 𝐹)
1110, 3fveq12d 6666 . . . . . . . . 9 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (𝑓𝑚) = (𝐹𝑀))
1211s1eqd 13995 . . . . . . . 8 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → ⟨“(𝑓𝑚)”⟩ = ⟨“(𝐹𝑀)”⟩)
133, 12oveq12d 7169 . . . . . . 7 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (𝑚 ++ ⟨“(𝑓𝑚)”⟩) = (𝑀 ++ ⟨“(𝐹𝑀)”⟩))
1413sneqd 4535 . . . . . 6 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)} = {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})
1514xpeq2d 5555 . . . . 5 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}) = (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))
164, 9, 15seqeq123d 13420 . . . 4 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})) = seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))
1716coeq2d 5703 . . 3 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)}))) = (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))))
183, 17uneq12d 4070 . 2 ((𝜑 ∧ (𝑚 = 𝑀𝑓 = 𝐹)) → (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓𝑚)”⟩)})))) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))))
19 sseqval.2 . . 3 (𝜑𝑀 ∈ Word 𝑆)
20 elex 3429 . . 3 (𝑀 ∈ Word 𝑆𝑀 ∈ V)
2119, 20syl 17 . 2 (𝜑𝑀 ∈ V)
22 sseqval.4 . . 3 (𝜑𝐹:𝑊𝑆)
23 sseqval.3 . . . 4 𝑊 = (Word 𝑆 ∩ (♯ “ (ℤ‘(♯‘𝑀))))
24 sseqval.1 . . . . 5 (𝜑𝑆 ∈ V)
25 wrdexg 13916 . . . . 5 (𝑆 ∈ V → Word 𝑆 ∈ V)
26 inex1g 5190 . . . . 5 (Word 𝑆 ∈ V → (Word 𝑆 ∩ (♯ “ (ℤ‘(♯‘𝑀)))) ∈ V)
2724, 25, 263syl 18 . . . 4 (𝜑 → (Word 𝑆 ∩ (♯ “ (ℤ‘(♯‘𝑀)))) ∈ V)
2823, 27eqeltrid 2857 . . 3 (𝜑𝑊 ∈ V)
29 fex 6981 . . 3 ((𝐹:𝑊𝑆𝑊 ∈ V) → 𝐹 ∈ V)
3022, 28, 29syl2anc 588 . 2 (𝜑𝐹 ∈ V)
31 df-lsw 13955 . . . . . 6 lastS = (𝑥 ∈ V ↦ (𝑥‘((♯‘𝑥) − 1)))
3231funmpt2 6375 . . . . 5 Fun lastS
3332a1i 11 . . . 4 (𝜑 → Fun lastS)
34 seqex 13413 . . . . 5 seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})) ∈ V
3534a1i 11 . . . 4 (𝜑 → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})) ∈ V)
36 cofunexg 7655 . . . 4 ((Fun lastS ∧ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})) ∈ V) → (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))) ∈ V)
3733, 35, 36syl2anc 588 . . 3 (𝜑 → (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))) ∈ V)
38 unexg 7471 . . 3 ((𝑀 ∈ V ∧ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))) ∈ V) → (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))) ∈ V)
3921, 37, 38syl2anc 588 . 2 (𝜑 → (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))) ∈ V)
402, 18, 21, 30, 39ovmpod 7298 1 (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  Vcvv 3410   ∪ cun 3857   ∩ cin 3858  {csn 4523   × cxp 5523  ◡ccnv 5524   “ cima 5528   ∘ ccom 5529  Fun wfun 6330  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151   ∈ cmpo 7153  1c1 10569   − cmin 10901  ℕ0cn0 11927  ℤ≥cuz 12275  seqcseq 13411  ♯chash 13733  Word cword 13906  lastSclsw 13954   ++ cconcat 13962  ⟨“cs1 13989  seqstrcsseq 31862 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-inf2 9130  ax-cnex 10624  ax-1cn 10626  ax-addcl 10628 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-map 8419  df-nn 11668  df-n0 11928  df-seq 13412  df-word 13907  df-lsw 13955  df-s1 13990  df-sseq 31863 This theorem is referenced by:  sseqfv1  31868  sseqfn  31869  sseqf  31871  sseqfv2  31873
 Copyright terms: Public domain W3C validator