Theorem chndrin

Description: A chain whose alphabet is intersection of two classes is also a chain in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chndrin	|- ( A e. ( R Chain ( B i^i C ) ) -> ( A e. ( R Chain B ) /\ A e. ( R Chain C ) ) )

Proof

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