Metamath Proof Explorer

Theorem qtopss

Description: A surjective continuous function from J to K induces a topology J qTop F on the base set of K . This topology is in general finer than K . Together with qtopid , this implies that J qTop F is the finest topology making F continuous, i.e. the final topology with respect to the family { F } . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion qtopss 
|- ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) -> K C_ ( J qTop F ) )

Proof

Step Hyp Ref Expression
1 toponss 
 |-  ( ( K e. ( TopOn ` Y ) /\ x e. K ) -> x C_ Y )
2 1 3ad2antl2 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> x C_ Y )
3 cnima 
 |-  ( ( F e. ( J Cn K ) /\ x e. K ) -> ( `' F " x ) e. J )
4 3 3ad2antl1 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> ( `' F " x ) e. J )
5 simpl1 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> F e. ( J Cn K ) )
6 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
7 5 6 syl 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> J e. Top )
8 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
9 7 8 sylib 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> J e. ( TopOn ` U. J ) )
10 simpl2 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> K e. ( TopOn ` Y ) )
11 cnf2 
 |-  ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : U. J --> Y )
12 9 10 5 11 syl3anc 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> F : U. J --> Y )
13 12 ffnd 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> F Fn U. J )
14 simpl3 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> ran F = Y )
15 df-fo 
 |-  ( F : U. J -onto-> Y <-> ( F Fn U. J /\ ran F = Y ) )
16 13 14 15 sylanbrc 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> F : U. J -onto-> Y )
17 elqtop3 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F : U. J -onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
18 9 16 17 syl2anc 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
19 2 4 18 mpbir2and 
 |-  ( ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) /\ x e. K ) -> x e. ( J qTop F ) )
20 19 ex 
 |-  ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) -> ( x e. K -> x e. ( J qTop F ) ) )
21 20 ssrdv 
 |-  ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) -> K C_ ( J qTop F ) )