Step | Hyp | Ref
| Expression |
1 | | eleq2w 2873 |
. . 3
⊢ (𝑥 = 𝑧 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑧)) |
2 | | id 22 |
. . . 4
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
3 | | unieq 4811 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ∪ 𝑥 = ∪
𝑧) |
4 | 3 | difeq1d 4049 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∪ 𝑥 ∖ 𝑦) = (∪ 𝑧 ∖ 𝑦)) |
5 | 4, 2 | eleq12d 2884 |
. . . 4
⊢ (𝑥 = 𝑧 → ((∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ (∪ 𝑧 ∖ 𝑦) ∈ 𝑧)) |
6 | 2, 5 | raleqbidv 3354 |
. . 3
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (∪ 𝑧 ∖ 𝑦) ∈ 𝑧)) |
7 | | pweq 4513 |
. . . 4
⊢ (𝑥 = 𝑧 → 𝒫 𝑥 = 𝒫 𝑧) |
8 | | eleq2w 2873 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∪ 𝑦 ∈ 𝑥 ↔ ∪ 𝑦 ∈ 𝑧)) |
9 | 8 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔ (𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧))) |
10 | 7, 9 | raleqbidv 3354 |
. . 3
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥) ↔
∀𝑦 ∈ 𝒫
𝑧(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧))) |
11 | 1, 6, 10 | 3anbi123d 1433 |
. 2
⊢ (𝑥 = 𝑧 → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥)) ↔ (∅
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (∪
𝑧 ∖ 𝑦) ∈ 𝑧 ∧ ∀𝑦 ∈ 𝒫 𝑧(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧)))) |
12 | | eleq2 2878 |
. . 3
⊢ (𝑧 = 𝑆 → (∅ ∈ 𝑧 ↔ ∅ ∈ 𝑆)) |
13 | | id 22 |
. . . 4
⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆) |
14 | | unieq 4811 |
. . . . . 6
⊢ (𝑧 = 𝑆 → ∪ 𝑧 = ∪
𝑆) |
15 | 14 | difeq1d 4049 |
. . . . 5
⊢ (𝑧 = 𝑆 → (∪ 𝑧 ∖ 𝑦) = (∪ 𝑆 ∖ 𝑦)) |
16 | 15, 13 | eleq12d 2884 |
. . . 4
⊢ (𝑧 = 𝑆 → ((∪ 𝑧 ∖ 𝑦) ∈ 𝑧 ↔ (∪ 𝑆 ∖ 𝑦) ∈ 𝑆)) |
17 | 13, 16 | raleqbidv 3354 |
. . 3
⊢ (𝑧 = 𝑆 → (∀𝑦 ∈ 𝑧 (∪ 𝑧 ∖ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆)) |
18 | | pweq 4513 |
. . . 4
⊢ (𝑧 = 𝑆 → 𝒫 𝑧 = 𝒫 𝑆) |
19 | | eleq2 2878 |
. . . . 5
⊢ (𝑧 = 𝑆 → (∪ 𝑦 ∈ 𝑧 ↔ ∪ 𝑦 ∈ 𝑆)) |
20 | 19 | imbi2d 344 |
. . . 4
⊢ (𝑧 = 𝑆 → ((𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧) ↔ (𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆))) |
21 | 18, 20 | raleqbidv 3354 |
. . 3
⊢ (𝑧 = 𝑆 → (∀𝑦 ∈ 𝒫 𝑧(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧) ↔
∀𝑦 ∈ 𝒫
𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆))) |
22 | 12, 17, 21 | 3anbi123d 1433 |
. 2
⊢ (𝑧 = 𝑆 → ((∅ ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (∪ 𝑧 ∖ 𝑦) ∈ 𝑧 ∧ ∀𝑦 ∈ 𝒫 𝑧(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑧)) ↔ (∅
∈ 𝑆 ∧
∀𝑦 ∈ 𝑆 (∪
𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆)))) |
23 | | df-salg 42951 |
. 2
⊢ SAlg =
{𝑥 ∣ (∅ ∈
𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑥))} |
24 | 11, 22, 23 | elab2gw 3613 |
1
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦
∈ 𝑆)))) |