Metamath Proof Explorer

Theorem kgenval

Description: Value of the compact generator. (The "k" in kGen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgenval	\|- ( J e. ( TopOn ` X ) -> ( kGen ` J ) = { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } )

Proof

Step	Hyp	Ref	Expression
1		df-kgen	\|- kGen = ( j e. Top \|-> { x e. ~P U. j \| A. k e. ~P U. j ( ( j \|`t k ) e. Comp -> ( x i^i k ) e. ( j \|`t k ) ) } )
2		unieq	\|- ( j = J -> U. j = U. J )
3		toponuni	\|- ( J e. ( TopOn ` X ) -> X = U. J )
4	3	eqcomd	\|- ( J e. ( TopOn ` X ) -> U. J = X )
5	2 4	sylan9eqr	\|- ( ( J e. ( TopOn ` X ) /\ j = J ) -> U. j = X )
6	5	pweqd	\|- ( ( J e. ( TopOn ` X ) /\ j = J ) -> ~P U. j = ~P X )
7		oveq1	\|- ( j = J -> ( j \|`t k ) = ( J \|`t k ) )
8	7	eleq1d	\|- ( j = J -> ( ( j \|`t k ) e. Comp <-> ( J \|`t k ) e. Comp ) )
9	7	eleq2d	\|- ( j = J -> ( ( x i^i k ) e. ( j \|`t k ) <-> ( x i^i k ) e. ( J \|`t k ) ) )
10	8 9	imbi12d	\|- ( j = J -> ( ( ( j \|`t k ) e. Comp -> ( x i^i k ) e. ( j \|`t k ) ) <-> ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) )
11	10	adantl	\|- ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( ( ( j \|`t k ) e. Comp -> ( x i^i k ) e. ( j \|`t k ) ) <-> ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) )
12	6 11	raleqbidv	\|- ( ( J e. ( TopOn ` X ) /\ j = J ) -> ( A. k e. ~P U. j ( ( j \|`t k ) e. Comp -> ( x i^i k ) e. ( j \|`t k ) ) <-> A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) )
13	6 12	rabeqbidv	\|- ( ( J e. ( TopOn ` X ) /\ j = J ) -> { x e. ~P U. j \| A. k e. ~P U. j ( ( j \|`t k ) e. Comp -> ( x i^i k ) e. ( j \|`t k ) ) } = { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } )
14		topontop	\|- ( J e. ( TopOn ` X ) -> J e. Top )
15		toponmax	\|- ( J e. ( TopOn ` X ) -> X e. J )
16		pwexg	\|- ( X e. J -> ~P X e. _V )
17		rabexg	\|- ( ~P X e. _V -> { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } e. _V )
18	15 16 17	3syl	\|- ( J e. ( TopOn ` X ) -> { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } e. _V )
19	1 13 14 18	fvmptd2	\|- ( J e. ( TopOn ` X ) -> ( kGen ` J ) = { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } )