Metamath Proof Explorer

Theorem chndin

Description: A chain in two alphabets at once is also a chain in their intersection. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion chndin ⊢ A ∈ Chain B R ∧ A ∈ Chain C R → A ∈ Chain B ∩ C R

Proof

Step Hyp Ref Expression
1 id ⊢ A ∈ Chain B R → A ∈ Chain B R
2 1 chnwrd ⊢ A ∈ Chain B R → A ∈ Word B
3 id ⊢ A ∈ Chain C R → A ∈ Chain C R
4 3 chnwrd ⊢ A ∈ Chain C R → A ∈ Word C
5 wrddin ⊢ A ∈ Word B ∧ A ∈ Word C → A ∈ Word B ∩ C
6 2 4 5 syl2an ⊢ A ∈ Chain B R ∧ A ∈ Chain C R → A ∈ Word B ∩ C
7 ischn ⊢ A ∈ Chain B R ↔ A ∈ Word B ∧ ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
8 7 simprbi ⊢ A ∈ Chain B R → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
9 8 adantr ⊢ A ∈ Chain B R ∧ A ∈ Chain C R → ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
10 ischn ⊢ A ∈ Chain B ∩ C R ↔ A ∈ Word B ∩ C ∧ ∀ n ∈ dom ⁡ A ∖ 0 A ⁡ n − 1 R A ⁡ n
11 6 9 10 sylanbrc ⊢ A ∈ Chain B R ∧ A ∈ Chain C R → A ∈ Chain B ∩ C R