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	$$⊢A\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\to \left(A\in {\mathrm{Chain}}_{B}R\wedge A\in {\mathrm{Chain}}_{C}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢B\cap C\subseteq B$$
2		chndss	$$⊢B\cap C\subseteq B\to {\mathrm{Chain}}_{\left(B\cap C\right)}R\subseteq {\mathrm{Chain}}_{B}R$$
3	1 2	ax-mp	$$⊢{\mathrm{Chain}}_{\left(B\cap C\right)}R\subseteq {\mathrm{Chain}}_{B}R$$
4	3	sseli	$$⊢A\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\to A\in {\mathrm{Chain}}_{B}R$$
5		inss2	$$⊢B\cap C\subseteq C$$
6		chndss	$$⊢B\cap C\subseteq C\to {\mathrm{Chain}}_{\left(B\cap C\right)}R\subseteq {\mathrm{Chain}}_{C}R$$
7	5 6	ax-mp	$$⊢{\mathrm{Chain}}_{\left(B\cap C\right)}R\subseteq {\mathrm{Chain}}_{C}R$$
8	7	sseli	$$⊢A\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\to A\in {\mathrm{Chain}}_{C}R$$
9	4 8	jca	$$⊢A\in {\mathrm{Chain}}_{\left(B\cap C\right)}R\to \left(A\in {\mathrm{Chain}}_{B}R\wedge A\in {\mathrm{Chain}}_{C}R\right)$$