qtoptopon

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

		Ref	Expression
	Assertion	qtoptopon	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to J qTop F \in TopOn (Y)$

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
3		foeq2	$⊢ X = ⋃ J \to (F : X \underset{onto}{⟶} Y \leftrightarrow F : ⋃ J \underset{onto}{⟶} Y)$
4	2 3	syl	$⊢ J \in TopOn (X) \to (F : X \underset{onto}{⟶} Y \leftrightarrow F : ⋃ J \underset{onto}{⟶} Y)$
5	4	biimpa	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to F : ⋃ J \underset{onto}{⟶} Y$
6		fofn	$⊢ F : ⋃ J \underset{onto}{⟶} Y \to F Fn ⋃ J$
7	5 6	syl	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to F Fn ⋃ J$
8		eqid	$⊢ ⋃ J = ⋃ J$
9	8	qtoptop	$⊢ (J \in Top \land F Fn ⋃ J) \to J qTop F \in Top$
10	1 7 9	syl2an2r	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to J qTop F \in Top$
11	8	qtopuni	$⊢ (J \in Top \land F : ⋃ J \underset{onto}{⟶} Y) \to Y = ⋃ (J qTop F)$
12	1 5 11	syl2an2r	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to Y = ⋃ (J qTop F)$
13		istopon	$⊢ J qTop F \in TopOn (Y) \leftrightarrow (J qTop F \in Top \land Y = ⋃ (J qTop F))$
14	10 12 13	sylanbrc	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to J qTop F \in TopOn (Y)$

Metamath Proof Explorer