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	⊢ SalOn = ( 𝑥 ∈ V ↦ { 𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csalon	⊢ SalOn
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		csalg	⊢ SAlg
5	3	cv	⊢ 𝑠
6	5	cuni	⊢ ∪ 𝑠
7	1	cv	⊢ 𝑥
8	6 7	wceq	⊢ ∪ 𝑠 = 𝑥
9	8 3 4	crab	⊢ { 𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥 }
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥 } )
11	0 10	wceq	⊢ SalOn = ( 𝑥 ∈ V ↦ { 𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥 } )