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	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
Assertion	isldsys	⊢ ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
2		eleq2	⊢ ( 𝑠 = 𝑆 → ( ∅ ∈ 𝑠 ↔ ∅ ∈ 𝑆 ) )
3		eleq2	⊢ ( 𝑠 = 𝑆 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
4	3	raleqbi1dv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
5		pweq	⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
6		eleq2	⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆 ) )
7	6	imbi2d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑆 ) ) )
8	5 7	raleqbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑆 ) ) )
9	2 4 8	3anbi123d	⊢ ( 𝑠 = 𝑆 → ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑆 ) ) ) )
10	9 1	elrab2	⊢ ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑆 ) ) ) )