Definition df-coll

Description: Define the collection operation. This is similar to the image set operation " , but it uses Scott's trick to ensure the output is always a set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Assertion	df-coll	$$⊢\left(FCollA\right)=\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2	1 0	ccoll	$$class\left(FCollA\right)$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	4	csn	$$class\left\{x\right\}$$
6	0 5	cima	$$classF\left[\left\{x\right\}\right]$$
7	6	cscott	$$classScottF\left[\left\{x\right\}\right]$$
8	3 1 7	ciun	$$class\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$
9	2 8	wceq	$$wff\left(FCollA\right)=\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$