# Metamath Proof Explorer

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