Theorem chnwrd 18529

Description: A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)

Hypothesis

Ref	Expression
chnwrd.1	⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))

Assertion

Ref	Expression
chnwrd	⊢ (𝜑 → 𝐶 ∈ Word 𝐴)

Proof of Theorem chnwrd

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		chnwrd.1	. 2 ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))
2		ischn 18528	. . 3 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
3	2	simplbi 497	. 2 ⊢ (𝐶 ∈ ( < Chain 𝐴) → 𝐶 ∈ Word 𝐴)
4	1, 3	syl 17	1 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3049   ∖ cdif 3896  {csn 4578   class class class wbr 5096  dom cdm 5622  ‘cfv 6490  (class class class)co 7356  0cc0 11024  1c1 11025   − cmin 11362  Word cword 14434   Chain cchn 18526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632  df-iota 6446  df-fv 6498  df-chn 18527

This theorem is referenced by:  pfxchn  18531  chnexg  18539  chnind  18542  chnub  18543  chnlt  18544  chnccats1  18546  chnccat  18547  chnrev  18548  chnflenfi  18549  chnf  18550  chnpolleha  18553  chnpolfz  18554  fldext2chn  33834  constrextdg2lem  33854  constrext2chnlem  33856  chnsubseqword  47064  chnsubseqwl  47065  chnsubseq  47066  chnsuslle  47067  chnerlem1  47068  chnerlem2  47069  chner  47071