# Metamath Proof Explorer

## Theorem kgeni

Description: Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgeni
`|- ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i K ) e. ( J |`t K ) )`

### Proof

Step Hyp Ref Expression
1 inass
` |-  ( ( A i^i K ) i^i U. J ) = ( A i^i ( K i^i U. J ) )`
2 in32
` |-  ( ( A i^i K ) i^i U. J ) = ( ( A i^i U. J ) i^i K )`
3 1 2 eqtr3i
` |-  ( A i^i ( K i^i U. J ) ) = ( ( A i^i U. J ) i^i K )`
4 df-kgen
` |-  kGen = ( j e. Top |-> { x e. ~P U. j | A. y e. ~P U. j ( ( j |`t y ) e. Comp -> ( x i^i y ) e. ( j |`t y ) ) } )`
5 4 mptrcl
` |-  ( A e. ( kGen ` J ) -> J e. Top )`
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> J e. Top )`
7 toptopon2
` |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )`
8 6 7 sylib
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> J e. ( TopOn ` U. J ) )`
9 simpl
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> A e. ( kGen ` J ) )`
10 elkgen
` |-  ( J e. ( TopOn ` U. J ) -> ( A e. ( kGen ` J ) <-> ( A C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( A i^i y ) e. ( J |`t y ) ) ) ) )`
11 10 biimpa
` |-  ( ( J e. ( TopOn ` U. J ) /\ A e. ( kGen ` J ) ) -> ( A C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( A i^i y ) e. ( J |`t y ) ) ) )`
12 8 9 11 syl2anc
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( A i^i y ) e. ( J |`t y ) ) ) )`
13 12 simpld
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> A C_ U. J )`
14 df-ss
` |-  ( A C_ U. J <-> ( A i^i U. J ) = A )`
15 13 14 sylib
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i U. J ) = A )`
16 15 ineq1d
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( ( A i^i U. J ) i^i K ) = ( A i^i K ) )`
17 3 16 syl5eq
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i ( K i^i U. J ) ) = ( A i^i K ) )`
18 cmptop
` |-  ( ( J |`t K ) e. Comp -> ( J |`t K ) e. Top )`
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) e. Top )`
20 restrcl
` |-  ( ( J |`t K ) e. Top -> ( J e. _V /\ K e. _V ) )`
21 20 simprd
` |-  ( ( J |`t K ) e. Top -> K e. _V )`
22 19 21 syl
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> K e. _V )`
23 eqid
` |-  U. J = U. J`
24 23 restin
` |-  ( ( J e. Top /\ K e. _V ) -> ( J |`t K ) = ( J |`t ( K i^i U. J ) ) )`
25 6 22 24 syl2anc
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) = ( J |`t ( K i^i U. J ) ) )`
26 simpr
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( J |`t K ) e. Comp )`
27 25 26 eqeltrrd
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( J |`t ( K i^i U. J ) ) e. Comp )`
28 oveq2
` |-  ( y = ( K i^i U. J ) -> ( J |`t y ) = ( J |`t ( K i^i U. J ) ) )`
29 28 eleq1d
` |-  ( y = ( K i^i U. J ) -> ( ( J |`t y ) e. Comp <-> ( J |`t ( K i^i U. J ) ) e. Comp ) )`
30 ineq2
` |-  ( y = ( K i^i U. J ) -> ( A i^i y ) = ( A i^i ( K i^i U. J ) ) )`
31 30 28 eleq12d
` |-  ( y = ( K i^i U. J ) -> ( ( A i^i y ) e. ( J |`t y ) <-> ( A i^i ( K i^i U. J ) ) e. ( J |`t ( K i^i U. J ) ) ) )`
32 29 31 imbi12d
` |-  ( y = ( K i^i U. J ) -> ( ( ( J |`t y ) e. Comp -> ( A i^i y ) e. ( J |`t y ) ) <-> ( ( J |`t ( K i^i U. J ) ) e. Comp -> ( A i^i ( K i^i U. J ) ) e. ( J |`t ( K i^i U. J ) ) ) ) )`
33 12 simprd
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( A i^i y ) e. ( J |`t y ) ) )`
34 inss2
` |-  ( K i^i U. J ) C_ U. J`
35 inex1g
` |-  ( K e. _V -> ( K i^i U. J ) e. _V )`
36 elpwg
` |-  ( ( K i^i U. J ) e. _V -> ( ( K i^i U. J ) e. ~P U. J <-> ( K i^i U. J ) C_ U. J ) )`
37 22 35 36 3syl
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( ( K i^i U. J ) e. ~P U. J <-> ( K i^i U. J ) C_ U. J ) )`
38 34 37 mpbiri
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( K i^i U. J ) e. ~P U. J )`
39 32 33 38 rspcdva
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( ( J |`t ( K i^i U. J ) ) e. Comp -> ( A i^i ( K i^i U. J ) ) e. ( J |`t ( K i^i U. J ) ) ) )`
40 27 39 mpd
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i ( K i^i U. J ) ) e. ( J |`t ( K i^i U. J ) ) )`
41 17 40 eqeltrrd
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i K ) e. ( J |`t ( K i^i U. J ) ) )`
42 41 25 eleqtrrd
` |-  ( ( A e. ( kGen ` J ) /\ ( J |`t K ) e. Comp ) -> ( A i^i K ) e. ( J |`t K ) )`