Theorem 0elsiga

Description: A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016)

	Ref	Expression
Assertion	0elsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		isrnsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
2	1	simprbi	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
3		3simpa	⊢ ( ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) → ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) )
4	3	adantl	⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) )
5	4	eximi	⊢ ( ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ∃ 𝑜 ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) )
6		difeq2	⊢ ( 𝑥 = 𝑜 → ( 𝑜 ∖ 𝑥 ) = ( 𝑜 ∖ 𝑜 ) )
7		difid	⊢ ( 𝑜 ∖ 𝑜 ) = ∅
8	6 7	eqtrdi	⊢ ( 𝑥 = 𝑜 → ( 𝑜 ∖ 𝑥 ) = ∅ )
9	8	eleq1d	⊢ ( 𝑥 = 𝑜 → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ↔ ∅ ∈ 𝑆 ) )
10	9	rspcva	⊢ ( ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) → ∅ ∈ 𝑆 )
11	10	exlimiv	⊢ ( ∃ 𝑜 ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) → ∅ ∈ 𝑆 )
12	2 5 11	3syl	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )