![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > isldsys | Structured version Visualization version GIF version |
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 |
---|---|
isldsys.l | ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} |
Ref | Expression |
---|---|
isldsys | ⊢ (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2818 | . . 3 ⊢ (𝑠 = 𝑆 → (∅ ∈ 𝑠 ↔ ∅ ∈ 𝑆)) | |
2 | eleq2 2818 | . . . 4 ⊢ (𝑠 = 𝑆 → ((𝑂 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑆)) | |
3 | 2 | raleqbi1dv 3330 | . . 3 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆)) |
4 | pweq 4617 | . . . 4 ⊢ (𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆) | |
5 | eleq2 2818 | . . . . 5 ⊢ (𝑠 = 𝑆 → (∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆)) | |
6 | 5 | imbi2d 340 | . . . 4 ⊢ (𝑠 = 𝑆 → (((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠) ↔ ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆))) |
7 | 4, 6 | raleqbidv 3339 | . . 3 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠) ↔ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆))) |
8 | 1, 3, 7 | 3anbi123d 1433 | . 2 ⊢ (𝑠 = 𝑆 → ((∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠)) ↔ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆)))) |
9 | isldsys.l | . 2 ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} | |
10 | 8, 9 | elrab2 3685 | 1 ⊢ (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ∀wral 3058 {crab 3429 ∖ cdif 3944 ∅c0 4323 𝒫 cpw 4603 ∪ cuni 4908 Disj wdisj 5113 class class class wbr 5148 ωcom 7870 ≼ cdom 8961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1087 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-in 3954 df-ss 3964 df-pw 4605 |
This theorem is referenced by: pwldsys 33776 unelldsys 33777 sigaldsys 33778 ldsysgenld 33779 sigapildsyslem 33780 sigapildsys 33781 ldgenpisyslem1 33782 |
Copyright terms: Public domain | W3C validator |