Step | Hyp | Ref
| Expression |
1 | | eleq2 2677 |
. . 3
⊢ (𝑥 = 𝑆 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑆)) |
2 | | raleq 3115 |
. . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑆 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥)) |
3 | | unieq 4380 |
. . . . . . 7
⊢ (𝑥 = 𝑆 → ∪ 𝑥 = ∪
𝑆) |
4 | 3 | difeq1d 3689 |
. . . . . 6
⊢ (𝑥 = 𝑆 → (∪ 𝑥 ∖ 𝑦) = (∪ 𝑆 ∖ 𝑦)) |
5 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑆 → 𝑥 = 𝑆) |
6 | 4, 5 | eleq12d 2682 |
. . . . 5
⊢ (𝑥 = 𝑆 → ((∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ (∪ 𝑆 ∖ 𝑦) ∈ 𝑆)) |
7 | 6 | ralbidv 2969 |
. . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝑆 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆)) |
8 | 2, 7 | bitrd 267 |
. . 3
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆)) |
9 | | pweq 4111 |
. . . . 5
⊢ (𝑥 = 𝑆 → 𝒫 𝑥 = 𝒫 𝑆) |
10 | 9 | raleqdv 3121 |
. . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔
∀𝑦 ∈ 𝒫
𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥))) |
11 | | eleq2 2677 |
. . . . . 6
⊢ (𝑥 = 𝑆 → (∪ 𝑦 ∈ 𝑥 ↔ ∪ 𝑦 ∈ 𝑆)) |
12 | 11 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑆 → ((𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔ (𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆))) |
13 | 12 | ralbidv 2969 |
. . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔
∀𝑦 ∈ 𝒫
𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆))) |
14 | 10, 13 | bitrd 267 |
. . 3
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔
∀𝑦 ∈ 𝒫
𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆))) |
15 | 1, 8, 14 | 3anbi123d 1391 |
. 2
⊢ (𝑥 = 𝑆 → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥)) ↔ (∅
∈ 𝑆 ∧
∀𝑦 ∈ 𝑆 (∪
𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆)))) |
16 | | df-salg 39205 |
. 2
⊢ SAlg =
{𝑥 ∣ (∅ ∈
𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥))} |
17 | 15, 16 | elab2g 3322 |
1
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆)))) |