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 ) ) ) ) )
28 27 3ad2ant1 
 |-  ( ( 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 ) ) ) ) )
29 elkgen 
 |-  ( 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 ) ) ) ) )
30 29 3ad2ant2 
 |-  ( ( 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 ) ) ) ) )
31 26 28 30 3imtr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( x e. ( kGen ` J ) -> x e. ( kGen ` K ) ) )
32 31 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( kGen ` J ) C_ ( kGen ` K ) )