Theorem chnwrd 18791

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076   ∖ cdif 4044  {csn 4584   class class class wbr 5102  dom cdm 5651  ‘cfv 6543  (class class class)co 7424  0cc0 11207  1c1 11208   − cmin 11548  Word cword 14665   Chain cchn 18788

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5661  df-iota 6497  df-fv 6551  df-chn 18789

This theorem is used by:  pfxchn  18793  chnexg  18801  chnind  18804  chnub  18805  chnlt  18806  chnccats1  18808  chnccat  18809  chnrev  18810  chnflenfi  18811  chnf  18812  chnpolleha  18815  chnpolfz  18816  fldext2chn  34410  constrextdg2lem  34430  constrext2chnlem  34432  chnsubseqword  47996  chnsubseqwl  47997  chnsubseq  47998  chnsuslle  47999  chnerlem1  48000  chnerlem2  48001  chner  48003  chndin  48009