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

Theorem ischn 32983
Description: Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
Assertion
Ref Expression
ischn (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
Distinct variable groups:   < ,𝑛   𝐴,𝑛   𝐶,𝑛

Proof of Theorem ischn
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 dmeq 5912 . . . 4 (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
21difeq1d 4124 . . 3 (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
3 fveq1 6903 . . . 4 (𝑐 = 𝐶 → (𝑐‘(𝑛 − 1)) = (𝐶‘(𝑛 − 1)))
4 fveq1 6903 . . . 4 (𝑐 = 𝐶 → (𝑐𝑛) = (𝐶𝑛))
53, 4breq12d 5154 . . 3 (𝑐 = 𝐶 → ((𝑐‘(𝑛 − 1)) < (𝑐𝑛) ↔ (𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
62, 5raleqbidv 3345 . 2 (𝑐 = 𝐶 → (∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛) ↔ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
7 df-chn 32982 . 2 ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
86, 7elrab2 3694 1 (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3060  cdif 3947  {csn 4624   class class class wbr 5141  dom cdm 5683  cfv 6559  (class class class)co 7429  0cc0 11151  1c1 11152  cmin 11488  Word cword 14548  Chaincchn 32981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-dm 5693  df-iota 6512  df-fv 6567  df-chn 32982
This theorem is referenced by:  chnwrd  32984  chnltm1  32985  pfxchn  32986  chnind  32987  chnso  32990
  Copyright terms: Public domain W3C validator