Proof of Theorem pwldsys
Step | Hyp | Ref
| Expression |
1 | | pwexg 5077 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) |
2 | | pwidg 4392 |
. . . 4
⊢
(𝒫 𝑂 ∈
V → 𝒫 𝑂 ∈
𝒫 𝒫 𝑂) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝒫 𝒫 𝑂) |
4 | | 0elpw 5055 |
. . . . 5
⊢ ∅
∈ 𝒫 𝑂 |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → ∅ ∈ 𝒫 𝑂) |
6 | | pwidg 4392 |
. . . . . . 7
⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂) |
7 | 6 | adantr 474 |
. . . . . 6
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂) → 𝑂 ∈ 𝒫 𝑂) |
8 | 7 | elpwdifcl 29905 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂) → (𝑂 ∖ 𝑥) ∈ 𝒫 𝑂) |
9 | 8 | ralrimiva 3174 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂) |
10 | | elpwi 4387 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 𝒫
𝑂 → 𝑥 ⊆ 𝒫 𝑂) |
11 | | pwuniss 29917 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝒫 𝑂 → ∪ 𝑥
⊆ 𝑂) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 𝒫
𝑂 → ∪ 𝑥
⊆ 𝑂) |
13 | 12 | adantl 475 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ∪ 𝑥 ⊆ 𝑂) |
14 | | vuniex 7213 |
. . . . . . . . 9
⊢ ∪ 𝑥
∈ V |
15 | 14 | elpw 4383 |
. . . . . . . 8
⊢ (∪ 𝑥
∈ 𝒫 𝑂 ↔
∪ 𝑥 ⊆ 𝑂) |
16 | 13, 15 | sylibr 226 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ∪ 𝑥 ∈ 𝒫 𝑂) |
17 | 16 | adantr 474 |
. . . . . 6
⊢ (((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) ∧ (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → ∪ 𝑥 ∈ 𝒫 𝑂) |
18 | 17 | ex 403 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)) |
19 | 18 | ralrimiva 3174 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)) |
20 | 5, 9, 19 | 3jca 1164 |
. . 3
⊢ (𝑂 ∈ 𝑉 → (∅ ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂))) |
21 | 3, 20 | jca 509 |
. 2
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝒫
𝑂 ∧ ∀𝑥 ∈ 𝒫 𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)))) |
22 | | isldsys.l |
. . 3
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} |
23 | 22 | isldsys 30763 |
. 2
⊢
(𝒫 𝑂 ∈
𝐿 ↔ (𝒫 𝑂 ∈ 𝒫 𝒫
𝑂 ∧ (∅ ∈
𝒫 𝑂 ∧
∀𝑥 ∈ 𝒫
𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)))) |
24 | 21, 23 | sylibr 226 |
1
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿) |