Metamath Proof Explorer

Theorem ischn

Description: Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Assertion ischn ⊢ C ∈ Chain A < ˙ ↔ C ∈ Word A ∧ ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n

Proof

Step Hyp Ref Expression
1 dmeq ⊢ c = C → dom ⁡ c = dom ⁡ C
2 1 difeq1d ⊢ c = C → dom ⁡ c ∖ 0 = dom ⁡ C ∖ 0
3 fveq1 ⊢ c = C → c ⁡ n − 1 = C ⁡ n − 1
4 fveq1 ⊢ c = C → c ⁡ n = C ⁡ n
5 3 4 breq12d ⊢ c = C → c ⁡ n − 1 < ˙ c ⁡ n ↔ C ⁡ n − 1 < ˙ C ⁡ n
6 2 5 raleqbidv ⊢ c = C → ∀ n ∈ dom ⁡ c ∖ 0 c ⁡ n − 1 < ˙ c ⁡ n ↔ ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n
7 df-chn ⊢ Chain A < ˙ = c ∈ Word A | ∀ n ∈ dom ⁡ c ∖ 0 c ⁡ n − 1 < ˙ c ⁡ n
8 6 7 elrab2 ⊢ C ∈ Chain A < ˙ ↔ C ∈ Word A ∧ ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n