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

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( R i^i .< ) C_ R
2		chnrss	|- ( ( R i^i .< ) C_ R -> ( ( R i^i .< ) Chain B ) C_ ( R Chain B ) )
3	1 2	ax-mp	|- ( ( R i^i .< ) Chain B ) C_ ( R Chain B )
4	3	sseli	|- ( A e. ( ( R i^i .< ) Chain B ) -> A e. ( R Chain B ) )
5		inss2	|- ( R i^i .< ) C_ .<
6		chnrss	|- ( ( R i^i .< ) C_ .< -> ( ( R i^i .< ) Chain B ) C_ ( .< Chain B ) )
7	5 6	ax-mp	|- ( ( R i^i .< ) Chain B ) C_ ( .< Chain B )
8	7	sseli	|- ( A e. ( ( R i^i .< ) Chain B ) -> A e. ( .< Chain B ) )
9	4 8	jca	|- ( A e. ( ( R i^i .< ) Chain B ) -> ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) )