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 ⊢ J ∈ Top ∧ J ↾ 𝑡 K ∈ Comp → J ↾ 𝑡 K = 𝑘Gen ⁡ J ↾ 𝑡 K

Proof

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