Step | Hyp | Ref
| Expression |
1 | | issalgend.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
2 | | eqid 2737 |
. . 3
⊢
(SalGen‘𝑋) =
(SalGen‘𝑋) |
3 | | issalgend.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
4 | | issalgend.i |
. . 3
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
5 | | issalgend.u |
. . 3
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝑋) |
6 | 1, 2, 3, 4, 5 | salgenss 43550 |
. 2
⊢ (𝜑 → (SalGen‘𝑋) ⊆ 𝑆) |
7 | | simpl 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝜑) |
8 | | elrabi 3596 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → 𝑦 ∈ SAlg) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑦 ∈ SAlg) |
10 | | unieq 4830 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑦 → ∪ 𝑠 = ∪
𝑦) |
11 | 10 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑦 → (∪ 𝑠 = ∪
𝑋 ↔ ∪ 𝑦 =
∪ 𝑋)) |
12 | | sseq2 3927 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑦 → (𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑦)) |
13 | 11, 12 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑦 → ((∪ 𝑠 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑠) ↔ (∪ 𝑦 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑦))) |
14 | 13 | elrab 3602 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ (𝑦 ∈ SAlg ∧ (∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦))) |
15 | 14 | biimpi 219 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → (𝑦 ∈ SAlg ∧ (∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦))) |
16 | 15 | simprld 772 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑦 = ∪
𝑋) |
17 | 16 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → ∪ 𝑦 = ∪
𝑋) |
18 | 15 | simprrd 774 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → 𝑋 ⊆ 𝑦) |
19 | 18 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑋 ⊆ 𝑦) |
20 | | issalgend.a |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ SAlg ∧ ∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 ⊆ 𝑦) |
21 | 7, 9, 17, 19, 20 | syl13anc 1374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑆 ⊆ 𝑦) |
22 | 21 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}𝑆 ⊆ 𝑦) |
23 | | ssint 4875 |
. . . 4
⊢ (𝑆 ⊆ ∩ {𝑠
∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ ∀𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}𝑆 ⊆ 𝑦) |
24 | 22, 23 | sylibr 237 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
25 | | salgenval 43537 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
26 | 1, 25 | syl 17 |
. . 3
⊢ (𝜑 → (SalGen‘𝑋) = ∩
{𝑠 ∈ SAlg ∣
(∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) |
27 | 24, 26 | sseqtrrd 3942 |
. 2
⊢ (𝜑 → 𝑆 ⊆ (SalGen‘𝑋)) |
28 | 6, 27 | eqssd 3918 |
1
⊢ (𝜑 → (SalGen‘𝑋) = 𝑆) |