| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | issalgend.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 2 |  | eqid 2736 | . . 3
⊢
(SalGen‘𝑋) =
(SalGen‘𝑋) | 
| 3 |  | issalgend.s | . . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) | 
| 4 |  | issalgend.i | . . 3
⊢ (𝜑 → 𝑋 ⊆ 𝑆) | 
| 5 |  | issalgend.u | . . 3
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝑋) | 
| 6 | 1, 2, 3, 4, 5 | salgenss 46356 | . 2
⊢ (𝜑 → (SalGen‘𝑋) ⊆ 𝑆) | 
| 7 |  | simpl 482 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝜑) | 
| 8 |  | elrabi 3686 | . . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → 𝑦 ∈ SAlg) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑦 ∈ SAlg) | 
| 10 |  | unieq 4917 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑦 → ∪ 𝑠 = ∪
𝑦) | 
| 11 | 10 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑦 → (∪ 𝑠 = ∪
𝑋 ↔ ∪ 𝑦 =
∪ 𝑋)) | 
| 12 |  | sseq2 4009 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑦 → (𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑦)) | 
| 13 | 11, 12 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑠 = 𝑦 → ((∪ 𝑠 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑠) ↔ (∪ 𝑦 = ∪
𝑋 ∧ 𝑋 ⊆ 𝑦))) | 
| 14 | 13 | elrab 3691 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ (𝑦 ∈ SAlg ∧ (∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦))) | 
| 15 | 14 | biimpi 216 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → (𝑦 ∈ SAlg ∧ (∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦))) | 
| 16 | 15 | simprld 771 | . . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → ∪ 𝑦 = ∪
𝑋) | 
| 17 | 16 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → ∪ 𝑦 = ∪
𝑋) | 
| 18 | 15 | simprrd 773 | . . . . . . 7
⊢ (𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} → 𝑋 ⊆ 𝑦) | 
| 19 | 18 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑋 ⊆ 𝑦) | 
| 20 |  | issalgend.a | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ SAlg ∧ ∪ 𝑦 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 ⊆ 𝑦) | 
| 21 | 7, 9, 17, 19, 20 | syl13anc 1373 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) → 𝑆 ⊆ 𝑦) | 
| 22 | 21 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}𝑆 ⊆ 𝑦) | 
| 23 |  | ssint 4963 | . . . 4
⊢ (𝑆 ⊆ ∩ {𝑠
∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ↔ ∀𝑦 ∈ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}𝑆 ⊆ 𝑦) | 
| 24 | 22, 23 | sylibr 234 | . . 3
⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | 
| 25 |  | salgenval 46341 | . . . 4
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 =
∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | 
| 26 | 1, 25 | syl 17 | . . 3
⊢ (𝜑 → (SalGen‘𝑋) = ∩
{𝑠 ∈ SAlg ∣
(∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | 
| 27 | 24, 26 | sseqtrrd 4020 | . 2
⊢ (𝜑 → 𝑆 ⊆ (SalGen‘𝑋)) | 
| 28 | 6, 27 | eqssd 4000 | 1
⊢ (𝜑 → (SalGen‘𝑋) = 𝑆) |