# 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}=\bigcup {J}$
Assertion qtopres ${⊢}{F}\in {V}\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)$

### Proof

Step Hyp Ref Expression
1 qtopval.1 ${⊢}{X}=\bigcup {J}$
2 resima ${⊢}\left({{F}↾}_{{X}}\right)\left[{X}\right]={F}\left[{X}\right]$
3 2 pweqi ${⊢}𝒫\left({{F}↾}_{{X}}\right)\left[{X}\right]=𝒫{F}\left[{X}\right]$
4 3 rabeqi ${⊢}\left\{{s}\in 𝒫\left({{F}↾}_{{X}}\right)\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
5 residm ${⊢}{\left({{F}↾}_{{X}}\right)↾}_{{X}}={{F}↾}_{{X}}$
6 5 cnveqi ${⊢}{\left({\left({{F}↾}_{{X}}\right)↾}_{{X}}\right)}^{-1}={\left({{F}↾}_{{X}}\right)}^{-1}$
7 6 imaeq1i ${⊢}{\left({\left({{F}↾}_{{X}}\right)↾}_{{X}}\right)}^{-1}\left[{s}\right]={\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]$
8 cnvresima ${⊢}{\left({\left({{F}↾}_{{X}}\right)↾}_{{X}}\right)}^{-1}\left[{s}\right]={\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}$
9 cnvresima ${⊢}{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]={{F}}^{-1}\left[{s}\right]\cap {X}$
10 7 8 9 3eqtr3i ${⊢}{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}={{F}}^{-1}\left[{s}\right]\cap {X}$
11 10 eleq1i ${⊢}{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}↔{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}$
12 11 rabbii ${⊢}\left\{{s}\in 𝒫{F}\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
13 4 12 eqtr2i ${⊢}\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}=\left\{{s}\in 𝒫\left({{F}↾}_{{X}}\right)\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
14 1 qtopval ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in {V}\right)\to {J}\mathrm{qTop}{F}=\left\{{s}\in 𝒫{F}\left[{X}\right]|{{F}}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
15 resexg ${⊢}{F}\in {V}\to {{F}↾}_{{X}}\in \mathrm{V}$
16 1 qtopval ${⊢}\left({J}\in \mathrm{V}\wedge {{F}↾}_{{X}}\in \mathrm{V}\right)\to {J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)=\left\{{s}\in 𝒫\left({{F}↾}_{{X}}\right)\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
17 15 16 sylan2 ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in {V}\right)\to {J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)=\left\{{s}\in 𝒫\left({{F}↾}_{{X}}\right)\left[{X}\right]|{\left({{F}↾}_{{X}}\right)}^{-1}\left[{s}\right]\cap {X}\in {J}\right\}$
18 13 14 17 3eqtr4a ${⊢}\left({J}\in \mathrm{V}\wedge {F}\in {V}\right)\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)$
19 18 expcom ${⊢}{F}\in {V}\to \left({J}\in \mathrm{V}\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)\right)$
20 df-qtop ${⊢}\mathrm{qTop}=\left({j}\in \mathrm{V},{f}\in \mathrm{V}⟼\left\{{s}\in 𝒫{f}\left[\bigcup {j}\right]|{{f}}^{-1}\left[{s}\right]\cap \bigcup {j}\in {j}\right\}\right)$
21 20 reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{qTop}$
22 21 ovprc1 ${⊢}¬{J}\in \mathrm{V}\to {J}\mathrm{qTop}{F}=\varnothing$
23 21 ovprc1 ${⊢}¬{J}\in \mathrm{V}\to {J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)=\varnothing$
24 22 23 eqtr4d ${⊢}¬{J}\in \mathrm{V}\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)$
25 19 24 pm2.61d1 ${⊢}{F}\in {V}\to {J}\mathrm{qTop}{F}={J}\mathrm{qTop}\left({{F}↾}_{{X}}\right)$