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	⊢ ( 𝜑 → ∼ Er 𝐴 )
	chner.2	⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
	chner.3	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
	chner.4	⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
Assertion	chner	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		chner.1	⊢ ( 𝜑 → ∼ Er 𝐴 )
2		chner.2	⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
3		chner.3	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
4		chner.4	⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
5	1 2 3	chnerlem2	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 0 ..^ 𝐽 ) ) → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝐼 ) ) → ∼ Er 𝐴 )
7	1 2 4	chnerlem2	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝐼 ) ) → ( 𝐶 ‘ 𝐽 ) ∼ ( 𝐶 ‘ 𝐼 ) )
8	6 7	ersym	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝐼 ) ) → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )
9		fveq2	⊢ ( 𝐼 = 𝐽 → ( 𝐶 ‘ 𝐼 ) = ( 𝐶 ‘ 𝐽 ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐶 ‘ 𝐼 ) = ( 𝐶 ‘ 𝐽 ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ∼ Er 𝐴 )
12	2	chnwrd	⊢ ( 𝜑 → 𝐶 ∈ Word 𝐴 )
13		wrdsymbcl	⊢ ( ( 𝐶 ∈ Word 𝐴 ∧ 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) → ( 𝐶 ‘ 𝐽 ) ∈ 𝐴 )
14	12 3 13	syl2anc	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐽 ) ∈ 𝐴 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐶 ‘ 𝐽 ) ∈ 𝐴 )
16	11 15	erref	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐶 ‘ 𝐽 ) ∼ ( 𝐶 ‘ 𝐽 ) )
17	10 16	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐼 = 𝐽 ) → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )
18	1 2 3 4	chnerlem3	⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝐽 ) ∨ 𝐽 ∈ ( 0 ..^ 𝐼 ) ∨ 𝐼 = 𝐽 ) )
19	5 8 17 18	mpjao3dan	⊢ ( 𝜑 → ( 𝐶 ‘ 𝐼 ) ∼ ( 𝐶 ‘ 𝐽 ) )