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	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2	1 0	ccoll	⊢ ( 𝐹 Coll 𝐴 )
3		vx	⊢ 𝑥
4	3	cv	⊢ 𝑥
5	4	csn	⊢ { 𝑥 }
6	0 5	cima	⊢ ( 𝐹 “ { 𝑥 } )
7	6	cscott	⊢ Scott ( 𝐹 “ { 𝑥 } )
8	3 1 7	ciun	⊢ ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } )
9	2 8	wceq	⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } )