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 )
6 5 adantr 
 |-  ( ( 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 )
19 18 adantl 
 |-  ( ( 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 ) )