sigasspw

Description: A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017)

		Ref	Expression
	Assertion	sigasspw	$⊢ S \in sigAlgebra (A) \to S \subseteq 𝒫 A$

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	biimpa	$⊢ (S \in V \land S \in sigAlgebra (A)) \to (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)))$
4	1 3	mpancom	$⊢ S \in sigAlgebra (A) \to (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)))$
5	4	simpld	$⊢ S \in sigAlgebra (A) \to S \subseteq 𝒫 A$

Metamath Proof Explorer