Theorem pwldsys

Description: The power set of the universe set O is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Hypothesis	isldsys.l	|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
Assertion	pwldsys	|- ( O e. V -> ~P O e. L )

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
2		pwexg	|- ( O e. V -> ~P O e. _V )
3		pwidg	|- ( ~P O e. _V -> ~P O e. ~P ~P O )
4	2 3	syl	|- ( O e. V -> ~P O e. ~P ~P O )
5		0elpw	|- (/) e. ~P O
6	5	a1i	|- ( O e. V -> (/) e. ~P O )
7		pwidg	|- ( O e. V -> O e. ~P O )
8	7	adantr	|- ( ( O e. V /\ x e. ~P O ) -> O e. ~P O )
9	8	elpwdifcl	|- ( ( O e. V /\ x e. ~P O ) -> ( O \ x ) e. ~P O )
10	9	ralrimiva	|- ( O e. V -> A. x e. ~P O ( O \ x ) e. ~P O )
11		elpwi	|- ( x e. ~P ~P O -> x C_ ~P O )
12		sspwuni	|- ( x C_ ~P O <-> U. x C_ O )
13	11 12	sylib	|- ( x e. ~P ~P O -> U. x C_ O )
14	13	adantl	|- ( ( O e. V /\ x e. ~P ~P O ) -> U. x C_ O )
15		vuniex	|- U. x e. _V
16	15	elpw	|- ( U. x e. ~P O <-> U. x C_ O )
17	14 16	sylibr	|- ( ( O e. V /\ x e. ~P ~P O ) -> U. x e. ~P O )
18	17	a1d	|- ( ( O e. V /\ x e. ~P ~P O ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. ~P O ) )
19	18	ralrimiva	|- ( O e. V -> A. x e. ~P ~P O ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. ~P O ) )
20	6 10 19	3jca	|- ( O e. V -> ( (/) e. ~P O /\ A. x e. ~P O ( O \ x ) e. ~P O /\ A. x e. ~P ~P O ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. ~P O ) ) )
21	1	isldsys	|- ( ~P O e. L <-> ( ~P O e. ~P ~P O /\ ( (/) e. ~P O /\ A. x e. ~P O ( O \ x ) e. ~P O /\ A. x e. ~P ~P O ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. ~P O ) ) ) )
22	4 20 21	sylanbrc	|- ( O e. V -> ~P O e. L )