Theorem chnrin

Description: Satisfying two chain relations makes a chain under their intersection. (Contributed by Ender Ting, 24-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ischn	|- ( A e. ( R Chain B ) <-> ( A e. Word B /\ A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) ) )
2	1	simplbi	|- ( A e. ( R Chain B ) -> A e. Word B )
3	2	adantr	|- ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) -> A e. Word B )
4	1	simprbi	|- ( A e. ( R Chain B ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) )
5	4	adantr	|- ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) R ( A ` n ) )
6	5	r19.21bi	|- ( ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) /\ n e. ( dom A \ { 0 } ) ) -> ( A ` ( n - 1 ) ) R ( A ` n ) )
7		ischn	|- ( A e. ( .< Chain B ) <-> ( A e. Word B /\ A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) .< ( A ` n ) ) )
8	7	simprbi	|- ( A e. ( .< Chain B ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) .< ( A ` n ) )
9	8	adantl	|- ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) .< ( A ` n ) )
10	9	r19.21bi	|- ( ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) /\ n e. ( dom A \ { 0 } ) ) -> ( A ` ( n - 1 ) ) .< ( A ` n ) )
11		brin	|- ( ( A ` ( n - 1 ) ) ( R i^i .< ) ( A ` n ) <-> ( ( A ` ( n - 1 ) ) R ( A ` n ) /\ ( A ` ( n - 1 ) ) .< ( A ` n ) ) )
12	6 10 11	sylanbrc	|- ( ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) /\ n e. ( dom A \ { 0 } ) ) -> ( A ` ( n - 1 ) ) ( R i^i .< ) ( A ` n ) )
13	12	ralrimiva	|- ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) -> A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) ( R i^i .< ) ( A ` n ) )
14		ischn	|- ( A e. ( ( R i^i .< ) Chain B ) <-> ( A e. Word B /\ A. n e. ( dom A \ { 0 } ) ( A ` ( n - 1 ) ) ( R i^i .< ) ( A ` n ) ) )
15	3 13 14	sylanbrc	|- ( ( A e. ( R Chain B ) /\ A e. ( .< Chain B ) ) -> A e. ( ( R i^i .< ) Chain B ) )