| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dmeq |
|- ( c = C -> dom c = dom C ) |
| 2 |
1
|
difeq1d |
|- ( c = C -> ( dom c \ { 0 } ) = ( dom C \ { 0 } ) ) |
| 3 |
|
fveq1 |
|- ( c = C -> ( c ` ( n - 1 ) ) = ( C ` ( n - 1 ) ) ) |
| 4 |
|
fveq1 |
|- ( c = C -> ( c ` n ) = ( C ` n ) ) |
| 5 |
3 4
|
breq12d |
|- ( c = C -> ( ( c ` ( n - 1 ) ) .< ( c ` n ) <-> ( C ` ( n - 1 ) ) .< ( C ` n ) ) ) |
| 6 |
2 5
|
raleqbidv |
|- ( c = C -> ( A. n e. ( dom c \ { 0 } ) ( c ` ( n - 1 ) ) .< ( c ` n ) <-> A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) ) |
| 7 |
|
df-chn |
|- ( .< Chain A ) = { c e. Word A | A. n e. ( dom c \ { 0 } ) ( c ` ( n - 1 ) ) .< ( c ` n ) } |
| 8 |
6 7
|
elrab2 |
|- ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) ) |