| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > chnwrd | Structured version Visualization version GIF version | ||
| Description: A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| Ref | Expression |
|---|---|
| chnwrd.1 | ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴)) |
| Ref | Expression |
|---|---|
| chnwrd | ⊢ (𝜑 → 𝐶 ∈ Word 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chnwrd.1 | . 2 ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴)) | |
| 2 | ischn 18611 | . . 3 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛))) | |
| 3 | 2 | simplbi 499 | . 2 ⊢ (𝐶 ∈ ( < Chain 𝐴) → 𝐶 ∈ Word 𝐴) |
| 4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2132 ∀wral 3066 ∖ cdif 3892 {csn 4572 class class class wbr 5090 dom cdm 5636 ‘cfv 6506 (class class class)co 7381 0cc0 11059 1c1 11060 − cmin 11400 Word cword 14512 Chain cchn 18609 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-ext 2724 |
| This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-sb 2081 df-clab 2731 df-cleq 2744 df-clel 2827 df-ral 3067 df-rab 3405 df-v 3446 df-dif 3898 df-un 3900 df-ss 3912 df-nul 4277 df-if 4471 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4856 df-br 5091 df-dm 5646 df-iota 6462 df-fv 6514 df-chn 18610 |
| This theorem is referenced by: pfxchn 18614 chnexg 18622 chnind 18625 chnub 18626 chnlt 18627 chnccats1 18629 chnccat 18630 chnrev 18631 chnflenfi 18632 chnf 18633 chnpolleha 18636 chnpolfz 18637 fldext2chn 33969 constrextdg2lem 33989 constrext2chnlem 33991 chnsubseqword 47392 chnsubseqwl 47393 chnsubseq 47394 chnsuslle 47395 chnerlem1 47396 chnerlem2 47397 chner 47399 |
| Copyright terms: Public domain | W3C validator |