Metamath Proof Explorer

Theorem elqtop

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 
|- X = U. J
Assertion elqtop 
|- ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )

Proof

Step Hyp Ref Expression
1 qtopval.1 
 |-  X = U. J
2 1 qtopval2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( J qTop F ) = { s e. ~P Y | ( `' F " s ) e. J } )
3 2 eleq2d 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. ( J qTop F ) <-> A e. { s e. ~P Y | ( `' F " s ) e. J } ) )
4 imaeq2 
 |-  ( s = A -> ( `' F " s ) = ( `' F " A ) )
5 4 eleq1d 
 |-  ( s = A -> ( ( `' F " s ) e. J <-> ( `' F " A ) e. J ) )
6 5 elrab 
 |-  ( A e. { s e. ~P Y | ( `' F " s ) e. J } <-> ( A e. ~P Y /\ ( `' F " A ) e. J ) )
7 uniexg 
 |-  ( J e. V -> U. J e. _V )
8 1 7 eqeltrid 
 |-  ( J e. V -> X e. _V )
9 8 3ad2ant1 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> X e. _V )
10 simp3 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Z C_ X )
11 9 10 ssexd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Z e. _V )
12 simp2 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> F : Z -onto-> Y )
13 fornex 
 |-  ( Z e. _V -> ( F : Z -onto-> Y -> Y e. _V ) )
14 11 12 13 sylc 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> Y e. _V )
15 elpw2g 
 |-  ( Y e. _V -> ( A e. ~P Y <-> A C_ Y ) )
16 14 15 syl 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. ~P Y <-> A C_ Y ) )
17 16 anbi1d 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( ( A e. ~P Y /\ ( `' F " A ) e. J ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
18 6 17 syl5bb 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. { s e. ~P Y | ( `' F " s ) e. J } <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
19 3 18 bitrd 
 |-  ( ( J e. V /\ F : Z -onto-> Y /\ Z C_ X ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )