# Metamath Proof Explorer

## Theorem qtopcld

Description: The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion qtopcld ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({A}\in \mathrm{Clsd}\left({J}\mathrm{qTop}{F}\right)↔\left({A}\subseteq {Y}\wedge {{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 qtoptopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to {J}\mathrm{qTop}{F}\in \mathrm{TopOn}\left({Y}\right)$
2 topontop ${⊢}{J}\mathrm{qTop}{F}\in \mathrm{TopOn}\left({Y}\right)\to {J}\mathrm{qTop}{F}\in \mathrm{Top}$
3 eqid ${⊢}\bigcup \left({J}\mathrm{qTop}{F}\right)=\bigcup \left({J}\mathrm{qTop}{F}\right)$
4 3 iscld ${⊢}{J}\mathrm{qTop}{F}\in \mathrm{Top}\to \left({A}\in \mathrm{Clsd}\left({J}\mathrm{qTop}{F}\right)↔\left({A}\subseteq \bigcup \left({J}\mathrm{qTop}{F}\right)\wedge \bigcup \left({J}\mathrm{qTop}{F}\right)\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)\right)$
5 1 2 4 3syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({A}\in \mathrm{Clsd}\left({J}\mathrm{qTop}{F}\right)↔\left({A}\subseteq \bigcup \left({J}\mathrm{qTop}{F}\right)\wedge \bigcup \left({J}\mathrm{qTop}{F}\right)\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)\right)$
6 toponuni ${⊢}{J}\mathrm{qTop}{F}\in \mathrm{TopOn}\left({Y}\right)\to {Y}=\bigcup \left({J}\mathrm{qTop}{F}\right)$
7 1 6 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to {Y}=\bigcup \left({J}\mathrm{qTop}{F}\right)$
8 7 sseq2d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({A}\subseteq {Y}↔{A}\subseteq \bigcup \left({J}\mathrm{qTop}{F}\right)\right)$
9 7 difeq1d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to {Y}\setminus {A}=\bigcup \left({J}\mathrm{qTop}{F}\right)\setminus {A}$
10 9 eleq1d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)↔\bigcup \left({J}\mathrm{qTop}{F}\right)\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)$
11 8 10 anbi12d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left(\left({A}\subseteq {Y}\wedge {Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)↔\left({A}\subseteq \bigcup \left({J}\mathrm{qTop}{F}\right)\wedge \bigcup \left({J}\mathrm{qTop}{F}\right)\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)\right)$
12 elqtop3 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)↔\left({Y}\setminus {A}\subseteq {Y}\wedge {{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}\right)\right)$
13 12 adantr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)↔\left({Y}\setminus {A}\subseteq {Y}\wedge {{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}\right)\right)$
14 difss ${⊢}{Y}\setminus {A}\subseteq {Y}$
15 14 biantrur ${⊢}{{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}↔\left({Y}\setminus {A}\subseteq {Y}\wedge {{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}\right)$
16 fofun ${⊢}{F}:{X}\underset{onto}{⟶}{Y}\to \mathrm{Fun}{F}$
17 16 ad2antlr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \mathrm{Fun}{F}$
18 funcnvcnv ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
19 imadif ${⊢}\mathrm{Fun}{{{F}}^{-1}}^{-1}\to {{F}}^{-1}\left[{Y}\setminus {A}\right]={{F}}^{-1}\left[{Y}\right]\setminus {{F}}^{-1}\left[{A}\right]$
20 17 18 19 3syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{Y}\setminus {A}\right]={{F}}^{-1}\left[{Y}\right]\setminus {{F}}^{-1}\left[{A}\right]$
21 fof ${⊢}{F}:{X}\underset{onto}{⟶}{Y}\to {F}:{X}⟶{Y}$
22 fimacnv ${⊢}{F}:{X}⟶{Y}\to {{F}}^{-1}\left[{Y}\right]={X}$
23 21 22 syl ${⊢}{F}:{X}\underset{onto}{⟶}{Y}\to {{F}}^{-1}\left[{Y}\right]={X}$
24 23 ad2antlr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{Y}\right]={X}$
25 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
26 25 ad2antrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {X}=\bigcup {J}$
27 24 26 eqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{Y}\right]=\bigcup {J}$
28 27 difeq1d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{Y}\right]\setminus {{F}}^{-1}\left[{A}\right]=\bigcup {J}\setminus {{F}}^{-1}\left[{A}\right]$
29 20 28 eqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{Y}\setminus {A}\right]=\bigcup {J}\setminus {{F}}^{-1}\left[{A}\right]$
30 29 eleq1d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}↔\bigcup {J}\setminus {{F}}^{-1}\left[{A}\right]\in {J}\right)$
31 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
32 31 ad2antrr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {J}\in \mathrm{Top}$
33 cnvimass ${⊢}{{F}}^{-1}\left[{A}\right]\subseteq \mathrm{dom}{F}$
34 fofn ${⊢}{F}:{X}\underset{onto}{⟶}{Y}\to {F}Fn{X}$
35 fndm ${⊢}{F}Fn{X}\to \mathrm{dom}{F}={X}$
36 34 35 syl ${⊢}{F}:{X}\underset{onto}{⟶}{Y}\to \mathrm{dom}{F}={X}$
37 36 ad2antlr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \mathrm{dom}{F}={X}$
38 33 37 sseqtrid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{A}\right]\subseteq {X}$
39 38 26 sseqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to {{F}}^{-1}\left[{A}\right]\subseteq \bigcup {J}$
40 eqid ${⊢}\bigcup {J}=\bigcup {J}$
41 40 iscld2 ${⊢}\left({J}\in \mathrm{Top}\wedge {{F}}^{-1}\left[{A}\right]\subseteq \bigcup {J}\right)\to \left({{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)↔\bigcup {J}\setminus {{F}}^{-1}\left[{A}\right]\in {J}\right)$
42 32 39 41 syl2anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)↔\bigcup {J}\setminus {{F}}^{-1}\left[{A}\right]\in {J}\right)$
43 30 42 bitr4d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}↔{{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)$
44 15 43 syl5bbr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left(\left({Y}\setminus {A}\subseteq {Y}\wedge {{F}}^{-1}\left[{Y}\setminus {A}\right]\in {J}\right)↔{{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)$
45 13 44 bitrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\wedge {A}\subseteq {Y}\right)\to \left({Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)↔{{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)$
46 45 pm5.32da ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left(\left({A}\subseteq {Y}\wedge {Y}\setminus {A}\in \left({J}\mathrm{qTop}{F}\right)\right)↔\left({A}\subseteq {Y}\wedge {{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$
47 5 11 46 3bitr2d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {F}:{X}\underset{onto}{⟶}{Y}\right)\to \left({A}\in \mathrm{Clsd}\left({J}\mathrm{qTop}{F}\right)↔\left({A}\subseteq {Y}\wedge {{F}}^{-1}\left[{A}\right]\in \mathrm{Clsd}\left({J}\right)\right)\right)$