| Step | Hyp | Ref
| Expression |
| 1 | | uniss 4915 |
. . . . . . 7
⊢ (𝑥 ⊆
(𝑘Gen‘𝐽)
→ ∪ 𝑥 ⊆ ∪
(𝑘Gen‘𝐽)) |
| 2 | | kgenval 23543 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽) =
{𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))}) |
| 3 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))} ⊆ 𝒫 𝑋 |
| 4 | 2, 3 | eqsstrdi 4028 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
⊆ 𝒫 𝑋) |
| 5 | | sspwuni 5100 |
. . . . . . . 8
⊢
((𝑘Gen‘𝐽) ⊆ 𝒫 𝑋 ↔ ∪
(𝑘Gen‘𝐽)
⊆ 𝑋) |
| 6 | 4, 5 | sylib 218 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∪ (𝑘Gen‘𝐽) ⊆ 𝑋) |
| 7 | 1, 6 | sylan9ssr 3998 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∪ 𝑥
⊆ 𝑋) |
| 8 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) = (𝑘 ∩ ∪
𝑦 ∈ 𝑥 𝑦) |
| 9 | | uniiun 5058 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
| 10 | 9 | ineq2i 4217 |
. . . . . . . . . 10
⊢ (𝑘 ∩ ∪ 𝑥) =
(𝑘 ∩ ∪ 𝑦 ∈ 𝑥 𝑦) |
| 11 | | incom 4209 |
. . . . . . . . . 10
⊢ (𝑘 ∩ ∪ 𝑥) =
(∪ 𝑥 ∩ 𝑘) |
| 12 | 8, 10, 11 | 3eqtr2i 2771 |
. . . . . . . . 9
⊢ ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) = (∪ 𝑥 ∩ 𝑘) |
| 13 | | cmptop 23403 |
. . . . . . . . . . 11
⊢ ((𝐽 ↾t 𝑘) ∈ Comp → (𝐽 ↾t 𝑘) ∈ Top) |
| 14 | 13 | ad2antll 729 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Top) |
| 15 | | incom 4209 |
. . . . . . . . . . . 12
⊢ (𝑦 ∩ 𝑘) = (𝑘 ∩ 𝑦) |
| 16 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑥 ⊆ (𝑘Gen‘𝐽)) |
| 17 | 16 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (𝑘Gen‘𝐽)) |
| 18 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝐽 ↾t 𝑘) ∈ Comp) |
| 19 | | kgeni 23545 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝑘)
∈ Comp) → (𝑦
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 21 | 15, 20 | eqeltrrid 2846 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
| 22 | 21 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ∀𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
| 23 | | iunopn 22904 |
. . . . . . . . . 10
⊢ (((𝐽 ↾t 𝑘) ∈ Top ∧ ∀𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) → ∪
𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
| 24 | 14, 22, 23 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
| 25 | 12, 24 | eqeltrrid 2846 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 26 | 25 | expr 456 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 27 | 26 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 28 | | elkgen 23544 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → (∪ 𝑥
∈ (𝑘Gen‘𝐽) ↔ (∪ 𝑥 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → (∪ 𝑥
∈ (𝑘Gen‘𝐽) ↔ (∪ 𝑥 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
| 30 | 7, 27, 29 | mpbir2and 713 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∪ 𝑥
∈ (𝑘Gen‘𝐽)) |
| 31 | 30 | ex 412 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽))) |
| 32 | 31 | alrimiv 1927 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑥(𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽))) |
| 33 | | inss1 4237 |
. . . . . 6
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
| 34 | | elssuni 4937 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑘Gen‘𝐽)
→ 𝑥 ⊆ ∪ (𝑘Gen‘𝐽)) |
| 35 | 34 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑥 ⊆ ∪
(𝑘Gen‘𝐽)) |
| 36 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ⊆ 𝑋) |
| 37 | | elpwi 4607 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋) |
| 38 | 37 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ 𝑋) |
| 39 | | sseqin2 4223 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑘) = 𝑘) |
| 40 | 38, 39 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑋 ∩ 𝑘) = 𝑘) |
| 41 | 37 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp) → 𝑘 ⊆ 𝑋) |
| 42 | | resttopon 23169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘 ⊆ 𝑋) → (𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘)) |
| 43 | 41, 42 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘)) |
| 44 | | toponmax 22932 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘) → 𝑘 ∈ (𝐽 ↾t 𝑘)) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ (𝐽 ↾t 𝑘)) |
| 46 | 40, 45 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 47 | 46 | expr 456 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 48 | 47 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 49 | | elkgen 23544 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑋 ∈ (𝑘Gen‘𝐽) ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
| 50 | 36, 48, 49 | mpbir2and 713 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ (𝑘Gen‘𝐽)) |
| 51 | | elssuni 4937 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(𝑘Gen‘𝐽)
→ 𝑋 ⊆ ∪ (𝑘Gen‘𝐽)) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ⊆ ∪
(𝑘Gen‘𝐽)) |
| 53 | 52, 6 | eqssd 4001 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪
(𝑘Gen‘𝐽)) |
| 54 | 53 | adantr 480 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑋 = ∪
(𝑘Gen‘𝐽)) |
| 55 | 35, 54 | sseqtrrd 4021 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑥 ⊆ 𝑋) |
| 56 | 33, 55 | sstrid 3995 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → (𝑥 ∩ 𝑦) ⊆ 𝑋) |
| 57 | | inindir 4236 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ∩ 𝑘) = ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) |
| 58 | 13 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Top) |
| 59 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘𝐽)) |
| 60 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Comp) |
| 61 | | kgeni 23545 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝑘)
∈ Comp) → (𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 62 | 59, 60, 61 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 63 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑦 ∈ (𝑘Gen‘𝐽)) |
| 64 | 63, 60, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 65 | | inopn 22905 |
. . . . . . . . 9
⊢ (((𝐽 ↾t 𝑘) ∈ Top ∧ (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘) ∧ (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) → ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) ∈ (𝐽 ↾t 𝑘)) |
| 66 | 58, 62, 64, 65 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) ∈ (𝐽 ↾t 𝑘)) |
| 67 | 57, 66 | eqeltrid 2845 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
| 68 | 67 | expr 456 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 69 | 68 | ralrimiva 3146 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
| 70 | | elkgen 23544 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽) ↔ ((𝑥 ∩ 𝑦) ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
| 71 | 70 | adantr 480 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → ((𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽) ↔ ((𝑥 ∩ 𝑦) ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
| 72 | 56, 69, 71 | mpbir2and 713 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → (𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)) |
| 73 | 72 | ralrimivva 3202 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑥 ∈
(𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)) |
| 74 | | fvex 6919 |
. . . 4
⊢
(𝑘Gen‘𝐽) ∈ V |
| 75 | | istopg 22901 |
. . . 4
⊢
((𝑘Gen‘𝐽) ∈ V → ((𝑘Gen‘𝐽) ∈ Top ↔
(∀𝑥(𝑥 ⊆
(𝑘Gen‘𝐽)
→ ∪ 𝑥 ∈ (𝑘Gen‘𝐽)) ∧ ∀𝑥 ∈ (𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)))) |
| 76 | 74, 75 | ax-mp 5 |
. . 3
⊢
((𝑘Gen‘𝐽) ∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽)) ∧ ∀𝑥 ∈ (𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽))) |
| 77 | 32, 73, 76 | sylanbrc 583 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
∈ Top) |
| 78 | | istopon 22918 |
. 2
⊢
((𝑘Gen‘𝐽) ∈ (TopOn‘𝑋) ↔ ((𝑘Gen‘𝐽) ∈ Top ∧ 𝑋 = ∪
(𝑘Gen‘𝐽))) |
| 79 | 77, 53, 78 | sylanbrc 583 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
∈ (TopOn‘𝑋)) |