Theorem chneq1

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

	Ref	Expression
Assertion	chneq1	$$⊢\underset{\dot{}}{<}=R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}={\mathrm{Chain}}_{A}R$$

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢\underset{\dot{}}{<}=R\to \left(c\left(x-1\right)\underset{\dot{}}{<}c\left(x\right)\leftrightarrow c\left(x-1\right)Rc\left(x\right)\right)$$
2	1	ralbidv	$$⊢\underset{\dot{}}{<}=R\to \left(\forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)\underset{\dot{}}{<}c\left(x\right)\leftrightarrow \forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)Rc\left(x\right)\right)$$
3	2	rabbidv	$$⊢\underset{\dot{}}{<}=R\to \left\{c\in \mathrm{Word}A|\forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)\underset{\dot{}}{<}c\left(x\right)\right\}=\left\{c\in \mathrm{Word}A|\forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)Rc\left(x\right)\right\}$$
4		df-chn	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}=\left\{c\in \mathrm{Word}A|\forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)\underset{\dot{}}{<}c\left(x\right)\right\}$$
5		df-chn	$$⊢{\mathrm{Chain}}_{A}R=\left\{c\in \mathrm{Word}A|\forall x\in \left(\mathrm{dom}c\setminus \left\{0\right\}\right)c\left(x-1\right)Rc\left(x\right)\right\}$$
6	3 4 5	3eqtr4g	$$⊢\underset{\dot{}}{<}=R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}={\mathrm{Chain}}_{A}R$$