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	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) → 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → 𝐴 ∈ ( 𝑅 Chain 𝐵 ) )
2	1	chnwrd	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → 𝐴 ∈ Word 𝐵 )
3		id	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐶 ) → 𝐴 ∈ ( 𝑅 Chain 𝐶 ) )
4	3	chnwrd	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐶 ) → 𝐴 ∈ Word 𝐶 )
5		wrddin	⊢ ( ( 𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶 ) → 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) )
6	2 4 5	syl2an	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) → 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) )
7		ischn	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ↔ ( 𝐴 ∈ Word 𝐵 ∧ ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) ) )
8	7	simprbi	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) )
10		ischn	⊢ ( 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝐴 ∈ Word ( 𝐵 ∩ 𝐶 ) ∧ ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) ) )
11	6 9 10	sylanbrc	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) → 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) )