Theorem salgenn0

Description: The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	salgenn0	|- ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( X e. V -> U. X e. _V )
2		pwsal	|- ( U. X e. _V -> ~P U. X e. SAlg )
3	1 2	syl	|- ( X e. V -> ~P U. X e. SAlg )
4		unipw	|- U. ~P U. X = U. X
5	4	a1i	|- ( X e. V -> U. ~P U. X = U. X )
6		pwuni	|- X C_ ~P U. X
7	6	a1i	|- ( X e. V -> X C_ ~P U. X )
8	5 7	jca	|- ( X e. V -> ( U. ~P U. X = U. X /\ X C_ ~P U. X ) )
9	3 8	jca	|- ( X e. V -> ( ~P U. X e. SAlg /\ ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
10		unieq	|- ( s = ~P U. X -> U. s = U. ~P U. X )
11	10	eqeq1d	|- ( s = ~P U. X -> ( U. s = U. X <-> U. ~P U. X = U. X ) )
12		sseq2	|- ( s = ~P U. X -> ( X C_ s <-> X C_ ~P U. X ) )
13	11 12	anbi12d	|- ( s = ~P U. X -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
14	13	elrab	|- ( ~P U. X e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( ~P U. X e. SAlg /\ ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
15	9 14	sylibr	|- ( X e. V -> ~P U. X e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
16	15	ne0d	|- ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )