Theorem chnrin2

Description: Distribution of chain class constructor over relation intersection. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chnrin2	⊢ ( ( 𝑅 ∩ < ) Chain 𝐵 ) = ( ( 𝑅 Chain 𝐵 ) ∩ ( < Chain 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		chnrrin	⊢ ( 𝑛 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) → ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( < Chain 𝐵 ) ) )
2		chnrin	⊢ ( ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( < Chain 𝐵 ) ) → 𝑛 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) )
3	1 2	impbii	⊢ ( 𝑛 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) ↔ ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( < Chain 𝐵 ) ) )
4		elin	⊢ ( 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∩ ( < Chain 𝐵 ) ) ↔ ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∧ 𝑛 ∈ ( < Chain 𝐵 ) ) )
5	3 4	bitr4i	⊢ ( 𝑛 ∈ ( ( 𝑅 ∩ < ) Chain 𝐵 ) ↔ 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∩ ( < Chain 𝐵 ) ) )
6	5	eqriv	⊢ ( ( 𝑅 ∩ < ) Chain 𝐵 ) = ( ( 𝑅 Chain 𝐵 ) ∩ ( < Chain 𝐵 ) )