Theorem chnwrd 18686

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 18685	. . 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 2146  ∀wral 3081   ∖ cdif 3903  {csn 4591   class class class wbr 5111  dom cdm 5663  ‘cfv 6540  (class class class)co 7419  0cc0 11115  1c1 11116   − cmin 11456  Word cword 14568   Chain cchn 18683

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-chn 18684

This theorem is used by:  pfxchn  18688  chnexg  18696  chnind  18699  chnub  18700  chnlt  18701  chnccats1  18703  chnccat  18704  chnrev  18705  chnflenfi  18706  chnf  18707  chnpolleha  18710  chnpolfz  18711  fldext2chn  34182  constrextdg2lem  34202  constrext2chnlem  34204  chnsubseqword  47652  chnsubseqwl  47653  chnsubseq  47654  chnsuslle  47655  chnerlem1  47656  chnerlem2  47657  chner  47659