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 32957
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 5911 . . . 4 (𝑐 = 𝐶 → dom 𝑐 = dom 𝐶)
21difeq1d 4135 . . 3 (𝑐 = 𝐶 → (dom 𝑐 ∖ {0}) = (dom 𝐶 ∖ {0}))
3 fveq1 6900 . . . 4 (𝑐 = 𝐶 → (𝑐‘(𝑛 − 1)) = (𝐶‘(𝑛 − 1)))
4 fveq1 6900 . . . 4 (𝑐 = 𝐶 → (𝑐𝑛) = (𝐶𝑛))
53, 4breq12d 5162 . . 3 (𝑐 = 𝐶 → ((𝑐‘(𝑛 − 1)) < (𝑐𝑛) ↔ (𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
62, 5raleqbidv 3342 . 2 (𝑐 = 𝐶 → (∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛) ↔ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
7 df-chn 32956 . 2 ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐𝑛)}
86, 7elrab2 3698 1 (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1535  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:  chnwrd  32958  chnltm1  32959  pfxchn  32960  chnind  32961  chnso  32964
  Copyright terms: Public domain W3C validator