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	|- ( ( A e. ( R Chain B ) \/ A e. ( R Chain C ) ) -> A e. ( R Chain ( B u. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- B C_ ( B u. C )
2		chndss	|- ( B C_ ( B u. C ) -> ( R Chain B ) C_ ( R Chain ( B u. C ) ) )
3	1 2	ax-mp	|- ( R Chain B ) C_ ( R Chain ( B u. C ) )
4	3	sseli	|- ( A e. ( R Chain B ) -> A e. ( R Chain ( B u. C ) ) )
5		ssun2	|- C C_ ( B u. C )
6		chndss	|- ( C C_ ( B u. C ) -> ( R Chain C ) C_ ( R Chain ( B u. C ) ) )
7	5 6	ax-mp	|- ( R Chain C ) C_ ( R Chain ( B u. C ) )
8	7	sseli	|- ( A e. ( R Chain C ) -> A e. ( R Chain ( B u. C ) ) )
9	4 8	jaoi	|- ( ( A e. ( R Chain B ) \/ A e. ( R Chain C ) ) -> A e. ( R Chain ( B u. C ) ) )