Theorem chnrin

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

	Ref	Expression
Assertion	chnrin	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ischn	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ↔ ( 𝐴 ∈ Word 𝐵 ∧ ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) ) )
2	1	simplbi	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → 𝐴 ∈ Word 𝐵 )
3	2	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → 𝐴 ∈ Word 𝐵 )
4	1	simprbi	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) )
6	5	r19.21bi	⊢ ( ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) ∧ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ) → ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) )
7		ischn	⊢ ( 𝐴 ∈ ( < Chain 𝐵 ) ↔ ( 𝐴 ∈ Word 𝐵 ∧ ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) < ( 𝐴 ‘ 𝑛 ) ) )
8	7	simprbi	⊢ ( 𝐴 ∈ ( < Chain 𝐵 ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) < ( 𝐴 ‘ 𝑛 ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) < ( 𝐴 ‘ 𝑛 ) )
10	9	r19.21bi	⊢ ( ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) ∧ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ) → ( 𝐴 ‘ ( 𝑛 − 1 ) ) < ( 𝐴 ‘ 𝑛 ) )
11		brin	⊢ ( ( 𝐴 ‘ ( 𝑛 − 1 ) ) ( 𝑅 ∩ < ) ( 𝐴 ‘ 𝑛 ) ↔ ( ( 𝐴 ‘ ( 𝑛 − 1 ) ) 𝑅 ( 𝐴 ‘ 𝑛 ) ∧ ( 𝐴 ‘ ( 𝑛 − 1 ) ) < ( 𝐴 ‘ 𝑛 ) ) )
12	6 10 11	sylanbrc	⊢ ( ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) ∧ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ) → ( 𝐴 ‘ ( 𝑛 − 1 ) ) ( 𝑅 ∩ < ) ( 𝐴 ‘ 𝑛 ) )
13	12	ralrimiva	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) ( 𝑅 ∩ < ) ( 𝐴 ‘ 𝑛 ) )
14		ischn	⊢ ( 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) ↔ ( 𝐴 ∈ Word 𝐵 ∧ ∀ 𝑛 ∈ ( dom 𝐴 ∖ { 0 } ) ( 𝐴 ‘ ( 𝑛 − 1 ) ) ( 𝑅 ∩ < ) ( 𝐴 ‘ 𝑛 ) ) )
15	3 13 14	sylanbrc	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝐴 ∈ ( < Chain 𝐵 ) ) → 𝐴 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) )