Theorem chndin2

Description: Distribution of chain class constructor over alphabet intersection. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chndin2	⊢ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝑅 Chain 𝐵 ) ∩ ( 𝑅 Chain 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		chndrin	⊢ ( 𝑛 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) → ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( 𝑅 Chain 𝐶 ) ) )
2		chndin	⊢ ( ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( 𝑅 Chain 𝐶 ) ) → 𝑛 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) )
3	1 2	impbii	⊢ ( 𝑛 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( 𝑅 Chain 𝐶 ) ) )
4		elin	⊢ ( 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∩ ( 𝑅 Chain 𝐶 ) ) ↔ ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( 𝑅 Chain 𝐶 ) ) )
5	3 4	bitr4i	⊢ ( 𝑛 ∈ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) ↔ 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∩ ( 𝑅 Chain 𝐶 ) ) )
6	5	eqriv	⊢ ( 𝑅 Chain ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝑅 Chain 𝐵 ) ∩ ( 𝑅 Chain 𝐶 ) )