Theorem dfcoll2

Description: Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Assertion	dfcoll2	$$⊢\left(FCollA\right)=\bigcup _{x\in A}Scott\left\{y|xFy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-coll	$$⊢\left(FCollA\right)=\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]$$
2		imasng	$$⊢x\in A\to F\left[\left\{x\right\}\right]=\left\{y|xFy\right\}$$
3	2	scotteqd	$$⊢x\in A\to ScottF\left[\left\{x\right\}\right]=Scott\left\{y|xFy\right\}$$
4	3	iuneq2i	$$⊢\bigcup _{x\in A}ScottF\left[\left\{x\right\}\right]=\bigcup _{x\in A}Scott\left\{y|xFy\right\}$$
5	1 4	eqtri	$$⊢\left(FCollA\right)=\bigcup _{x\in A}Scott\left\{y|xFy\right\}$$