Theorem chndrin

Description: A chain whose alphabet is intersection of two classes is also a chain in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chndrin	⊢ ( 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) → ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵
2		chndss	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵 → ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑅 Chain 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑅 Chain 𝐵 )
4	3	sseli	⊢ ( 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ ( 𝑅 Chain 𝐵 ) )
5		inss2	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶
6		chndss	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶 → ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑅 Chain 𝐶 ) )
7	5 6	ax-mp	⊢ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑅 Chain 𝐶 )
8	7	sseli	⊢ ( 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ ( 𝑅 Chain 𝐶 ) )
9	4 8	jca	⊢ ( 𝐴 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) → ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( 𝑅 Chain 𝐶 ) ) )