Proof of Theorem topjoin
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | topontop 22919 | . . . . . . 7
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑘 ∈ Top) | 
| 2 | 1 | ad2antrl 728 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → 𝑘 ∈ Top) | 
| 3 |  | toponmax 22932 | . . . . . . . . 9
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝑘) | 
| 4 | 3 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → 𝑋 ∈ 𝑘) | 
| 5 | 4 | snssd 4809 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → {𝑋} ⊆ 𝑘) | 
| 6 |  | simprr 773 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘) | 
| 7 |  | unissb 4939 | . . . . . . . 8
⊢ (∪ 𝑆
⊆ 𝑘 ↔
∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘) | 
| 8 | 6, 7 | sylibr 234 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → ∪ 𝑆 ⊆ 𝑘) | 
| 9 | 5, 8 | unssd 4192 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → ({𝑋} ∪ ∪ 𝑆) ⊆ 𝑘) | 
| 10 |  | tgfiss 22998 | . . . . . 6
⊢ ((𝑘 ∈ Top ∧ ({𝑋} ∪ ∪ 𝑆)
⊆ 𝑘) →
(topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ⊆ 𝑘) | 
| 11 | 2, 9, 10 | syl2anc 584 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ (𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
⊆ 𝑘) | 
| 12 | 11 | expr 456 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋)) → (∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘 → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
⊆ 𝑘)) | 
| 13 | 12 | ralrimiva 3146 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∀𝑘 ∈ (TopOn‘𝑋)(∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘 → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
⊆ 𝑘)) | 
| 14 |  | ssintrab 4971 | . . 3
⊢
((topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ⊆ ∩ {𝑘
∈ (TopOn‘𝑋)
∣ ∀𝑗 ∈
𝑆 𝑗 ⊆ 𝑘} ↔ ∀𝑘 ∈ (TopOn‘𝑋)(∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘 → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
⊆ 𝑘)) | 
| 15 | 13, 14 | sylibr 234 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
⊆ ∩ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘}) | 
| 16 |  | fibas 22984 | . . . . . 6
⊢
(fi‘({𝑋} ∪
∪ 𝑆)) ∈ TopBases | 
| 17 |  | tgtopon 22978 | . . . . . 6
⊢
((fi‘({𝑋}
∪ ∪ 𝑆)) ∈ TopBases →
(topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ∈ (TopOn‘∪ (fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 18 | 16, 17 | ax-mp 5 | . . . . 5
⊢
(topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ∈ (TopOn‘∪ (fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 19 |  | uniun 4930 | . . . . . . . 8
⊢ ∪ ({𝑋}
∪ ∪ 𝑆) = (∪ {𝑋} ∪ ∪ ∪ 𝑆) | 
| 20 |  | unisng 4925 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝑉 → ∪ {𝑋} = 𝑋) | 
| 21 | 20 | adantr 480 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪
{𝑋} = 𝑋) | 
| 22 | 21 | uneq1d 4167 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (∪
{𝑋} ∪ ∪ ∪ 𝑆) = (𝑋 ∪ ∪ ∪ 𝑆)) | 
| 23 | 19, 22 | eqtr2id 2790 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝑋 ∪ ∪ ∪ 𝑆) =
∪ ({𝑋} ∪ ∪ 𝑆)) | 
| 24 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → 𝑆 ⊆ (TopOn‘𝑋)) | 
| 25 |  | toponuni 22920 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑘) | 
| 26 |  | eqimss2 4043 | . . . . . . . . . . . . . . 15
⊢ (𝑋 = ∪
𝑘 → ∪ 𝑘
⊆ 𝑋) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (TopOn‘𝑋) → ∪ 𝑘
⊆ 𝑋) | 
| 28 |  | sspwuni 5100 | . . . . . . . . . . . . . 14
⊢ (𝑘 ⊆ 𝒫 𝑋 ↔ ∪ 𝑘
⊆ 𝑋) | 
| 29 | 27, 28 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑘 ⊆ 𝒫 𝑋) | 
| 30 |  | velpw 4605 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝒫 𝒫
𝑋 ↔ 𝑘 ⊆ 𝒫 𝑋) | 
| 31 | 29, 30 | sylibr 234 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑘 ∈ 𝒫 𝒫 𝑋) | 
| 32 | 31 | ssriv 3987 | . . . . . . . . . . 11
⊢
(TopOn‘𝑋)
⊆ 𝒫 𝒫 𝑋 | 
| 33 | 24, 32 | sstrdi 3996 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → 𝑆 ⊆ 𝒫 𝒫 𝑋) | 
| 34 |  | sspwuni 5100 | . . . . . . . . . 10
⊢ (𝑆 ⊆ 𝒫 𝒫
𝑋 ↔ ∪ 𝑆
⊆ 𝒫 𝑋) | 
| 35 | 33, 34 | sylib 218 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪ 𝑆 ⊆ 𝒫 𝑋) | 
| 36 |  | sspwuni 5100 | . . . . . . . . 9
⊢ (∪ 𝑆
⊆ 𝒫 𝑋 ↔
∪ ∪ 𝑆 ⊆ 𝑋) | 
| 37 | 35, 36 | sylib 218 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪ ∪ 𝑆
⊆ 𝑋) | 
| 38 |  | ssequn2 4189 | . . . . . . . 8
⊢ (∪ ∪ 𝑆 ⊆ 𝑋 ↔ (𝑋 ∪ ∪ ∪ 𝑆) =
𝑋) | 
| 39 | 37, 38 | sylib 218 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝑋 ∪ ∪ ∪ 𝑆) =
𝑋) | 
| 40 |  | snex 5436 | . . . . . . . . 9
⊢ {𝑋} ∈ V | 
| 41 |  | fvex 6919 | . . . . . . . . . . . 12
⊢
(TopOn‘𝑋)
∈ V | 
| 42 | 41 | ssex 5321 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ (TopOn‘𝑋) → 𝑆 ∈ V) | 
| 43 | 42 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → 𝑆 ∈ V) | 
| 44 | 43 | uniexd 7762 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪ 𝑆 ∈ V) | 
| 45 |  | unexg 7763 | . . . . . . . . 9
⊢ (({𝑋} ∈ V ∧ ∪ 𝑆
∈ V) → ({𝑋} ∪
∪ 𝑆) ∈ V) | 
| 46 | 40, 44, 45 | sylancr 587 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ({𝑋} ∪ ∪ 𝑆) ∈ V) | 
| 47 |  | fiuni 9468 | . . . . . . . 8
⊢ (({𝑋} ∪ ∪ 𝑆)
∈ V → ∪ ({𝑋} ∪ ∪ 𝑆) = ∪
(fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 48 | 46, 47 | syl 17 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪
({𝑋} ∪ ∪ 𝑆) =
∪ (fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 49 | 23, 39, 48 | 3eqtr3d 2785 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → 𝑋 = ∪
(fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 50 | 49 | fveq2d 6910 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (TopOn‘𝑋) = (TopOn‘∪ (fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 51 | 18, 50 | eleqtrrid 2848 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
∈ (TopOn‘𝑋)) | 
| 52 |  | elssuni 4937 | . . . . . . . 8
⊢ (𝑗 ∈ 𝑆 → 𝑗 ⊆ ∪ 𝑆) | 
| 53 |  | ssun2 4179 | . . . . . . . 8
⊢ ∪ 𝑆
⊆ ({𝑋} ∪ ∪ 𝑆) | 
| 54 | 52, 53 | sstrdi 3996 | . . . . . . 7
⊢ (𝑗 ∈ 𝑆 → 𝑗 ⊆ ({𝑋} ∪ ∪ 𝑆)) | 
| 55 |  | ssfii 9459 | . . . . . . . 8
⊢ (({𝑋} ∪ ∪ 𝑆)
∈ V → ({𝑋} ∪
∪ 𝑆) ⊆ (fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 56 | 46, 55 | syl 17 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ({𝑋} ∪ ∪ 𝑆) ⊆ (fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 57 | 54, 56 | sylan9ssr 3998 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑗 ∈ 𝑆) → 𝑗 ⊆ (fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 58 |  | bastg 22973 | . . . . . . 7
⊢
((fi‘({𝑋}
∪ ∪ 𝑆)) ∈ TopBases → (fi‘({𝑋} ∪ ∪ 𝑆))
⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 59 | 16, 58 | ax-mp 5 | . . . . . 6
⊢
(fi‘({𝑋} ∪
∪ 𝑆)) ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) | 
| 60 | 57, 59 | sstrdi 3996 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑗 ∈ 𝑆) → 𝑗 ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 61 | 60 | ralrimiva 3146 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∀𝑗 ∈ 𝑆 𝑗 ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 62 |  | sseq2 4010 | . . . . . 6
⊢ (𝑘 =
(topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) → (𝑗 ⊆ 𝑘 ↔ 𝑗 ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))))) | 
| 63 | 62 | ralbidv 3178 | . . . . 5
⊢ (𝑘 =
(topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) → (∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘 ↔ ∀𝑗 ∈ 𝑆 𝑗 ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))))) | 
| 64 | 63 | elrab 3692 | . . . 4
⊢
((topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘} ↔ ((topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
∈ (TopOn‘𝑋)
∧ ∀𝑗 ∈
𝑆 𝑗 ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))))) | 
| 65 | 51, 61, 64 | sylanbrc 583 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
∈ {𝑘 ∈
(TopOn‘𝑋) ∣
∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘}) | 
| 66 |  | intss1 4963 | . . 3
⊢
((topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘} → ∩ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘} ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 67 | 65, 66 | syl 17 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∩
{𝑘 ∈
(TopOn‘𝑋) ∣
∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘} ⊆ (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))) | 
| 68 | 15, 67 | eqssd 4001 | 1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆)))
= ∩ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘}) |