Metamath Proof Explorer

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 \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
	Assertion	isldsys	$⊢ S \in L \leftrightarrow (S \in 𝒫 𝒫 O \land (\emptyset \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in S)))$

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
2		eleq2	$⊢ s = S \to (\emptyset \in s \leftrightarrow \emptyset \in S)$
3		eleq2	$⊢ s = S \to (O ∖ x \in s \leftrightarrow O ∖ x \in S)$
4	3	raleqbi1dv	$⊢ s = S \to (\forall x \in s O ∖ x \in s \leftrightarrow \forall x \in S O ∖ x \in S)$
5		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
6		eleq2	$⊢ s = S \to (⋃ x \in s \leftrightarrow ⋃ x \in S)$
7	6	imbi2d	$⊢ s = S \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s) \leftrightarrow ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in S))$
8	5 7	raleqbidv	$⊢ s = S \to (\forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s) \leftrightarrow \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in S))$
9	2 4 8	3anbi123d	$⊢ s = S \to ((\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s)) \leftrightarrow (\emptyset \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in S)))$
10	9 1	elrab2	$⊢ S \in L \leftrightarrow (S \in 𝒫 𝒫 O \land (\emptyset \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in S)))$