Theorem chndin2

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

	Ref	Expression
Assertion	chndin2	$$⊢{\mathrm{Chain}}_{\left(B\cap C\right)}R={\mathrm{Chain}}_{B}R\cap {\mathrm{Chain}}_{C}R$$

Proof

Step	Hyp	Ref	Expression
1		chndrin	$$⊢n\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\to \left(n\in {\mathrm{Chain}}_{B}R\wedge n\in {\mathrm{Chain}}_{C}R\right)$$
2		chndin	$$⊢\left(n\in {\mathrm{Chain}}_{B}R\wedge n\in {\mathrm{Chain}}_{C}R\right)\to n\in {\mathrm{Chain}}_{\left(B\cap C\right)}R$$
3	1 2	impbii	$$⊢n\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\leftrightarrow \left(n\in {\mathrm{Chain}}_{B}R\wedge n\in {\mathrm{Chain}}_{C}R\right)$$
4		elin	$$⊢n\in \left({\mathrm{Chain}}_{B}R\cap {\mathrm{Chain}}_{C}R\right)\leftrightarrow \left(n\in {\mathrm{Chain}}_{B}R\wedge n\in {\mathrm{Chain}}_{C}R\right)$$
5	3 4	bitr4i	$$⊢n\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\leftrightarrow n\in \left({\mathrm{Chain}}_{B}R\cap {\mathrm{Chain}}_{C}R\right)$$
6	5	eqriv	$$⊢{\mathrm{Chain}}_{\left(B\cap C\right)}R={\mathrm{Chain}}_{B}R\cap {\mathrm{Chain}}_{C}R$$