Theorem pwsal

Description: The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwsal	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		0elpw	⊢ ∅ ∈ 𝒫 𝑋
2	1	a1i	⊢ ( 𝑋 ∈ 𝑉 → ∅ ∈ 𝒫 𝑋 )
3		unipw	⊢ ∪ 𝒫 𝑋 = 𝑋
4	3	difeq1i	⊢ ( ∪ 𝒫 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑦 )
5	4	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( ∪ 𝒫 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑦 ) )
6		difssd	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋 )
7		difexg	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ 𝑦 ) ∈ V )
8		elpwg	⊢ ( ( 𝑋 ∖ 𝑦 ) ∈ V → ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋 ) )
9	7 8	syl	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑋 ) )
10	6 9	mpbird	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
11	5 10	eqeltrd	⊢ ( 𝑋 ∈ 𝑉 → ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
12	11	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
13	12	ralrimiva	⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑦 ∈ 𝒫 𝑋 ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 )
14		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → 𝑦 ⊆ 𝒫 𝑋 )
15	14	unissd	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → ∪ 𝑦 ⊆ ∪ 𝒫 𝑋 )
16	15 3	sseqtrdi	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → ∪ 𝑦 ⊆ 𝑋 )
17		vuniex	⊢ ∪ 𝑦 ∈ V
18	17	a1i	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → ∪ 𝑦 ∈ V )
19		elpwg	⊢ ( ∪ 𝑦 ∈ V → ( ∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 ) )
20	18 19	syl	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → ( ∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋 ) )
21	16 20	mpbird	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → ∪ 𝑦 ∈ 𝒫 𝑋 )
22	21	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) → ∪ 𝑦 ∈ 𝒫 𝑋 )
23	22	a1d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) → ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝒫 𝑋 ) )
24	23	ralrimiva	⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝒫 𝑋 ) )
25	2 13 24	3jca	⊢ ( 𝑋 ∈ 𝑉 → ( ∅ ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝒫 𝑋 ) ) )
26		pwexg	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V )
27		issal	⊢ ( 𝒫 𝑋 ∈ V → ( 𝒫 𝑋 ∈ SAlg ↔ ( ∅ ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝒫 𝑋 ) ) ) )
28	26 27	syl	⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ SAlg ↔ ( ∅ ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ( ∪ 𝒫 𝑋 ∖ 𝑦 ) ∈ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ 𝒫 𝑋 ) ) ) )
29	25 28	mpbird	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg )