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

Proof

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