Step | Hyp | Ref
| Expression |
1 | | uniss 4458 |
. . . . . . 7
⊢ (𝑥 ⊆
(𝑘Gen‘𝐽)
→ ∪ 𝑥 ⊆ ∪
(𝑘Gen‘𝐽)) |
2 | | kgenval 21338 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽) =
{𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))}) |
3 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))} ⊆ 𝒫 𝑋 |
4 | 2, 3 | syl6eqss 3655 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
⊆ 𝒫 𝑋) |
5 | | sspwuni 4611 |
. . . . . . . 8
⊢
((𝑘Gen‘𝐽) ⊆ 𝒫 𝑋 ↔ ∪
(𝑘Gen‘𝐽)
⊆ 𝑋) |
6 | 4, 5 | sylib 208 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∪ (𝑘Gen‘𝐽) ⊆ 𝑋) |
7 | 1, 6 | sylan9ssr 3617 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∪ 𝑥
⊆ 𝑋) |
8 | | iunin2 4584 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) = (𝑘 ∩ ∪
𝑦 ∈ 𝑥 𝑦) |
9 | | uniiun 4573 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
10 | 9 | ineq2i 3811 |
. . . . . . . . . 10
⊢ (𝑘 ∩ ∪ 𝑥) =
(𝑘 ∩ ∪ 𝑦 ∈ 𝑥 𝑦) |
11 | | incom 3805 |
. . . . . . . . . 10
⊢ (𝑘 ∩ ∪ 𝑥) =
(∪ 𝑥 ∩ 𝑘) |
12 | 8, 10, 11 | 3eqtr2i 2650 |
. . . . . . . . 9
⊢ ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) = (∪ 𝑥 ∩ 𝑘) |
13 | | cmptop 21198 |
. . . . . . . . . . 11
⊢ ((𝐽 ↾t 𝑘) ∈ Comp → (𝐽 ↾t 𝑘) ∈ Top) |
14 | 13 | ad2antll 765 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Top) |
15 | | incom 3805 |
. . . . . . . . . . . 12
⊢ (𝑦 ∩ 𝑘) = (𝑘 ∩ 𝑦) |
16 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑥 ⊆ (𝑘Gen‘𝐽)) |
17 | 16 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (𝑘Gen‘𝐽)) |
18 | | simplrr 801 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝐽 ↾t 𝑘) ∈ Comp) |
19 | | kgeni 21340 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝑘)
∈ Comp) → (𝑦
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
20 | 17, 18, 19 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
21 | 15, 20 | syl5eqelr 2706 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) ∧ 𝑦 ∈ 𝑥) → (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
22 | 21 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ∀𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
23 | | iunopn 20703 |
. . . . . . . . . 10
⊢ (((𝐽 ↾t 𝑘) ∈ Top ∧ ∀𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) → ∪
𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
24 | 14, 22, 23 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ∪ 𝑦 ∈ 𝑥 (𝑘 ∩ 𝑦) ∈ (𝐽 ↾t 𝑘)) |
25 | 12, 24 | syl5eqelr 2706 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
26 | 25 | expr 643 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
27 | 26 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
28 | | elkgen 21339 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → (∪ 𝑥
∈ (𝑘Gen‘𝐽) ↔ (∪ 𝑥 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
29 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → (∪ 𝑥
∈ (𝑘Gen‘𝐽) ↔ (∪ 𝑥 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (∪ 𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
30 | 7, 27, 29 | mpbir2and 957 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ⊆ (𝑘Gen‘𝐽)) → ∪ 𝑥
∈ (𝑘Gen‘𝐽)) |
31 | 30 | ex 450 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽))) |
32 | 31 | alrimiv 1855 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑥(𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽))) |
33 | | inss1 3833 |
. . . . . 6
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
34 | | elssuni 4467 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑘Gen‘𝐽)
→ 𝑥 ⊆ ∪ (𝑘Gen‘𝐽)) |
35 | 34 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑥 ⊆ ∪
(𝑘Gen‘𝐽)) |
36 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ 𝑋 ⊆ 𝑋 |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ⊆ 𝑋) |
38 | | elpwi 4168 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋) |
39 | 38 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ 𝑋) |
40 | | sseqin2 3817 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑘) = 𝑘) |
41 | 39, 40 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑋 ∩ 𝑘) = 𝑘) |
42 | 38 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp) → 𝑘 ⊆ 𝑋) |
43 | | resttopon 20965 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘 ⊆ 𝑋) → (𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘)) |
44 | 42, 43 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘)) |
45 | | toponmax 20730 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ↾t 𝑘) ∈ (TopOn‘𝑘) → 𝑘 ∈ (𝐽 ↾t 𝑘)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ (𝐽 ↾t 𝑘)) |
47 | 41, 46 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
48 | 47 | expr 643 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
49 | 48 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
50 | | elkgen 21339 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑋 ∈ (𝑘Gen‘𝐽) ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑋 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
51 | 37, 49, 50 | mpbir2and 957 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ (𝑘Gen‘𝐽)) |
52 | | elssuni 4467 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(𝑘Gen‘𝐽)
→ 𝑋 ⊆ ∪ (𝑘Gen‘𝐽)) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ⊆ ∪
(𝑘Gen‘𝐽)) |
54 | 53, 6 | eqssd 3620 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪
(𝑘Gen‘𝐽)) |
55 | 54 | adantr 481 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑋 = ∪
(𝑘Gen‘𝐽)) |
56 | 35, 55 | sseqtr4d 3642 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → 𝑥 ⊆ 𝑋) |
57 | 33, 56 | syl5ss 3614 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → (𝑥 ∩ 𝑦) ⊆ 𝑋) |
58 | | inindir 3831 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ∩ 𝑘) = ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) |
59 | 13 | ad2antll 765 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Top) |
60 | | simplrl 800 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘𝐽)) |
61 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝐽 ↾t 𝑘) ∈ Comp) |
62 | | kgeni 21340 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝑘)
∈ Comp) → (𝑥
∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
63 | 60, 61, 62 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
64 | | simplrr 801 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → 𝑦 ∈ (𝑘Gen‘𝐽)) |
65 | 64, 61, 19 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
66 | | inopn 20704 |
. . . . . . . . 9
⊢ (((𝐽 ↾t 𝑘) ∈ Top ∧ (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘) ∧ (𝑦 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) → ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) ∈ (𝐽 ↾t 𝑘)) |
67 | 59, 63, 65, 66 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ((𝑥 ∩ 𝑘) ∩ (𝑦 ∩ 𝑘)) ∈ (𝐽 ↾t 𝑘)) |
68 | 58, 67 | syl5eqel 2705 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ (𝑘 ∈ 𝒫 𝑋 ∧ (𝐽 ↾t 𝑘) ∈ Comp)) → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) |
69 | 68 | expr 643 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) ∧ 𝑘 ∈ 𝒫 𝑋) → ((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
70 | 69 | ralrimiva 2966 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))) |
71 | | elkgen 21339 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽) ↔ ((𝑥 ∩ 𝑦) ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
72 | 71 | adantr 481 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → ((𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽) ↔ ((𝑥 ∩ 𝑦) ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → ((𝑥 ∩ 𝑦) ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) |
73 | 57, 70, 72 | mpbir2and 957 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑥 ∈ (𝑘Gen‘𝐽) ∧ 𝑦 ∈ (𝑘Gen‘𝐽))) → (𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)) |
74 | 73 | ralrimivva 2971 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∀𝑥 ∈
(𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)) |
75 | | fvex 6201 |
. . . 4
⊢
(𝑘Gen‘𝐽) ∈ V |
76 | | istopg 20700 |
. . . 4
⊢
((𝑘Gen‘𝐽) ∈ V → ((𝑘Gen‘𝐽) ∈ Top ↔
(∀𝑥(𝑥 ⊆
(𝑘Gen‘𝐽)
→ ∪ 𝑥 ∈ (𝑘Gen‘𝐽)) ∧ ∀𝑥 ∈ (𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽)))) |
77 | 75, 76 | ax-mp 5 |
. . 3
⊢
((𝑘Gen‘𝐽) ∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝑘Gen‘𝐽) → ∪ 𝑥
∈ (𝑘Gen‘𝐽)) ∧ ∀𝑥 ∈ (𝑘Gen‘𝐽)∀𝑦 ∈ (𝑘Gen‘𝐽)(𝑥 ∩ 𝑦) ∈ (𝑘Gen‘𝐽))) |
78 | 32, 74, 77 | sylanbrc 698 |
. 2
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
∈ Top) |
79 | | istopon 20717 |
. 2
⊢
((𝑘Gen‘𝐽) ∈ (TopOn‘𝑋) ↔ ((𝑘Gen‘𝐽) ∈ Top ∧ 𝑋 = ∪
(𝑘Gen‘𝐽))) |
80 | 78, 54, 79 | sylanbrc 698 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) →
(𝑘Gen‘𝐽)
∈ (TopOn‘𝑋)) |