Metamath Proof Explorer

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 A
chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
chner.3 ⊢ φ → J ∈ 0 ..^ C
chner.4 ⊢ φ → I ∈ 0 ..^ C
Assertion chner ⊢ φ → C ⁡ I ∼ ˙ C ⁡ J

Proof

Step Hyp Ref Expression
1 chner.1 ⊢ φ → ∼ ˙ Er A
2 chner.2 ⊢ φ → C ∈ Chain A ∼ ˙
3 chner.3 ⊢ φ → J ∈ 0 ..^ C
4 chner.4 ⊢ φ → I ∈ 0 ..^ C
5 1 2 3 chnerlem2 ⊢ φ ∧ I ∈ 0 ..^ J → C ⁡ I ∼ ˙ C ⁡ J
6 1 adantr ⊢ φ ∧ J ∈ 0 ..^ I → ∼ ˙ Er A
7 1 2 4 chnerlem2 ⊢ φ ∧ J ∈ 0 ..^ I → C ⁡ J ∼ ˙ C ⁡ I
8 6 7 ersym ⊢ φ ∧ J ∈ 0 ..^ I → C ⁡ I ∼ ˙ C ⁡ J
9 fveq2 ⊢ I = J → C ⁡ I = C ⁡ J
10 9 adantl ⊢ φ ∧ I = J → C ⁡ I = C ⁡ J
11 1 adantr ⊢ φ ∧ I = J → ∼ ˙ Er A
12 2 chnwrd ⊢ φ → C ∈ Word A
13 wrdsymbcl ⊢ C ∈ Word A ∧ J ∈ 0 ..^ C → C ⁡ J ∈ A
14 12 3 13 syl2anc ⊢ φ → C ⁡ J ∈ A
15 14 adantr ⊢ φ ∧ I = J → C ⁡ J ∈ A
16 11 15 erref ⊢ φ ∧ I = J → C ⁡ J ∼ ˙ C ⁡ J
17 10 16 eqbrtrd ⊢ φ ∧ I = J → C ⁡ I ∼ ˙ C ⁡ J
18 1 2 3 4 chnerlem3 ⊢ φ → I ∈ 0 ..^ J ∨ J ∈ 0 ..^ I ∨ I = J
19 5 8 17 18 mpjao3dan ⊢ φ → C ⁡ I ∼ ˙ C ⁡ J