Definition df-salon

Description: Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	df-salon	$$⊢\mathrm{SalOn}=\left(x\in \mathrm{V}⟼\left\{s\in \mathrm{SAlg}|\bigcup s=x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalon	$$class\mathrm{SalOn}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		csalg	$$class\mathrm{SAlg}$$
5	3	cv	$$setvars$$
6	5	cuni	$$class\bigcup s$$
7	1	cv	$$setvarx$$
8	6 7	wceq	$$wff\bigcup s=x$$
9	8 3 4	crab	$$class\left\{s\in \mathrm{SAlg}|\bigcup s=x\right\}$$
10	1 2 9	cmpt	$$class\left(x\in \mathrm{V}⟼\left\{s\in \mathrm{SAlg}|\bigcup s=x\right\}\right)$$
11	0 10	wceq	$$wff\mathrm{SalOn}=\left(x\in \mathrm{V}⟼\left\{s\in \mathrm{SAlg}|\bigcup s=x\right\}\right)$$