Theorem elkgen

Description: Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

	Ref	Expression
Assertion	elkgen	|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> ( A C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) } )
2	1	eleq2d	|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> A e. { x e. ~P X | A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) } ) )
3		ineq1	|- ( x = A -> ( x i^i k ) = ( A i^i k ) )
4	3	eleq1d	|- ( x = A -> ( ( x i^i k ) e. ( J |`t k ) <-> ( A i^i k ) e. ( J |`t k ) ) )
5	4	imbi2d	|- ( x = A -> ( ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) <-> ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) )
6	5	ralbidv	|- ( x = A -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) <-> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) )
7	6	elrab	|- ( A e. { x e. ~P X | A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) } <-> ( A e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) )
8		toponmax	|- ( J e. ( TopOn ` X ) -> X e. J )
9		elpw2g	|- ( X e. J -> ( A e. ~P X <-> A C_ X ) )
10	8 9	syl	|- ( J e. ( TopOn ` X ) -> ( A e. ~P X <-> A C_ X ) )
11	10	anbi1d	|- ( J e. ( TopOn ` X ) -> ( ( A e. ~P X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) <-> ( A C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) ) )
12	7 11	syl5bb	|- ( J e. ( TopOn ` X ) -> ( A e. { x e. ~P X | A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) } <-> ( A C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) ) )
13	2 12	bitrd	|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> ( A C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( A i^i k ) e. ( J |`t k ) ) ) ) )