Metamath Proof Explorer

Theorem kgentopon

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

Ref Expression
Assertion kgentopon ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 uniss ⊢ ( 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) → ∪ 𝑥 ⊆ ∪ ( 𝑘Gen ‘ 𝐽 ) )
2 kgenval ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } )
3 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) } ⊆ 𝒫 𝑋
4 2 3 eqsstrdi ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝒫 𝑋 )
5 sspwuni ⊢ ( ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝒫 𝑋 ↔ ∪ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝑋 )
6 4 5 sylib ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∪ ( 𝑘Gen ‘ 𝐽 ) ⊆ 𝑋 )
7 1 6 sylan9ssr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ∪ 𝑥 ⊆ 𝑋 )
8 iunin2 ⊢ ∪ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) = ( 𝑘 ∩ ∪ 𝑦 ∈ 𝑥 𝑦 )
9 uniiun ⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
10 9 ineq2i ⊢ ( 𝑘 ∩ ∪ 𝑥 ) = ( 𝑘 ∩ ∪ 𝑦 ∈ 𝑥 𝑦 )
11 incom ⊢ ( 𝑘 ∩ ∪ 𝑥 ) = ( ∪ 𝑥 ∩ 𝑘 )
12 8 10 11 3eqtr2i ⊢ ∪ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) = ( ∪ 𝑥 ∩ 𝑘 )
13 cmptop ⊢ ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐽 ↾t 𝑘 ) ∈ Top )
14 13 ad2antll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝐽 ↾t 𝑘 ) ∈ Top )
15 incom ⊢ ( 𝑦 ∩ 𝑘 ) = ( 𝑘 ∩ 𝑦 )
16 simplr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
17 16 sselda ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) )
18 simplrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐽 ↾t 𝑘 ) ∈ Comp )
19 kgeni ⊢ ( ( 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) → ( 𝑦 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
20 17 18 19 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
21 15 20 eqeltrrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑘 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑘 ) )
22 21 ralrimiva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑘 ) )
23 iunopn ⊢ ( ( ( 𝐽 ↾t 𝑘 ) ∈ Top ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → ∪ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑘 ) )
24 14 22 23 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ∪ 𝑦 ∈ 𝑥 ( 𝑘 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑘 ) )
25 12 24 eqeltrrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( ∪ 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
26 25 expr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∪ 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
27 26 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∪ 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
28 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∪ 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
29 28 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ( ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∪ 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
30 7 27 29 mpbir2and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) )
31 30 ex ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) → ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) )
32 31 alrimiv ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑥 ( 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) → ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) )
33 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
34 elssuni ⊢ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑥 ⊆ ∪ ( 𝑘Gen ‘ 𝐽 ) )
35 34 ad2antrl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → 𝑥 ⊆ ∪ ( 𝑘Gen ‘ 𝐽 ) )
36 ssidd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ⊆ 𝑋 )
37 elpwi ⊢ ( 𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋 )
38 37 ad2antrl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 ⊆ 𝑋 )
39 sseqin2 ⊢ ( 𝑘 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝑘 ) = 𝑘 )
40 38 39 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑋 ∩ 𝑘 ) = 𝑘 )
41 37 adantr ⊢ ( ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) → 𝑘 ⊆ 𝑋 )
42 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
43 41 42 sylan2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
44 toponmax ⊢ ( ( 𝐽 ↾t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) → 𝑘 ∈ ( 𝐽 ↾t 𝑘 ) )
45 43 44 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 ∈ ( 𝐽 ↾t 𝑘 ) )
46 40 45 eqeltrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑋 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
47 46 expr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑋 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
48 47 ralrimiva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑋 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
49 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑋 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑋 ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑋 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
50 36 48 49 mpbir2and ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ ( 𝑘Gen ‘ 𝐽 ) )
51 elssuni ⊢ ( 𝑋 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝑋 ⊆ ∪ ( 𝑘Gen ‘ 𝐽 ) )
52 50 51 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ⊆ ∪ ( 𝑘Gen ‘ 𝐽 ) )
53 52 6 eqssd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ ( 𝑘Gen ‘ 𝐽 ) )
54 53 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → 𝑋 = ∪ ( 𝑘Gen ‘ 𝐽 ) )
55 35 54 sseqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → 𝑥 ⊆ 𝑋 )
56 33 55 sstrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
57 inindir ⊢ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) = ( ( 𝑥 ∩ 𝑘 ) ∩ ( 𝑦 ∩ 𝑘 ) )
58 13 ad2antll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝐽 ↾t 𝑘 ) ∈ Top )
59 simplrl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) )
60 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝐽 ↾t 𝑘 ) ∈ Comp )
61 kgeni ⊢ ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
62 59 60 61 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
63 simplrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) )
64 63 60 19 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑦 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
65 inopn ⊢ ( ( ( 𝐽 ↾t 𝑘 ) ∈ Top ∧ ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ∧ ( 𝑦 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) → ( ( 𝑥 ∩ 𝑘 ) ∩ ( 𝑦 ∩ 𝑘 ) ) ∈ ( 𝐽 ↾t 𝑘 ) )
66 58 62 64 65 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑥 ∩ 𝑘 ) ∩ ( 𝑦 ∩ 𝑘 ) ) ∈ ( 𝐽 ↾t 𝑘 ) )
67 57 66 eqeltrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ ( 𝑘 ∈ 𝒫 𝑋 ∧ ( 𝐽 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
68 67 expr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
69 68 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
70 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
71 70 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
72 56 69 71 mpbir2and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) )
73 72 ralrimivva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∀ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) )
74 fvex ⊢ ( 𝑘Gen ‘ 𝐽 ) ∈ V
75 istopg ⊢ ( ( 𝑘Gen ‘ 𝐽 ) ∈ V → ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) → ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∀ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ) ) )
76 74 75 ax-mp ⊢ ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝑘Gen ‘ 𝐽 ) → ∪ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) ∧ ∀ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∀ 𝑦 ∈ ( 𝑘Gen ‘ 𝐽 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑘Gen ‘ 𝐽 ) ) )
77 32 73 76 sylanbrc ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ Top )
78 istopon ⊢ ( ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ 𝑋 ) ↔ ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ∧ 𝑋 = ∪ ( 𝑘Gen ‘ 𝐽 ) ) )
79 77 53 78 sylanbrc ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑘Gen ‘ 𝐽 ) ∈ ( TopOn ‘ 𝑋 ) )