Theorem chner

Description: Any two elements are equivalent in a chain constructed on an equivalence relation. (Contributed by Ender Ting, 29-Jan-2026)

	Ref	Expression
Hypotheses	chner.1	|- ( ph -> .~ Er A )
	chner.2	|- ( ph -> C e. ( .~ Chain A ) )
	chner.3	|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
	chner.4	|- ( ph -> I e. ( 0 ..^ ( # ` C ) ) )
Assertion	chner	|- ( ph -> ( C ` I ) .~ ( C ` J ) )

Proof

Step	Hyp	Ref	Expression
1		chner.1	|- ( ph -> .~ Er A )
2		chner.2	|- ( ph -> C e. ( .~ Chain A ) )
3		chner.3	|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
4		chner.4	|- ( ph -> I e. ( 0 ..^ ( # ` C ) ) )
5	1 2 3	chnerlem2	|- ( ( ph /\ I e. ( 0 ..^ J ) ) -> ( C ` I ) .~ ( C ` J ) )
6	1	adantr	|- ( ( ph /\ J e. ( 0 ..^ I ) ) -> .~ Er A )
7	1 2 4	chnerlem2	|- ( ( ph /\ J e. ( 0 ..^ I ) ) -> ( C ` J ) .~ ( C ` I ) )
8	6 7	ersym	|- ( ( ph /\ J e. ( 0 ..^ I ) ) -> ( C ` I ) .~ ( C ` J ) )
9		fveq2	|- ( I = J -> ( C ` I ) = ( C ` J ) )
10	9	adantl	|- ( ( ph /\ I = J ) -> ( C ` I ) = ( C ` J ) )
11	1	adantr	|- ( ( ph /\ I = J ) -> .~ Er A )
12	2	chnwrd	|- ( ph -> C e. Word A )
13		wrdsymbcl	|- ( ( C e. Word A /\ J e. ( 0 ..^ ( # ` C ) ) ) -> ( C ` J ) e. A )
14	12 3 13	syl2anc	|- ( ph -> ( C ` J ) e. A )
15	14	adantr	|- ( ( ph /\ I = J ) -> ( C ` J ) e. A )
16	11 15	erref	|- ( ( ph /\ I = J ) -> ( C ` J ) .~ ( C ` J ) )
17	10 16	eqbrtrd	|- ( ( ph /\ I = J ) -> ( C ` I ) .~ ( C ` J ) )
18	1 2 3 4	chnerlem3	|- ( ph -> ( I e. ( 0 ..^ J ) \/ J e. ( 0 ..^ I ) \/ I = J ) )
19	5 8 17 18	mpjao3dan	|- ( ph -> ( C ` I ) .~ ( C ` J ) )