Metamath Proof Explorer


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 → ∅ ∈ 𝑆 )