Metamath Proof Explorer

Theorem chnltm1

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

Ref Expression
Hypotheses chnwrd.1 ⊢ φ → C ∈ Chain A < ˙
chnltm1.2 ⊢ φ → N ∈ dom ⁡ C ∖ 0
Assertion chnltm1 ⊢ φ → C ⁡ N − 1 < ˙ C ⁡ N

Proof

Step Hyp Ref Expression
1 chnwrd.1 ⊢ φ → C ∈ Chain A < ˙
2 chnltm1.2 ⊢ φ → N ∈ dom ⁡ C ∖ 0
3 fvoveq1 ⊢ n = N → C ⁡ n − 1 = C ⁡ N − 1
4 fveq2 ⊢ n = N → C ⁡ n = C ⁡ N
5 3 4 breq12d ⊢ n = N → C ⁡ n − 1 < ˙ C ⁡ n ↔ C ⁡ N − 1 < ˙ C ⁡ N
6 ischn ⊢ C ∈ Chain A < ˙ ↔ C ∈ Word A ∧ ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n
7 1 6 sylib ⊢ φ → C ∈ Word A ∧ ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n
8 7 simprd ⊢ φ → ∀ n ∈ dom ⁡ C ∖ 0 C ⁡ n − 1 < ˙ C ⁡ n
9 5 8 2 rspcdva ⊢ φ → C ⁡ N − 1 < ˙ C ⁡ N