Theorem collexd

Description: The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	collexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	collexd	⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		collexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		df-coll	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } )
3		scottex2	⊢ Scott ( 𝐹 “ { 𝑥 } ) ∈ V
4	3	a1i	⊢ ( 𝜑 → Scott ( 𝐹 “ { 𝑥 } ) ∈ V )
5	4	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) ∈ V )
6		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) ∈ V )
7	1 5 6	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) ∈ V )
8	2 7	eqeltrid	⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) ∈ V )