Metamath Proof Explorer

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 ∈ Word A | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x = c ∈ Word B | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x
3 1 2 syl ⊢ A = B → c ∈ Word A | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x = c ∈ Word B | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x
4 df-chn ⊢ Chain A < ˙ = c ∈ Word A | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x
5 df-chn ⊢ Chain B < ˙ = c ∈ Word B | ∀ x ∈ dom ⁡ c ∖ 0 c ⁡ x − 1 < ˙ c ⁡ x
6 3 4 5 3eqtr4g ⊢ A = B → Chain A < ˙ = Chain B < ˙