# Metamath Proof Explorer

## Theorem kgen2ss

Description: The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgen2ss
`|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( kGen ` J ) C_ ( kGen ` K ) )`

### Proof

Step Hyp Ref Expression
1 simp1
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. ( TopOn ` X ) )`
2 elpwi
` |-  ( k e. ~P X -> k C_ X )`
3 resttopon
` |-  ( ( J e. ( TopOn ` X ) /\ k C_ X ) -> ( J |`t k ) e. ( TopOn ` k ) )`
4 1 2 3 syl2an
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( J |`t k ) e. ( TopOn ` k ) )`
5 simp2
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. ( TopOn ` X ) )`
6 resttopon
` |-  ( ( K e. ( TopOn ` X ) /\ k C_ X ) -> ( K |`t k ) e. ( TopOn ` k ) )`
7 5 2 6 syl2an
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( K |`t k ) e. ( TopOn ` k ) )`
8 toponuni
` |-  ( ( K |`t k ) e. ( TopOn ` k ) -> k = U. ( K |`t k ) )`
9 7 8 syl
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> k = U. ( K |`t k ) )`
10 9 fveq2d
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( TopOn ` k ) = ( TopOn ` U. ( K |`t k ) ) )`
11 4 10 eleqtrd
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( J |`t k ) e. ( TopOn ` U. ( K |`t k ) ) )`
12 simpl2
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> K e. ( TopOn ` X ) )`
13 topontop
` |-  ( K e. ( TopOn ` X ) -> K e. Top )`
14 12 13 syl
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> K e. Top )`
15 simpl3
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> J C_ K )`
16 ssrest
` |-  ( ( K e. Top /\ J C_ K ) -> ( J |`t k ) C_ ( K |`t k ) )`
17 14 15 16 syl2anc
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( J |`t k ) C_ ( K |`t k ) )`
18 eqid
` |-  U. ( K |`t k ) = U. ( K |`t k )`
19 18 sscmp
` |-  ( ( ( J |`t k ) e. ( TopOn ` U. ( K |`t k ) ) /\ ( K |`t k ) e. Comp /\ ( J |`t k ) C_ ( K |`t k ) ) -> ( J |`t k ) e. Comp )`
20 19 3com23
` |-  ( ( ( J |`t k ) e. ( TopOn ` U. ( K |`t k ) ) /\ ( J |`t k ) C_ ( K |`t k ) /\ ( K |`t k ) e. Comp ) -> ( J |`t k ) e. Comp )`
21 20 3expia
` |-  ( ( ( J |`t k ) e. ( TopOn ` U. ( K |`t k ) ) /\ ( J |`t k ) C_ ( K |`t k ) ) -> ( ( K |`t k ) e. Comp -> ( J |`t k ) e. Comp ) )`
22 11 17 21 syl2anc
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( ( K |`t k ) e. Comp -> ( J |`t k ) e. Comp ) )`
23 17 sseld
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( ( x i^i k ) e. ( J |`t k ) -> ( x i^i k ) e. ( K |`t k ) ) )`
24 22 23 imim12d
` |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) /\ k e. ~P X ) -> ( ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> ( ( K |`t k ) e. Comp -> ( x i^i k ) e. ( K |`t k ) ) ) )`
25 24 ralimdva
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) -> A. k e. ~P X ( ( K |`t k ) e. Comp -> ( x i^i k ) e. ( K |`t k ) ) ) )`
26 25 anim2d
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) -> ( x C_ X /\ A. k e. ~P X ( ( K |`t k ) e. Comp -> ( x i^i k ) e. ( K |`t k ) ) ) ) )`
27 elkgen
` |-  ( J e. ( TopOn ` X ) -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )`
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( x i^i k ) e. ( J |`t k ) ) ) ) )`
` |-  ( K e. ( TopOn ` X ) -> ( x e. ( kGen ` K ) <-> ( x C_ X /\ A. k e. ~P X ( ( K |`t k ) e. Comp -> ( x i^i k ) e. ( K |`t k ) ) ) ) )`
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( x e. ( kGen ` K ) <-> ( x C_ X /\ A. k e. ~P X ( ( K |`t k ) e. Comp -> ( x i^i k ) e. ( K |`t k ) ) ) ) )`
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( x e. ( kGen ` J ) -> x e. ( kGen ` K ) ) )`
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( kGen ` J ) C_ ( kGen ` K ) )`