Theorem chnwrd 18612

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 18611	. . 3 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
3	2	simplbi 499	. 2 ⊢ (𝐶 ∈ ( < Chain 𝐴) → 𝐶 ∈ Word 𝐴)
4	1, 3	syl 17	1 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2132  ∀wral 3066   ∖ cdif 3892  {csn 4572   class class class wbr 5090  dom cdm 5636  ‘cfv 6506  (class class class)co 7381  0cc0 11059  1c1 11060   − cmin 11400  Word cword 14512   Chain cchn 18609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-dm 5646  df-iota 6462  df-fv 6514  df-chn 18610

This theorem is referenced by:  pfxchn  18614  chnexg  18622  chnind  18625  chnub  18626  chnlt  18627  chnccats1  18629  chnccat  18630  chnrev  18631  chnflenfi  18632  chnf  18633  chnpolleha  18636  chnpolfz  18637  fldext2chn  33969  constrextdg2lem  33989  constrext2chnlem  33991  chnsubseqword  47392  chnsubseqwl  47393  chnsubseq  47394  chnsuslle  47395  chnerlem1  47396  chnerlem2  47397  chner  47399