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\in V\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		wrdexg	$$⊢A\in V\to \mathrm{Word}A\in \mathrm{V}$$
2		id	$$⊢x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}$$
3	2	chnwrd	$$⊢x\in {\mathrm{Chain}}_A\underset{\dot{}}{<}\to x\in \mathrm{Word}A$$
4	3	ssriv	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq \mathrm{Word}A$$
5	1 4	jctil	$$⊢A\in V\to \left({\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq \mathrm{Word}A\wedge \mathrm{Word}A\in \mathrm{V}\right)$$
6		ssexg	$$⊢\left({\mathrm{Chain}}_A\underset{\dot{}}{<}\subseteq \mathrm{Word}A\wedge \mathrm{Word}A\in \mathrm{V}\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{V}$$
7	5 6	syl	$$⊢A\in V\to {\mathrm{Chain}}_A\underset{\dot{}}{<}\in \mathrm{V}$$