qtopid

Description: A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Assertion	qtopid	$⊢ (J \in TopOn (X) \land F Fn X) \to F \in (J Cn (J qTop F))$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in TopOn (X) \land F Fn X) \to F Fn X$
2		dffn4	$⊢ F Fn X \leftrightarrow F : X \underset{onto}{⟶} ran F$
3	1 2	sylib	$⊢ (J \in TopOn (X) \land F Fn X) \to F : X \underset{onto}{⟶} ran F$
4		fof	$⊢ F : X \underset{onto}{⟶} ran F \to F : X ⟶ ran F$
5	3 4	syl	$⊢ (J \in TopOn (X) \land F Fn X) \to F : X ⟶ ran F$
6		elqtop3	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} ran F) \to (x \in (J qTop F) \leftrightarrow (x \subseteq ran F \land F^{-1} [x] \in J))$
7	3 6	syldan	$⊢ (J \in TopOn (X) \land F Fn X) \to (x \in (J qTop F) \leftrightarrow (x \subseteq ran F \land F^{-1} [x] \in J))$
8	7	simplbda	$⊢ ((J \in TopOn (X) \land F Fn X) \land x \in (J qTop F)) \to F^{-1} [x] \in J$
9	8	ralrimiva	$⊢ (J \in TopOn (X) \land F Fn X) \to \forall x \in (J qTop F) F^{-1} [x] \in J$
10		qtoptopon	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} ran F) \to J qTop F \in TopOn (ran F)$
11	3 10	syldan	$⊢ (J \in TopOn (X) \land F Fn X) \to J qTop F \in TopOn (ran F)$
12		iscn	$⊢ (J \in TopOn (X) \land J qTop F \in TopOn (ran F)) \to (F \in (J Cn (J qTop F)) \leftrightarrow (F : X ⟶ ran F \land \forall x \in (J qTop F) F^{-1} [x] \in J))$
13	11 12	syldan	$⊢ (J \in TopOn (X) \land F Fn X) \to (F \in (J Cn (J qTop F)) \leftrightarrow (F : X ⟶ ran F \land \forall x \in (J qTop F) F^{-1} [x] \in J))$
14	5 9 13	mpbir2and	$⊢ (J \in TopOn (X) \land F Fn X) \to F \in (J Cn (J qTop F))$

Metamath Proof Explorer