Theorem chndun

Description: Chains in either of two alphabets are chains in their union. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chndun	$$⊢\left(A\in {\mathrm{Chain}}_{B}R\vee A\in {\mathrm{Chain}}_{C}R\right)\to A\in {\mathrm{Chain}}_{\left(B\cup C\right)}R$$

Proof

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