Theorem chneq2

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

	Ref	Expression
Assertion	chneq2	|- ( A = B -> ( .< Chain A ) = ( .< Chain B ) )

Proof

Step	Hyp	Ref	Expression
1		wrdeq	|- ( A = B -> Word A = Word B )
2		rabeq	|- ( Word A = Word B -> { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) } = { c e. Word B | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) } )
3	1 2	syl	|- ( A = B -> { c e. Word A | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) } = { c e. Word B | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( 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	|- ( .< Chain B ) = { c e. Word B | A. x e. ( dom c \ { 0 } ) ( c ` ( x - 1 ) ) .< ( c ` x ) }
6	3 4 5	3eqtr4g	|- ( A = B -> ( .< Chain A ) = ( .< Chain B ) )