Theorem chnrun2

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

	Ref	Expression
Assertion	chnrun2	|- ( ( R Chain B ) u. ( .< Chain B ) ) C_ ( ( R u. .< ) Chain B )

Proof

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