| 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 18639 | . . 3 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛))) | |
| 3 | 2 | simplbi 500 | . 2 ⊢ (𝐶 ∈ ( < Chain 𝐴) → 𝐶 ∈ Word 𝐴) |
| 4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → 𝐶 ∈ Word 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2142 ∀wral 3076 ∖ cdif 3901 {csn 4582 class class class wbr 5100 dom cdm 5647 ‘cfv 6521 (class class class)co 7396 0cc0 11073 1c1 11074 − cmin 11414 Word cword 14526 Chain cchn 18637 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-ral 3077 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-dm 5657 df-iota 6477 df-fv 6529 df-chn 18638 |
| This theorem is referenced by: pfxchn 18642 chnexg 18650 chnind 18653 chnub 18654 chnlt 18655 chnccats1 18657 chnccat 18658 chnrev 18659 chnflenfi 18660 chnf 18661 chnpolleha 18664 chnpolfz 18665 fldext2chn 34025 constrextdg2lem 34045 constrext2chnlem 34047 chnsubseqword 47454 chnsubseqwl 47455 chnsubseq 47456 chnsuslle 47457 chnerlem1 47458 chnerlem2 47459 chner 47461 |
| Copyright terms: Public domain | W3C validator |