# 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 ) ) )`