qtopuni

Description: The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Hypothesis	qtoptop.1	$⊢ X = ⋃ J$
	Assertion	qtopuni	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y = ⋃ (J qTop F)$

Proof

Step	Hyp	Ref	Expression
1		qtoptop.1	$⊢ X = ⋃ J$
2		ssidd	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y \subseteq Y$
3		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
4	3	adantl	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to F : X ⟶ Y$
5		fimacnv	$⊢ F : X ⟶ Y \to F^{-1} [Y] = X$
6	4 5	syl	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to F^{-1} [Y] = X$
7	1	topopn	$⊢ J \in Top \to X \in J$
8	7	adantr	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to X \in J$
9	6 8	eqeltrd	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to F^{-1} [Y] \in J$
10	1	elqtop2	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to (Y \in (J qTop F) \leftrightarrow (Y \subseteq Y \land F^{-1} [Y] \in J))$
11	2 9 10	mpbir2and	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y \in (J qTop F)$
12		elssuni	$⊢ Y \in (J qTop F) \to Y \subseteq ⋃ (J qTop F)$
13	11 12	syl	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y \subseteq ⋃ (J qTop F)$
14	1	elqtop2	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to (x \in (J qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in J))$
15		simpl	$⊢ (x \subseteq Y \land F^{-1} [x] \in J) \to x \subseteq Y$
16		velpw	$⊢ x \in 𝒫 Y \leftrightarrow x \subseteq Y$
17	15 16	sylibr	$⊢ (x \subseteq Y \land F^{-1} [x] \in J) \to x \in 𝒫 Y$
18	14 17	syl6bi	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to (x \in (J qTop F) \to x \in 𝒫 Y)$
19	18	ssrdv	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to J qTop F \subseteq 𝒫 Y$
20		sspwuni	$⊢ J qTop F \subseteq 𝒫 Y \leftrightarrow ⋃ (J qTop F) \subseteq Y$
21	19 20	sylib	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to ⋃ (J qTop F) \subseteq Y$
22	13 21	eqssd	$⊢ (J \in Top \land F : X \underset{onto}{⟶} Y) \to Y = ⋃ (J qTop F)$

Metamath Proof Explorer

Theorem qtopuni

Proof