Theorem kgenuni

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

	Ref	Expression
Hypothesis	kgenuni.1	|- X = U. J
Assertion	kgenuni	|- ( J e. Top -> X = U. ( kGen ` J ) )

Proof

Step	Hyp	Ref	Expression
1		kgenuni.1	|- X = U. J
2	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
3		kgentopon	|- ( J e. ( TopOn ` X ) -> ( kGen ` J ) e. ( TopOn ` X ) )
4	2 3	sylbi	|- ( J e. Top -> ( kGen ` J ) e. ( TopOn ` X ) )
5		toponuni	|- ( ( kGen ` J ) e. ( TopOn ` X ) -> X = U. ( kGen ` J ) )
6	4 5	syl	|- ( J e. Top -> X = U. ( kGen ` J ) )