Definition df-salon 42686

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

Assertion

Ref	Expression
df-salon	⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})

Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-salon

Step	Hyp	Ref	Expression
1		csalon 42685	. 2 class SalOn
2		vx	. . 3 setvar 𝑥
3		cvv 3486	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1536	. . . . . 6 class 𝑠
6	5	cuni 4824	. . . . 5 class ∪ 𝑠
7	2	cv 1536	. . . . 5 class 𝑥
8	6, 7	wceq 1537	. . . 4 wff ∪ 𝑠 = 𝑥
9		csalg 42683	. . . 4 class SAlg
10	8, 4, 9	crab 3142	. . 3 class {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥}
11	2, 3, 10	cmpt 5132	. 2 class (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})
12	1, 11	wceq 1537	1 wff SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})

This definition is referenced by: (None)