Step | Hyp | Ref
| Expression |
1 | | df-salgen 43396 |
. . 3
⊢ SalGen =
(𝑥 ∈ V ↦ ∩ {𝑠
∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → SalGen = (𝑥 ∈ V ↦ ∩ {𝑠
∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})) |
3 | | unieq 4807 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ∪ 𝑥 = ∪
𝑋) |
4 | 3 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∪ 𝑠 = ∪
𝑥 ↔ ∪ 𝑠 =
∪ 𝑋)) |
5 | | sseq1 3902 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑠)) |
6 | 4, 5 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((∪ 𝑠 = ∪
𝑥 ∧ 𝑥 ⊆ 𝑠) ↔ (∪ 𝑠 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑠))) |
7 | 6 | rabbidv 3381 |
. . . 4
⊢ (𝑥 = 𝑋 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)} = {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
8 | 7 | inteqd 4841 |
. . 3
⊢ (𝑥 = 𝑋 → ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)} = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
9 | 8 | adantl 485 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 = 𝑋) → ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)} = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
10 | | elex 3416 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V) |
11 | | uniexg 7484 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → ∪ 𝑋 ∈ V) |
12 | | pwsal 43398 |
. . . . . . 7
⊢ (∪ 𝑋
∈ V → 𝒫 ∪ 𝑋 ∈ SAlg) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋
∈ SAlg) |
14 | | unipw 5309 |
. . . . . . 7
⊢ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ∪
𝒫 ∪ 𝑋 = ∪ 𝑋) |
16 | | pwuni 4835 |
. . . . . . 7
⊢ 𝑋 ⊆ 𝒫 ∪ 𝑋 |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝒫 ∪ 𝑋) |
18 | 13, 15, 17 | jca32 519 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝒫 ∪ 𝑋
∈ SAlg ∧ (∪ 𝒫 ∪ 𝑋 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋))) |
19 | | unieq 4807 |
. . . . . . . 8
⊢ (𝑠 = 𝒫 ∪ 𝑋
→ ∪ 𝑠 = ∪ 𝒫
∪ 𝑋) |
20 | 19 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑠 = 𝒫 ∪ 𝑋
→ (∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋)) |
21 | | sseq2 3903 |
. . . . . . 7
⊢ (𝑠 = 𝒫 ∪ 𝑋
→ (𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝒫 ∪ 𝑋)) |
22 | 20, 21 | anbi12d 634 |
. . . . . 6
⊢ (𝑠 = 𝒫 ∪ 𝑋
→ ((∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠) ↔ (∪
𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋))) |
23 | 22 | elrab 3588 |
. . . . 5
⊢
(𝒫 ∪ 𝑋 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ (𝒫 ∪ 𝑋
∈ SAlg ∧ (∪ 𝒫 ∪ 𝑋 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋))) |
24 | 18, 23 | sylibr 237 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋
∈ {𝑠 ∈ SAlg
∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
25 | 24 | ne0d 4224 |
. . 3
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) |
26 | | intex 5205 |
. . 3
⊢ ({𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅ ↔ ∩ {𝑠
∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ∈ V) |
27 | 25, 26 | sylib 221 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ∈ V) |
28 | 2, 9, 10, 27 | fvmptd 6782 |
1
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |