0elsiga

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

		Ref	Expression
	Assertion	0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$

Step	Hyp	Ref	Expression
1		isrnsiga	$⊢ S \in ⋃ ran sigAlgebra \leftrightarrow (S \in V \land \exists o (S \subseteq 𝒫 o \land (o \in S \land \forall x \in S o ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
2	1	simprbi	$⊢ S \in ⋃ ran sigAlgebra \to \exists o (S \subseteq 𝒫 o \land (o \in S \land \forall x \in S o ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
3		3simpa	$⊢ (o \in S \land \forall x \in S o ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)) \to (o \in S \land \forall x \in S o ∖ x \in S)$
4	3	adantl	$⊢ (S \subseteq 𝒫 o \land (o \in S \land \forall x \in S o ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to (o \in S \land \forall x \in S o ∖ x \in S)$
5	4	eximi	$⊢ \exists o (S \subseteq 𝒫 o \land (o \in S \land \forall x \in S o ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to \exists o (o \in S \land \forall x \in S o ∖ x \in S)$
6		difeq2	$⊢ x = o \to o ∖ x = o ∖ o$
7		difid	$⊢ o ∖ o = \emptyset$
8	6 7	eqtrdi	$⊢ x = o \to o ∖ x = \emptyset$
9	8	eleq1d	$⊢ x = o \to (o ∖ x \in S \leftrightarrow \emptyset \in S)$
10	9	rspcva	$⊢ (o \in S \land \forall x \in S o ∖ x \in S) \to \emptyset \in S$
11	10	exlimiv	$⊢ \exists o (o \in S \land \forall x \in S o ∖ x \in S) \to \emptyset \in S$
12	2 5 11	3syl	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$

Metamath Proof Explorer