Theorem chnrun

Description: Satisfying either of two chain relations is sufficient to make a chain under their union. (Contributed by Ender Ting, 24-Jul-2026)

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

Proof

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