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	⊢ ( 𝐴 ∈ 𝑉 → ( < Chain 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		wrdexg	⊢ ( 𝐴 ∈ 𝑉 → Word 𝐴 ∈ V )
2		id	⊢ ( 𝑥 ∈ ( < Chain 𝐴 ) → 𝑥 ∈ ( < Chain 𝐴 ) )
3	2	chnwrd	⊢ ( 𝑥 ∈ ( < Chain 𝐴 ) → 𝑥 ∈ Word 𝐴 )
4	3	ssriv	⊢ ( < Chain 𝐴 ) ⊆ Word 𝐴
5	1 4	jctil	⊢ ( 𝐴 ∈ 𝑉 → ( ( < Chain 𝐴 ) ⊆ Word 𝐴 ∧ Word 𝐴 ∈ V ) )
6		ssexg	⊢ ( ( ( < Chain 𝐴 ) ⊆ Word 𝐴 ∧ Word 𝐴 ∈ V ) → ( < Chain 𝐴 ) ∈ V )
7	5 6	syl	⊢ ( 𝐴 ∈ 𝑉 → ( < Chain 𝐴 ) ∈ V )