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	|- ( ph -> A e. V )
Assertion	collexd	|- ( ph -> ( F Coll A ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		collexd.1	|- ( ph -> A e. V )
2		df-coll	|- ( F Coll A ) = U_ x e. A Scott ( F " { x } )
3		scottex2	|- Scott ( F " { x } ) e. _V
4	3	a1i	|- ( ph -> Scott ( F " { x } ) e. _V )
5	4	ralrimivw	|- ( ph -> A. x e. A Scott ( F " { x } ) e. _V )
6		iunexg	|- ( ( A e. V /\ A. x e. A Scott ( F " { x } ) e. _V ) -> U_ x e. A Scott ( F " { x } ) e. _V )
7	1 5 6	syl2anc	|- ( ph -> U_ x e. A Scott ( F " { x } ) e. _V )
8	2 7	eqeltrid	|- ( ph -> ( F Coll A ) e. _V )