This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kgencmp2

Description: The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgencmp2 ( 𝐽 ∈ Top → ( ( 𝐽 ↾t 𝐾 ) ∈ Comp ↔ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) )

Proof

Step Hyp Ref Expression
1 kgencmp ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) = ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
2 simpr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp )
3 1 2 eqeltrrd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp )
4 cmptop ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Top )
5 restrcl ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Top → ( ( 𝑘Gen ‘ 𝐽 ) ∈ V ∧ 𝐾 ∈ V ) )
6 5 simprd ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Top → 𝐾 ∈ V )
7 4 6 syl ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp → 𝐾 ∈ V )
8 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) → ( 𝐽 ↾t 𝐾 ) ∈ Top )
9 7 8 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Top )
10 toptopon2 ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top ↔ ( 𝐽 ↾t 𝐾 ) ∈ ( TopOn ‘ ∪ ( 𝐽 ↾t 𝐾 ) ) )
11 9 10 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ ( TopOn ‘ ∪ ( 𝐽 ↾t 𝐾 ) ) )
12 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
13 12 kgenuni ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 = ∪ ( 𝑘Gen ‘ 𝐽 ) )
14 13 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ∪ 𝐽 = ∪ ( 𝑘Gen ‘ 𝐽 ) )
15 14 ineq2d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐾 ∩ ∪ 𝐽 ) = ( 𝐾 ∩ ∪ ( 𝑘Gen ‘ 𝐽 ) ) )
16 12 restuni2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) → ( 𝐾 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐾 ) )
17 7 16 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐾 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐾 ) )
18 kgenftop ⊢ ( 𝐽 ∈ Top → ( 𝑘Gen ‘ 𝐽 ) ∈ Top )
19 eqid ⊢ ∪ ( 𝑘Gen ‘ 𝐽 ) = ∪ ( 𝑘Gen ‘ 𝐽 )
20 19 restuni2 ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ∧ 𝐾 ∈ V ) → ( 𝐾 ∩ ∪ ( 𝑘Gen ‘ 𝐽 ) ) = ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
21 18 7 20 syl2an ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐾 ∩ ∪ ( 𝑘Gen ‘ 𝐽 ) ) = ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
22 15 17 21 3eqtr3d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ∪ ( 𝐽 ↾t 𝐾 ) = ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
23 22 fveq2d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( TopOn ‘ ∪ ( 𝐽 ↾t 𝐾 ) ) = ( TopOn ‘ ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ) )
24 11 23 eleqtrd ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ ( TopOn ‘ ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ) )
25 simpr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp )
26 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
27 26 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
28 ssrest ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ∧ 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
29 18 27 28 syl2an2r ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
30 eqid ⊢ ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) = ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 )
31 30 sscmp ⊢ ( ( ( 𝐽 ↾t 𝐾 ) ∈ ( TopOn ‘ ∪ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ) ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ∧ ( 𝐽 ↾t 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp )
32 24 25 29 31 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp )
33 3 32 impbida ⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ↾t 𝐾 ) ∈ Comp ↔ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ∈ Comp ) )