Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  chnwrd Structured version   Visualization version   GIF version

Theorem chnwrd 32958
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.
StepHypRef Expression
1 chnwrd.1 . 2 (𝜑𝐶 ∈ ( < Chain𝐴))
2 ischn 32957 . . 3 (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
32simplbi 497 . 2 (𝐶 ∈ ( < Chain𝐴) → 𝐶 ∈ Word 𝐴)
41, 3syl 17 1 (𝜑𝐶 ∈ Word 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2104  wral 3057  cdif 3960  {csn 4630   class class class wbr 5149  dom cdm 5683  cfv 6558  (class class class)co 7425  0cc0 11146  1c1 11147  cmin 11483  Word cword 14538  Chaincchn 32955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-ext 2704
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-sb 2061  df-clab 2711  df-cleq 2725  df-clel 2812  df-ral 3058  df-rab 3433  df-v 3479  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4915  df-br 5150  df-dm 5693  df-iota 6510  df-fv 6566  df-chn 32956
This theorem is referenced by:  pfxchn  32960  chnind  32961  chnub  32962  chnlt  32963  fldext2chn  33697
  Copyright terms: Public domain W3C validator