Metamath Proof Explorer

Theorem qtopval2

Description: Value of the quotient topology function when F is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 
|- X = U. J
Assertion qtopval2 
|- ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P Y | ( `' F " s ) e. J } )

Proof

Step Hyp Ref Expression
1 qtopval.1 
 |-  X = U. J
2 simp1 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> J e. V )
3 fof 
 |-  ( F : Z -onto-> Y -> F : Z --> Y )
4 3 3ad2ant2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> F : Z --> Y )
5 uniexg 
 |-  ( J e. V -> U. J e. _V )
6 5 3ad2ant1 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> U. J e. _V )
7 1 6 eqeltrid 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> X e. _V )
8 simp3 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Z C_ X )
9 7 8 ssexd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Z e. _V )
10 fex 
 |-  ( ( F : Z --> Y /\ Z e. _V ) -> F e. _V )
11 4 9 10 syl2anc 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> F e. _V )
12 1 qtopval 
 |-  ( ( J e. V /\ F e. _V ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
13 2 11 12 syl2anc 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
14 imassrn 
 |-  ( F " X ) C_ ran F
15 forn 
 |-  ( F : Z -onto-> Y -> ran F = Y )
16 15 3ad2ant2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ran F = Y )
17 14 16 sseqtrid 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " X ) C_ Y )
18 foima 
 |-  ( F : Z -onto-> Y -> ( F " Z ) = Y )
19 18 3ad2ant2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " Z ) = Y )
20 imass2 
 |-  ( Z C_ X -> ( F " Z ) C_ ( F " X ) )
21 8 20 syl 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " Z ) C_ ( F " X ) )
22 19 21 eqsstrrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Y C_ ( F " X ) )
23 17 22 eqssd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " X ) = Y )
24 23 pweqd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ~P ( F " X ) = ~P Y )
25 cnvimass 
 |-  ( `' F " s ) C_ dom F
26 25 4 fssdm 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( `' F " s ) C_ Z )
27 26 8 sstrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( `' F " s ) C_ X )
28 df-ss 
 |-  ( ( `' F " s ) C_ X <-> ( ( `' F " s ) i^i X ) = ( `' F " s ) )
29 27 28 sylib 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( ( `' F " s ) i^i X ) = ( `' F " s ) )
30 29 eleq1d 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( ( ( `' F " s ) i^i X ) e. J <-> ( `' F " s ) e. J ) )
31 24 30 rabeqbidv 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } = { s e. ~P Y | ( `' F " s ) e. J } )
32 13 31 eqtrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P Y | ( `' F " s ) e. J } )