Metamath Proof Explorer

Theorem qtopval

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

Ref Expression
Hypothesis qtopval.1 
|- X = U. J
Assertion qtopval 
|- ( ( J e. V /\ F e. W ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )

Proof

Step Hyp Ref Expression
1 qtopval.1 
 |-  X = U. J
2 elex 
 |-  ( J e. V -> J e. _V )
3 elex 
 |-  ( F e. W -> F e. _V )
4 imaexg 
 |-  ( F e. _V -> ( F " X ) e. _V )
5 pwexg 
 |-  ( ( F " X ) e. _V -> ~P ( F " X ) e. _V )
6 rabexg 
 |-  ( ~P ( F " X ) e. _V -> { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } e. _V )
7 4 5 6 3syl 
 |-  ( F e. _V -> { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } e. _V )
8 7 adantl 
 |-  ( ( J e. _V /\ F e. _V ) -> { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } e. _V )
9 simpr 
 |-  ( ( j = J /\ f = F ) -> f = F )
10 simpl 
 |-  ( ( j = J /\ f = F ) -> j = J )
11 10 unieqd 
 |-  ( ( j = J /\ f = F ) -> U. j = U. J )
12 11 1 eqtr4di 
 |-  ( ( j = J /\ f = F ) -> U. j = X )
13 9 12 imaeq12d 
 |-  ( ( j = J /\ f = F ) -> ( f " U. j ) = ( F " X ) )
14 13 pweqd 
 |-  ( ( j = J /\ f = F ) -> ~P ( f " U. j ) = ~P ( F " X ) )
15 9 cnveqd 
 |-  ( ( j = J /\ f = F ) -> `' f = `' F )
16 15 imaeq1d 
 |-  ( ( j = J /\ f = F ) -> ( `' f " s ) = ( `' F " s ) )
17 16 12 ineq12d 
 |-  ( ( j = J /\ f = F ) -> ( ( `' f " s ) i^i U. j ) = ( ( `' F " s ) i^i X ) )
18 17 10 eleq12d 
 |-  ( ( j = J /\ f = F ) -> ( ( ( `' f " s ) i^i U. j ) e. j <-> ( ( `' F " s ) i^i X ) e. J ) )
19 14 18 rabeqbidv 
 |-  ( ( j = J /\ f = F ) -> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
20 df-qtop 
 |-  qTop = ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )
21 19 20 ovmpoga 
 |-  ( ( J e. _V /\ F e. _V /\ { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } e. _V ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
22 8 21 mpd3an3 
 |-  ( ( J e. _V /\ F e. _V ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
23 2 3 22 syl2an 
 |-  ( ( J e. V /\ F e. W ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )