Theorem baselsiga

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

	Ref	Expression
Assertion	baselsiga	|- ( S e. ( sigAlgebra ` A ) -> A e. S )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( S e. ( sigAlgebra ` A ) -> S e. _V )
2		issiga	|- ( S e. _V -> ( S e. ( sigAlgebra ` A ) <-> ( S C_ ~P A /\ ( A e. S /\ A. x e. S ( A \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
3	2	simplbda	|- ( ( S e. _V /\ S e. ( sigAlgebra ` A ) ) -> ( A e. S /\ A. x e. S ( A \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
4	3	simp1d	|- ( ( S e. _V /\ S e. ( sigAlgebra ` A ) ) -> A e. S )
5	1 4	mpancom	|- ( S e. ( sigAlgebra ` A ) -> A e. S )