| Step | Hyp | Ref
| Expression |
| 1 | | salgenuni.s |
. . . . 5
⊢ 𝑆 = (SalGen‘𝑋) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑆 = (SalGen‘𝑋)) |
| 3 | | salgenuni.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 4 | | salgenval 46336 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (SalGen‘𝑋) = ∩
{𝑠 ∈ SAlg ∣
(∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
| 6 | 2, 5 | eqtrd 2777 |
. . 3
⊢ (𝜑 → 𝑆 = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
| 7 | 6 | unieqd 4920 |
. 2
⊢ (𝜑 → ∪ 𝑆 =
∪ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
| 8 | | ssrab2 4080 |
. . . 4
⊢ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ⊆ SAlg |
| 9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ⊆ SAlg) |
| 10 | | salgenn0 46346 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) |
| 11 | 3, 10 | syl 17 |
. . 3
⊢ (𝜑 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) |
| 12 | | unieq 4918 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → ∪ 𝑠 = ∪
𝑡) |
| 13 | 12 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (∪ 𝑠 = ∪
𝑋 ↔ ∪ 𝑡 =
∪ 𝑋)) |
| 14 | | sseq2 4010 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑡)) |
| 15 | 13, 14 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → ((∪ 𝑠 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑠) ↔ (∪ 𝑡 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑡))) |
| 16 | 15 | elrab 3692 |
. . . . . . 7
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ (𝑡 ∈ SAlg ∧ (∪ 𝑡 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑡))) |
| 17 | 16 | biimpi 216 |
. . . . . 6
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → (𝑡 ∈ SAlg ∧ (∪ 𝑡 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑡))) |
| 18 | 17 | simprld 772 |
. . . . 5
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑡 = ∪
𝑋) |
| 19 | | salgenuni.u |
. . . . . . 7
⊢ 𝑈 = ∪
𝑋 |
| 20 | 19 | eqcomi 2746 |
. . . . . 6
⊢ ∪ 𝑋 =
𝑈 |
| 21 | 20 | a1i 11 |
. . . . 5
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑋 = 𝑈) |
| 22 | 18, 21 | eqtrd 2777 |
. . . 4
⊢ (𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑡 = 𝑈) |
| 23 | 22 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → ∪ 𝑡 = 𝑈) |
| 24 | 9, 11, 23 | intsaluni 46344 |
. 2
⊢ (𝜑 → ∪ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} = 𝑈) |
| 25 | 7, 24 | eqtrd 2777 |
1
⊢ (𝜑 → ∪ 𝑆 =
𝑈) |