qtopss

Description: A surjective continuous function from J to K induces a topology J qTop F on the base set of K . This topology is in general finer than K . Together with qtopid , this implies that J qTop F is the finest topology making F continuous, i.e. the final topology with respect to the family { F } . (Contributed by Mario Carneiro, 24-Mar-2015)

		Ref	Expression
	Assertion	qtopss	$⊢ (F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \to K \subseteq J qTop F$

Proof

Step	Hyp	Ref	Expression
1		toponss	$⊢ (K \in TopOn (Y) \land x \in K) \to x \subseteq Y$
2	1	3ad2antl2	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to x \subseteq Y$
3		cnima	$⊢ (F \in (J Cn K) \land x \in K) \to F^{-1} [x] \in J$
4	3	3ad2antl1	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to F^{-1} [x] \in J$
5		simpl1	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to F \in (J Cn K)$
6		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
7	5 6	syl	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to J \in Top$
8		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
9	7 8	sylib	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to J \in TopOn (⋃ J)$
10		simpl2	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to K \in TopOn (Y)$
11		cnf2	$⊢ (J \in TopOn (⋃ J) \land K \in TopOn (Y) \land F \in (J Cn K)) \to F : ⋃ J ⟶ Y$
12	9 10 5 11	syl3anc	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to F : ⋃ J ⟶ Y$
13	12	ffnd	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to F Fn ⋃ J$
14		simpl3	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to ran F = Y$
15		df-fo	$⊢ F : ⋃ J \underset{onto}{⟶} Y \leftrightarrow (F Fn ⋃ J \land ran F = Y)$
16	13 14 15	sylanbrc	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to F : ⋃ J \underset{onto}{⟶} Y$
17		elqtop3	$⊢ (J \in TopOn (⋃ J) \land F : ⋃ J \underset{onto}{⟶} Y) \to (x \in (J qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in J))$
18	9 16 17	syl2anc	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to (x \in (J qTop F) \leftrightarrow (x \subseteq Y \land F^{-1} [x] \in J))$
19	2 4 18	mpbir2and	$⊢ ((F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \land x \in K) \to x \in (J qTop F)$
20	19	ex	$⊢ (F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \to (x \in K \to x \in (J qTop F))$
21	20	ssrdv	$⊢ (F \in (J Cn K) \land K \in TopOn (Y) \land ran F = Y) \to K \subseteq J qTop F$

Metamath Proof Explorer

Theorem qtopss

Proof