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