Theorem chnltm1

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

	Ref	Expression
Hypotheses	chnwrd.1	|- ( ph -> C e. ( .< Chain A ) )
	chnltm1.2	|- ( ph -> N e. ( dom C \ { 0 } ) )
Assertion	chnltm1	|- ( ph -> ( C ` ( N - 1 ) ) .< ( C ` N ) )

Proof

Step	Hyp	Ref	Expression
1		chnwrd.1	|- ( ph -> C e. ( .< Chain A ) )
2		chnltm1.2	|- ( ph -> N e. ( dom C \ { 0 } ) )
3		fvoveq1	|- ( n = N -> ( C ` ( n - 1 ) ) = ( C ` ( N - 1 ) ) )
4		fveq2	|- ( n = N -> ( C ` n ) = ( C ` N ) )
5	3 4	breq12d	|- ( n = N -> ( ( C ` ( n - 1 ) ) .< ( C ` n ) <-> ( C ` ( N - 1 ) ) .< ( C ` N ) ) )
6		ischn	|- ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
7	1 6	sylib	|- ( ph -> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
8	7	simprd	|- ( ph -> A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) )
9	5 8 2	rspcdva	|- ( ph -> ( C ` ( N - 1 ) ) .< ( C ` N ) )