qtopcld

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

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

Proof

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

Metamath Proof Explorer

Theorem qtopcld

Proof