Metamath Proof Explorer

Theorem chnrin

Description: Satisfying two chain relations makes a chain under their intersection. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion chnrin ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → A ∈ Chain B R ∩ < ˙

Proof

Step Hyp Ref Expression
1 ischn ⊢ A ∈ Chain B R ↔ A ∈ Word B ∧ ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
2 1 simplbi ⊢ A ∈ Chain B R → A ∈ Word B
3 2 adantr ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → A ∈ Word B
4 1 simprbi ⊢ A ∈ Chain B R → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
5 4 adantr ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
6 5 r19.21bi ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ ∧ n ∈ dom ⁡ A ∖ 0 → A ⁡ n − 1 R A ⁡ n
7 ischn ⊢ A ∈ Chain B < ˙ ↔ A ∈ Word B ∧ ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 < ˙ A ⁡ n
8 7 simprbi ⊢ A ∈ Chain B < ˙ → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 < ˙ A ⁡ n
9 8 adantl ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 < ˙ A ⁡ n
10 9 r19.21bi ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ ∧ n ∈ dom ⁡ A ∖ 0 → A ⁡ n − 1 < ˙ A ⁡ n
11 brin ⊢ A ⁡ n − 1 R ∩ < ˙ A ⁡ n ↔ A ⁡ n − 1 R A ⁡ n ∧ A ⁡ n − 1 < ˙ A ⁡ n
12 6 10 11 sylanbrc ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ ∧ n ∈ dom ⁡ A ∖ 0 → A ⁡ n − 1 R ∩ < ˙ A ⁡ n
13 12 ralrimiva ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R ∩ < ˙ A ⁡ n
14 ischn ⊢ A ∈ Chain B R ∩ < ˙ ↔ A ∈ Word B ∧ ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R ∩ < ˙ A ⁡ n
15 3 13 14 sylanbrc ⊢ A ∈ Chain B R ∧ A ∈ Chain B < ˙ → A ∈ Chain B R ∩ < ˙