Step | Hyp | Ref
| Expression |
1 | | 0elpw 5278 |
. . . 4
⊢ ∅
∈ 𝒫 𝑋 |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ∅ ∈ 𝒫 𝑋) |
3 | | unipw 5366 |
. . . . . . . 8
⊢ ∪ 𝒫 𝑋 = 𝑋 |
4 | 3 | difeq1i 4053 |
. . . . . . 7
⊢ (∪ 𝒫 𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑦) |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (∪
𝒫 𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑦)) |
6 | | difssd 4067 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∖ 𝑦) ⊆ 𝑋) |
7 | | difexg 5251 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∖ 𝑦) ∈ V) |
8 | | elpwg 4536 |
. . . . . . . 8
⊢ ((𝑋 ∖ 𝑦) ∈ V → ((𝑋 ∖ 𝑦) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑦) ⊆ 𝑋)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ((𝑋 ∖ 𝑦) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑦) ⊆ 𝑋)) |
10 | 6, 9 | mpbird 256 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∖ 𝑦) ∈ 𝒫 𝑋) |
11 | 5, 10 | eqeltrd 2839 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∪
𝒫 𝑋 ∖ 𝑦) ∈ 𝒫 𝑋) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝑋) → (∪
𝒫 𝑋 ∖ 𝑦) ∈ 𝒫 𝑋) |
13 | 12 | ralrimiva 3103 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 𝑋(∪ 𝒫
𝑋 ∖ 𝑦) ∈ 𝒫 𝑋) |
14 | | elpwi 4542 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → 𝑦 ⊆ 𝒫 𝑋) |
15 | 14 | unissd 4849 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → ∪ 𝑦
⊆ ∪ 𝒫 𝑋) |
16 | 15, 3 | sseqtrdi 3971 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → ∪ 𝑦
⊆ 𝑋) |
17 | | vuniex 7592 |
. . . . . . . . 9
⊢ ∪ 𝑦
∈ V |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → ∪ 𝑦
∈ V) |
19 | | elpwg 4536 |
. . . . . . . 8
⊢ (∪ 𝑦
∈ V → (∪ 𝑦 ∈ 𝒫 𝑋 ↔ ∪ 𝑦 ⊆ 𝑋)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → (∪ 𝑦
∈ 𝒫 𝑋 ↔
∪ 𝑦 ⊆ 𝑋)) |
21 | 16, 20 | mpbird 256 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝒫
𝑋 → ∪ 𝑦
∈ 𝒫 𝑋) |
22 | 21 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) → ∪ 𝑦 ∈ 𝒫 𝑋) |
23 | 22 | a1d 25 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) → (𝑦 ≼ ω → ∪ 𝑦
∈ 𝒫 𝑋)) |
24 | 23 | ralrimiva 3103 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 𝒫 𝑋(𝑦 ≼ ω → ∪ 𝑦
∈ 𝒫 𝑋)) |
25 | 2, 13, 24 | 3jca 1127 |
. 2
⊢ (𝑋 ∈ 𝑉 → (∅ ∈ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋(∪
𝒫 𝑋 ∖ 𝑦) ∈ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝒫
𝑋(𝑦 ≼ ω → ∪ 𝑦
∈ 𝒫 𝑋))) |
26 | | pwexg 5301 |
. . 3
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
27 | | issal 43855 |
. . 3
⊢
(𝒫 𝑋 ∈
V → (𝒫 𝑋
∈ SAlg ↔ (∅ ∈ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋(∪ 𝒫
𝑋 ∖ 𝑦) ∈ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝒫
𝑋(𝑦 ≼ ω → ∪ 𝑦
∈ 𝒫 𝑋)))) |
28 | 26, 27 | syl 17 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 ∈ SAlg ↔ (∅ ∈
𝒫 𝑋 ∧
∀𝑦 ∈ 𝒫
𝑋(∪ 𝒫 𝑋 ∖ 𝑦) ∈ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝒫 𝑋(𝑦 ≼ ω → ∪ 𝑦
∈ 𝒫 𝑋)))) |
29 | 25, 28 | mpbird 256 |
1
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg) |