Theorem chnwrd 18565

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 18564	. . 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 2119  ∀wral 3053   ∖ cdif 3880  {csn 4555   class class class wbr 5072  dom cdm 5618  ‘cfv 6485  (class class class)co 7356  0cc0 11029  1c1 11030   − cmin 11368  Word cword 14466   Chain cchn 18562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493  df-chn 18563

This theorem is referenced by:  pfxchn  18567  chnexg  18575  chnind  18578  chnub  18579  chnlt  18580  chnccats1  18582  chnccat  18583  chnrev  18584  chnflenfi  18585  chnf  18586  chnpolleha  18589  chnpolfz  18590  fldext2chn  33912  constrextdg2lem  33932  constrext2chnlem  33934  chnsubseqword  47323  chnsubseqwl  47324  chnsubseq  47325  chnsuslle  47326  chnerlem1  47327  chnerlem2  47328  chner  47330