Metamath Proof Explorer

Theorem ischn

Description: Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Assertion ischn 
|- ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )

Proof

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 ) ) )