Metamath Proof Explorer

Theorem 0elsros

Description: A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020)

		Ref	Expression
	Hypothesis	issros.1	\|- N = { s e. ~P ~P O \| ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
	Assertion	0elsros	\|- ( S e. N -> (/) e. S )

Proof

Step	Hyp	Ref	Expression
1		issros.1	\|- N = { s e. ~P ~P O \| ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
2	1	issros	\|- ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )
3	2	simp2bi	\|- ( S e. N -> (/) e. S )

Step

Hyp

Ref

Expression

issros.1

 |-  N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }

issros

 |-  ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )

simp2bi

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