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 4 9 fexd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> F e. _V )
11 1 qtopval 
 |-  ( ( J e. V /\ F e. _V ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
12 2 10 11 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 } )
13 imassrn 
 |-  ( F " X ) C_ ran F
14 forn 
 |-  ( F : Z -onto-> Y -> ran F = Y )
15 14 3ad2ant2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ran F = Y )
16 13 15 sseqtrid 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " X ) C_ Y )
17 foima 
 |-  ( F : Z -onto-> Y -> ( F " Z ) = Y )
18 17 3ad2ant2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " Z ) = Y )
19 imass2 
 |-  ( Z C_ X -> ( F " Z ) C_ ( F " X ) )
20 8 19 syl 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " Z ) C_ ( F " X ) )
21 18 20 eqsstrrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Y C_ ( F " X ) )
22 16 21 eqssd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( F " X ) = Y )
23 22 pweqd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ~P ( F " X ) = ~P Y )
24 cnvimass 
 |-  ( `' F " s ) C_ dom F
25 24 4 fssdm 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( `' F " s ) C_ Z )
26 25 8 sstrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( `' F " s ) C_ X )
27 dfss2 
 |-  ( ( `' F " s ) C_ X <-> ( ( `' F " s ) i^i X ) = ( `' F " s ) )
28 26 27 sylib 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( ( `' F " s ) i^i X ) = ( `' F " s ) )
29 28 eleq1d 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( ( ( `' F " s ) i^i X ) e. J <-> ( `' F " s ) e. J ) )
30 23 29 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 } )
31 12 30 eqtrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P Y | ( `' F " s ) e. J } )