Theorem chndun2

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

	Ref	Expression
Assertion	chndun2	⊢ ( ( 𝑅 Chain 𝐵 ) ∪ ( 𝑅 Chain 𝐶 ) ) ⊆ ( 𝑅 Chain ( 𝐵 ∪ 𝐶 ) )

Proof

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