qtoptop

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Hypothesis	qtoptop.1	$⊢ X = ⋃ J$
	Assertion	qtoptop	$⊢ (J \in Top \land F Fn X) \to J qTop F \in Top$

Step	Hyp	Ref	Expression
1		qtoptop.1	$⊢ X = ⋃ J$
2		simpl	$⊢ (J \in Top \land F Fn X) \to J \in Top$
3		id	$⊢ F Fn X \to F Fn X$
4	1	topopn	$⊢ J \in Top \to X \in J$
5		fnex	$⊢ (F Fn X \land X \in J) \to F \in V$
6	3 4 5	syl2anr	$⊢ (J \in Top \land F Fn X) \to F \in V$
7		fnfun	$⊢ F Fn X \to Fun F$
8	7	adantl	$⊢ (J \in Top \land F Fn X) \to Fun F$
9		qtoptop2	$⊢ (J \in Top \land F \in V \land Fun F) \to J qTop F \in Top$
10	2 6 8 9	syl3anc	$⊢ (J \in Top \land F Fn X) \to J qTop F \in Top$

Metamath Proof Explorer