Definition df-siga

Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using S and O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016)

	Ref	Expression
Assertion	df-siga	⊢ sigAlgebra = ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csiga	⊢ sigAlgebra
1		vo	⊢ 𝑜
2		cvv	⊢ V
3		vs	⊢ 𝑠
4	3	cv	⊢ 𝑠
5	1	cv	⊢ 𝑜
6	5	cpw	⊢ 𝒫 𝑜
7	4 6	wss	⊢ 𝑠 ⊆ 𝒫 𝑜
8	5 4	wcel	⊢ 𝑜 ∈ 𝑠
9		vx	⊢ 𝑥
10	9	cv	⊢ 𝑥
11	5 10	cdif	⊢ ( 𝑜 ∖ 𝑥 )
12	11 4	wcel	⊢ ( 𝑜 ∖ 𝑥 ) ∈ 𝑠
13	12 9 4	wral	⊢ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠
14	4	cpw	⊢ 𝒫 𝑠
15		cdom	⊢ ≼
16		com	⊢ ω
17	10 16 15	wbr	⊢ 𝑥 ≼ ω
18	10	cuni	⊢ ∪ 𝑥
19	18 4	wcel	⊢ ∪ 𝑥 ∈ 𝑠
20	17 19	wi	⊢ ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 )
21	20 9 14	wral	⊢ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 )
22	8 13 21	w3a	⊢ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) )
23	7 22	wa	⊢ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) )
24	23 3	cab	⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) }
25	1 2 24	cmpt	⊢ ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
26	0 25	wceq	⊢ sigAlgebra = ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )