baselsiga

Description: A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016)

		Ref	Expression
	Assertion	baselsiga	$⊢ S \in sigAlgebra (A) \to A \in S$

Step	Hyp	Ref	Expression
1		elex	$⊢ S \in sigAlgebra (A) \to S \in V$
2		issiga	$⊢ S \in V \to (S \in sigAlgebra (A) \leftrightarrow (S \subseteq 𝒫 A \land (A \in S \land \forall x \in S A ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
3	2	simplbda	$⊢ (S \in V \land S \in sigAlgebra (A)) \to (A \in S \land \forall x \in S A ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
4	3	simp1d	$⊢ (S \in V \land S \in sigAlgebra (A)) \to A \in S$
5	1 4	mpancom	$⊢ S \in sigAlgebra (A) \to A \in S$

Metamath Proof Explorer