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

Metamath Proof Explorer

Theorem kgencmp

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

Ref Expression
Assertion kgencmp ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) = ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )

Proof

Step Hyp Ref Expression
1 kgenftop ⊢ ( 𝐽 ∈ Top → ( 𝑘Gen ‘ 𝐽 ) ∈ Top )
2 1 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝑘Gen ‘ 𝐽 ) ∈ Top )
3 kgenss ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
4 3 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )
5 ssrest ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ∧ 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
6 2 4 5 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ⊆ ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )
7 cmptop ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Comp → ( 𝐽 ↾t 𝐾 ) ∈ Top )
8 7 adantl ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Top )
9 restrcl ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ) )
10 9 simprd ⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → 𝐾 ∈ V )
11 8 10 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐾 ∈ V )
12 restval ⊢ ( ( ( 𝑘Gen ‘ 𝐽 ) ∈ Top ∧ 𝐾 ∈ V ) → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) = ran ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↦ ( 𝑥 ∩ 𝐾 ) ) )
13 2 11 12 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) = ran ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↦ ( 𝑥 ∩ 𝐾 ) ) )
14 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) )
15 simplr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp )
16 kgeni ⊢ ( ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝑥 ∩ 𝐾 ) ∈ ( 𝐽 ↾t 𝐾 ) )
17 14 15 16 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝑥 ∩ 𝐾 ) ∈ ( 𝐽 ↾t 𝐾 ) )
18 17 fmpttd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↦ ( 𝑥 ∩ 𝐾 ) ) : ( 𝑘Gen ‘ 𝐽 ) ⟶ ( 𝐽 ↾t 𝐾 ) )
19 18 frnd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ran ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↦ ( 𝑥 ∩ 𝐾 ) ) ⊆ ( 𝐽 ↾t 𝐾 ) )
20 13 19 eqsstrd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) ⊆ ( 𝐽 ↾t 𝐾 ) )
21 6 20 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) = ( ( 𝑘Gen ‘ 𝐽 ) ↾t 𝐾 ) )