Metamath Proof Explorer

Theorem 0sal

Description: The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	0sal	\|- ( S e. SAlg -> (/) e. S )

Step	Hyp	Ref	Expression
1		issal	\|- ( S e. SAlg -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
2	1	ibi	\|- ( S e. SAlg -> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
3	2	simp1d	\|- ( S e. SAlg -> (/) e. S )

Step

Hyp

Ref

Expression

 |-  ( S e. SAlg -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )

 |-  ( S e. SAlg -> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )

 |-  ( S e. SAlg -> (/) e. S )