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	⊢ ( 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) → ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝑅 ∩ < ) ⊆ 𝑅
2		chnrss	⊢ ( ( 𝑅 ∩ < ) ⊆ 𝑅 → ( ( 𝑅 ∩ < ) Chain 𝐵 ) ⊆ ( 𝑅 Chain 𝐵 ) )
3	1 2	ax-mp	⊢ ( ( 𝑅 ∩ < ) Chain 𝐵 ) ⊆ ( 𝑅 Chain 𝐵 )
4	3	sseli	⊢ ( 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) → 𝐴 ∈ ( 𝑅 Chain 𝐵 ) )
5		inss2	⊢ ( 𝑅 ∩ < ) ⊆ <
6		chnrss	⊢ ( ( 𝑅 ∩ < ) ⊆ < → ( ( 𝑅 ∩ < ) Chain 𝐵 ) ⊆ ( < Chain 𝐵 ) )
7	5 6	ax-mp	⊢ ( ( 𝑅 ∩ < ) Chain 𝐵 ) ⊆ ( < Chain 𝐵 )
8	7	sseli	⊢ ( 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) → 𝐴 ∈ ( < Chain 𝐵 ) )
9	4 8	jca	⊢ ( 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) → ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) )