Proof of Theorem pwldsys
Step | Hyp | Ref
| Expression |
1 | | pwexg 5242 |
. . 3
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) |
2 | | pwidg 4507 |
. . 3
⊢
(𝒫 𝑂 ∈
V → 𝒫 𝑂 ∈
𝒫 𝒫 𝑂) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝒫 𝒫 𝑂) |
4 | | 0elpw 5219 |
. . . 4
⊢ ∅
∈ 𝒫 𝑂 |
5 | 4 | a1i 11 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ∅ ∈ 𝒫 𝑂) |
6 | | pwidg 4507 |
. . . . . 6
⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂) → 𝑂 ∈ 𝒫 𝑂) |
8 | 7 | elpwdifcl 30441 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂) → (𝑂 ∖ 𝑥) ∈ 𝒫 𝑂) |
9 | 8 | ralrimiva 3096 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂) |
10 | | elpwi 4494 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝒫
𝑂 → 𝑥 ⊆ 𝒫 𝑂) |
11 | | sspwuni 4982 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝒫 𝑂 ↔ ∪ 𝑥
⊆ 𝑂) |
12 | 10, 11 | sylib 221 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝒫
𝑂 → ∪ 𝑥
⊆ 𝑂) |
13 | 12 | adantl 485 |
. . . . . 6
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ∪ 𝑥 ⊆ 𝑂) |
14 | | vuniex 7477 |
. . . . . . 7
⊢ ∪ 𝑥
∈ V |
15 | 14 | elpw 4489 |
. . . . . 6
⊢ (∪ 𝑥
∈ 𝒫 𝑂 ↔
∪ 𝑥 ⊆ 𝑂) |
16 | 13, 15 | sylibr 237 |
. . . . 5
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ∪ 𝑥 ∈ 𝒫 𝑂) |
17 | 16 | a1d 25 |
. . . 4
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂) → ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)) |
18 | 17 | ralrimiva 3096 |
. . 3
⊢ (𝑂 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)) |
19 | 5, 9, 18 | 3jca 1129 |
. 2
⊢ (𝑂 ∈ 𝑉 → (∅ ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂))) |
20 | | isldsys.l |
. . 3
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))} |
21 | 20 | isldsys 31686 |
. 2
⊢
(𝒫 𝑂 ∈
𝐿 ↔ (𝒫 𝑂 ∈ 𝒫 𝒫
𝑂 ∧ (∅ ∈
𝒫 𝑂 ∧
∀𝑥 ∈ 𝒫
𝑂(𝑂 ∖ 𝑥) ∈ 𝒫 𝑂 ∧ ∀𝑥 ∈ 𝒫 𝒫 𝑂((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝒫 𝑂)))) |
22 | 3, 19, 21 | sylanbrc 586 |
1
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿) |