Step | Hyp | Ref
| Expression |
1 | | salgenuni.s |
. . . . 5
⊢ 𝑆 = (SalGen‘𝑋) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑆 = (SalGen‘𝑋)) |
3 | | salgenuni.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
4 | | salgenval 43426 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (SalGen‘𝑋) = ∩
{𝑠 ∈ SAlg ∣
(∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
6 | 2, 5 | eqtrd 2773 |
. . 3
⊢ (𝜑 → 𝑆 = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
7 | 6 | unieqd 4810 |
. 2
⊢ (𝜑 → ∪ 𝑆 =
∪ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
8 | | ssrab2 3969 |
. . . 4
⊢ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ⊆ SAlg |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ⊆ SAlg) |
10 | | salgenn0 43434 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) |
11 | 3, 10 | syl 17 |
. . 3
⊢ (𝜑 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) |
12 | | unieq 4807 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → ∪ 𝑠 = ∪
𝑡) |
13 | 12 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (∪ 𝑠 = ∪
𝑋 ↔ ∪ 𝑡 =
∪ 𝑋)) |
14 | | sseq2 3903 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑡)) |
15 | 13, 14 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → ((∪ 𝑠 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑠) ↔ (∪ 𝑡 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑡))) |
16 | 15 | elrab 3588 |
. . . . . . 7
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ (𝑡 ∈ SAlg ∧ (∪ 𝑡 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑡))) |
17 | 16 | biimpi 219 |
. . . . . 6
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → (𝑡 ∈ SAlg ∧ (∪ 𝑡 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑡))) |
18 | 17 | simprld 772 |
. . . . 5
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑡 = ∪
𝑋) |
19 | | salgenuni.u |
. . . . . . 7
⊢ 𝑈 = ∪
𝑋 |
20 | 19 | eqcomi 2747 |
. . . . . 6
⊢ ∪ 𝑋 =
𝑈 |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑋 = 𝑈) |
22 | 18, 21 | eqtrd 2773 |
. . . 4
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑡 = 𝑈) |
23 | 22 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → ∪ 𝑡 = 𝑈) |
24 | 9, 11, 23 | intsaluni 43432 |
. 2
⊢ (𝜑 → ∪ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} = 𝑈) |
25 | 7, 24 | eqtrd 2773 |
1
⊢ (𝜑 → ∪ 𝑆 =
𝑈) |