Theorem chnrun2

Description: Superadditivity of chain constructor over relation parameter. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chnrun2	⊢ ( ( 𝑅 Chain 𝐵 ) ∪ ( < Chain 𝐵 ) ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∪ ( < Chain 𝐵 ) ) ↔ ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∨ 𝑛 ∈ ( < Chain 𝐵 ) ) )
2		chnrun	⊢ ( ( 𝑛 ∈ ( 𝑅 Chain 𝐵 ) ∨ 𝑛 ∈ ( < Chain 𝐵 ) ) → 𝑛 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
3	1 2	sylbi	⊢ ( 𝑛 ∈ ( ( 𝑅 Chain 𝐵 ) ∪ ( < Chain 𝐵 ) ) → 𝑛 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
4	3	ssriv	⊢ ( ( 𝑅 Chain 𝐵 ) ∪ ( < Chain 𝐵 ) ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 )