Theorem chnexg

Description: Chains with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024) (Revised by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	chnexg	|- ( A e. V -> ( .< Chain A ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		wrdexg	|- ( A e. V -> Word A e. _V )
2		id	|- ( x e. ( .< Chain A ) -> x e. ( .< Chain A ) )
3	2	chnwrd	|- ( x e. ( .< Chain A ) -> x e. Word A )
4	3	ssriv	|- ( .< Chain A ) C_ Word A
5	1 4	jctil	|- ( A e. V -> ( ( .< Chain A ) C_ Word A /\ Word A e. _V ) )
6		ssexg	|- ( ( ( .< Chain A ) C_ Word A /\ Word A e. _V ) -> ( .< Chain A ) e. _V )
7	5 6	syl	|- ( A e. V -> ( .< Chain A ) e. _V )