Theorem isldsys

Description: The property of being a lambda-system or Dynkin system. Lambda-systems contain the empty set, are closed under complement, and closed under countable disjoint union. (Contributed by Thierry Arnoux, 13-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	isldsys	|- ( S e. 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 ) ) ) )

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		eleq2	|- ( s = S -> ( (/) e. s <-> (/) e. S ) )
3		eleq2	|- ( s = S -> ( ( O \ x ) e. s <-> ( O \ x ) e. S ) )
4	3	raleqbi1dv	|- ( s = S -> ( A. x e. s ( O \ x ) e. s <-> A. x e. S ( O \ x ) e. S ) )
5		pweq	|- ( s = S -> ~P s = ~P S )
6		eleq2	|- ( s = S -> ( U. x e. s <-> U. x e. S ) )
7	6	imbi2d	|- ( s = S -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) <-> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. S ) ) )
8	5 7	raleqbidv	|- ( s = S -> ( A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) <-> A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. S ) ) )
9	2 4 8	3anbi123d	|- ( s = S -> ( ( (/) 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 ) ) <-> ( (/) 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 ) ) ) )
10	9 1	elrab2	|- ( S e. 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 ) ) ) )