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 𝐾 ) )