Theorem chnrrin

Description: A chain of elements satisfying two relations at once is a chain under either of them. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chnrrin	$$⊢A\in {\mathrm{Chain}}_B\left(R\cap \underset{\dot{}}{<}\right)\to \left(A\in {\mathrm{Chain}}_{B}R\wedge A\in {\mathrm{Chain}}_B\underset{\dot{}}{<}\right)$$

Proof

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