# Metamath Proof Explorer

## Theorem kgentopon

Description: The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion kgentopon ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 uniss ${⊢}{x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\to \bigcup {x}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
2 kgenval ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)=\left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}$
3 ssrab2 ${⊢}\left\{{x}\in 𝒫{X}|\forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right\}\subseteq 𝒫{X}$
4 2 3 eqsstrdi ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)\subseteq 𝒫{X}$
5 sspwuni ${⊢}\mathrm{𝑘Gen}\left({J}\right)\subseteq 𝒫{X}↔\bigcup \mathrm{𝑘Gen}\left({J}\right)\subseteq {X}$
6 4 5 sylib ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \bigcup \mathrm{𝑘Gen}\left({J}\right)\subseteq {X}$
7 1 6 sylan9ssr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to \bigcup {x}\subseteq {X}$
8 iunin2 ${⊢}\bigcup _{{y}\in {x}}\left({k}\cap {y}\right)={k}\cap \bigcup _{{y}\in {x}}{y}$
9 uniiun ${⊢}\bigcup {x}=\bigcup _{{y}\in {x}}{y}$
10 9 ineq2i ${⊢}{k}\cap \bigcup {x}={k}\cap \bigcup _{{y}\in {x}}{y}$
11 incom ${⊢}{k}\cap \bigcup {x}=\bigcup {x}\cap {k}$
12 8 10 11 3eqtr2i ${⊢}\bigcup _{{y}\in {x}}\left({k}\cap {y}\right)=\bigcup {x}\cap {k}$
13 cmptop ${⊢}{J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {J}{↾}_{𝑡}{k}\in \mathrm{Top}$
14 13 ad2antll ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Top}$
15 incom ${⊢}{y}\cap {k}={k}\cap {y}$
16 simplr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)$
17 16 sselda ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\wedge {y}\in {x}\right)\to {y}\in \mathrm{𝑘Gen}\left({J}\right)$
18 simplrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\wedge {y}\in {x}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
19 kgeni ${⊢}\left({y}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {y}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
20 17 18 19 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\wedge {y}\in {x}\right)\to {y}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
21 15 20 eqeltrrid ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\wedge {y}\in {x}\right)\to {k}\cap {y}\in \left({J}{↾}_{𝑡}{k}\right)$
22 21 ralrimiva ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{k}\cap {y}\in \left({J}{↾}_{𝑡}{k}\right)$
23 iunopn ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{Top}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{k}\cap {y}\in \left({J}{↾}_{𝑡}{k}\right)\right)\to \bigcup _{{y}\in {x}}\left({k}\cap {y}\right)\in \left({J}{↾}_{𝑡}{k}\right)$
24 14 22 23 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \bigcup _{{y}\in {x}}\left({k}\cap {y}\right)\in \left({J}{↾}_{𝑡}{k}\right)$
25 12 24 eqeltrrid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \bigcup {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
26 25 expr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\wedge {k}\in 𝒫{X}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \bigcup {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
27 26 ralrimiva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \bigcup {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
28 elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left(\bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)↔\left(\bigcup {x}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \bigcup {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
29 28 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to \left(\bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)↔\left(\bigcup {x}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \bigcup {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
30 7 27 29 mpbir2and ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\right)\to \bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)$
31 30 ex ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\to \bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)$
32 31 alrimiv ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\to \bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)$
33 inss1 ${⊢}{x}\cap {y}\subseteq {x}$
34 elssuni ${⊢}{x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
35 34 ad2antrl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to {x}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
36 ssidd ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\subseteq {X}$
37 elpwi ${⊢}{k}\in 𝒫{X}\to {k}\subseteq {X}$
38 37 ad2antrl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {k}\subseteq {X}$
39 sseqin2 ${⊢}{k}\subseteq {X}↔{X}\cap {k}={k}$
40 38 39 sylib ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {X}\cap {k}={k}$
41 37 adantr ${⊢}\left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {k}\subseteq {X}$
42 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {k}\subseteq {X}\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
43 41 42 sylan2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
44 toponmax ${⊢}{J}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)\to {k}\in \left({J}{↾}_{𝑡}{k}\right)$
45 43 44 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {k}\in \left({J}{↾}_{𝑡}{k}\right)$
46 40 45 eqeltrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {X}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
47 46 expr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {k}\in 𝒫{X}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {X}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
48 47 ralrimiva ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {X}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
49 elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({X}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({X}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to {X}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
50 36 48 49 mpbir2and ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in \mathrm{𝑘Gen}\left({J}\right)$
51 elssuni ${⊢}{X}\in \mathrm{𝑘Gen}\left({J}\right)\to {X}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
52 50 51 syl ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
53 52 6 eqssd ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup \mathrm{𝑘Gen}\left({J}\right)$
54 53 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to {X}=\bigcup \mathrm{𝑘Gen}\left({J}\right)$
55 35 54 sseqtrrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to {x}\subseteq {X}$
56 33 55 sstrid ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to {x}\cap {y}\subseteq {X}$
57 inindir ${⊢}\left({x}\cap {y}\right)\cap {k}=\left({x}\cap {k}\right)\cap \left({y}\cap {k}\right)$
58 13 ad2antll ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Top}$
59 simplrl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\in \mathrm{𝑘Gen}\left({J}\right)$
60 simprr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
61 kgeni ${⊢}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
62 59 60 61 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
63 simplrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {y}\in \mathrm{𝑘Gen}\left({J}\right)$
64 63 60 19 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to {y}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
65 inopn ${⊢}\left({J}{↾}_{𝑡}{k}\in \mathrm{Top}\wedge {x}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\wedge {y}\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\to \left({x}\cap {k}\right)\cap \left({y}\cap {k}\right)\in \left({J}{↾}_{𝑡}{k}\right)$
66 58 62 64 65 syl3anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \left({x}\cap {k}\right)\cap \left({y}\cap {k}\right)\in \left({J}{↾}_{𝑡}{k}\right)$
67 57 66 eqeltrid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge \left({k}\in 𝒫{X}\wedge {J}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\right)\to \left({x}\cap {y}\right)\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)$
68 67 expr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\wedge {k}\in 𝒫{X}\right)\to \left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left({x}\cap {y}\right)\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
69 68 ralrimiva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left({x}\cap {y}\right)\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)$
70 elkgen ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({x}\cap {y}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left({x}\cap {y}\right)\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
71 70 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to \left({x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)↔\left({x}\cap {y}\subseteq {X}\wedge \forall {k}\in 𝒫{X}\phantom{\rule{.4em}{0ex}}\left({J}{↾}_{𝑡}{k}\in \mathrm{Comp}\to \left({x}\cap {y}\right)\cap {k}\in \left({J}{↾}_{𝑡}{k}\right)\right)\right)\right)$
72 56 69 71 mpbir2and ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)\to {x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)$
73 72 ralrimivva ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \forall {x}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)$
74 fvex ${⊢}\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{V}$
75 istopg ${⊢}\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{V}\to \left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\to \bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \forall {x}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)\right)$
76 74 75 ax-mp ${⊢}\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq \mathrm{𝑘Gen}\left({J}\right)\to \bigcup {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\wedge \forall {x}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{𝑘Gen}\left({J}\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \mathrm{𝑘Gen}\left({J}\right)\right)$
77 32 73 76 sylanbrc ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}$
78 istopon ${⊢}\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left({X}\right)↔\left(\mathrm{𝑘Gen}\left({J}\right)\in \mathrm{Top}\wedge {X}=\bigcup \mathrm{𝑘Gen}\left({J}\right)\right)$
79 77 53 78 sylanbrc ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{𝑘Gen}\left({J}\right)\in \mathrm{TopOn}\left({X}\right)$