Theorem chnwrd 18659

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079   ∖ cdif 3902  {csn 4589   class class class wbr 5109  dom cdm 5661  ‘cfv 6536  (class class class)co 7410  0cc0 11095  1c1 11096   − cmin 11436  Word cword 14546   Chain cchn 18656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544  df-chn 18657

This theorem is referenced by:  pfxchn  18661  chnexg  18669  chnind  18672  chnub  18673  chnlt  18674  chnccats1  18676  chnccat  18677  chnrev  18678  chnflenfi  18679  chnf  18680  chnpolleha  18683  chnpolfz  18684  fldext2chn  34118  constrextdg2lem  34138  constrext2chnlem  34140  chnsubseqword  47594  chnsubseqwl  47595  chnsubseq  47596  chnsuslle  47597  chnerlem1  47598  chnerlem2  47599  chner  47601