Theorem chneq1

Description: Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	chneq1	|- ( .< = R -> ( .< Chain A ) = ( R Chain A ) )

Proof

Step	Hyp	Ref	Expression
1		breq	|- ( .< = R -> ( ( c ` ( x - 1 ) ) .< ( c ` x ) <-> ( c ` ( x - 1 ) ) R ( c ` x ) ) )
2	1	ralbidv	|- ( .< = R -> ( A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) <-> A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) R ( c ` x ) ) )
3	2	rabbidv	|- ( .< = R -> { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) } = { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) R ( c ` x ) } )
4		df-chn	|- ( .< Chain A ) = { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) }
5		df-chn	|- ( R Chain A ) = { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) R ( c ` x ) }
6	3 4 5	3eqtr4g	|- ( .< = R -> ( .< Chain A ) = ( R Chain A ) )