Theorem chndun2

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

	Ref	Expression
Assertion	chndun2	|- ( ( R Chain B ) u. ( R Chain C ) ) C_ ( R Chain ( B u. C ) )

Proof

Step	Hyp	Ref	Expression
1		elun	|- ( n e. ( ( R Chain B ) u. ( R Chain C ) ) <-> ( n e. ( R Chain B ) \/ n e. ( R Chain C ) ) )
2		chndun	|- ( ( n e. ( R Chain B ) \/ n e. ( R Chain C ) ) -> n e. ( R Chain ( B u. C ) ) )
3	1 2	sylbi	|- ( n e. ( ( R Chain B ) u. ( R Chain C ) ) -> n e. ( R Chain ( B u. C ) ) )
4	3	ssriv	|- ( ( R Chain B ) u. ( R Chain C ) ) C_ ( R Chain ( B u. C ) )