Metamath Proof Explorer

Theorem qtopres

Description: The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that F be a function with domain X . (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 
|- X = U. J
Assertion qtopres 
|- ( F e. V -> ( J qTop F ) = ( J qTop ( F |` X ) ) )

Proof

Step Hyp Ref Expression
1 qtopval.1 
 |-  X = U. J
2 resima 
 |-  ( ( F |` X ) " X ) = ( F " X )
3 2 pweqi 
 |-  ~P ( ( F |` X ) " X ) = ~P ( F " X )
4 3 rabeqi 
 |-  { s e. ~P ( ( F |` X ) " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J } = { s e. ~P ( F " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J }
5 residm 
 |-  ( ( F |` X ) |` X ) = ( F |` X )
6 5 cnveqi 
 |-  `' ( ( F |` X ) |` X ) = `' ( F |` X )
7 6 imaeq1i 
 |-  ( `' ( ( F |` X ) |` X ) " s ) = ( `' ( F |` X ) " s )
8 cnvresima 
 |-  ( `' ( ( F |` X ) |` X ) " s ) = ( ( `' ( F |` X ) " s ) i^i X )
9 cnvresima 
 |-  ( `' ( F |` X ) " s ) = ( ( `' F " s ) i^i X )
10 7 8 9 3eqtr3i 
 |-  ( ( `' ( F |` X ) " s ) i^i X ) = ( ( `' F " s ) i^i X )
11 10 eleq1i 
 |-  ( ( ( `' ( F |` X ) " s ) i^i X ) e. J <-> ( ( `' F " s ) i^i X ) e. J )
12 11 rabbii 
 |-  { s e. ~P ( F " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J } = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J }
13 4 12 eqtr2i 
 |-  { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } = { s e. ~P ( ( F |` X ) " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J }
14 1 qtopval 
 |-  ( ( J e. _V /\ F e. V ) -> ( J qTop F ) = { s e. ~P ( F " X ) | ( ( `' F " s ) i^i X ) e. J } )
15 resexg 
 |-  ( F e. V -> ( F |` X ) e. _V )
16 1 qtopval 
 |-  ( ( J e. _V /\ ( F |` X ) e. _V ) -> ( J qTop ( F |` X ) ) = { s e. ~P ( ( F |` X ) " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J } )
17 15 16 sylan2 
 |-  ( ( J e. _V /\ F e. V ) -> ( J qTop ( F |` X ) ) = { s e. ~P ( ( F |` X ) " X ) | ( ( `' ( F |` X ) " s ) i^i X ) e. J } )
18 13 14 17 3eqtr4a 
 |-  ( ( J e. _V /\ F e. V ) -> ( J qTop F ) = ( J qTop ( F |` X ) ) )
19 18 expcom 
 |-  ( F e. V -> ( J e. _V -> ( J qTop F ) = ( J qTop ( F |` X ) ) ) )
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 20 reldmmpo 
 |-  Rel dom qTop
22 21 ovprc1 
 |-  ( -. J e. _V -> ( J qTop F ) = (/) )
23 21 ovprc1 
 |-  ( -. J e. _V -> ( J qTop ( F |` X ) ) = (/) )
24 22 23 eqtr4d 
 |-  ( -. J e. _V -> ( J qTop F ) = ( J qTop ( F |` X ) ) )
25 19 24 pm2.61d1 
 |-  ( F e. V -> ( J qTop F ) = ( J qTop ( F |` X ) ) )