qtopkgen

Description: A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Hypothesis	qtopcmp.1	$⊢ X = ⋃ J$
	Assertion	qtopkgen	$⊢ (J \in ran 𝑘Gen \land F Fn X) \to J qTop F \in ran 𝑘Gen$

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	$⊢ X = ⋃ J$
2		kgentop	$⊢ J \in ran 𝑘Gen \to J \in Top$
3	1	qtoptop	$⊢ (J \in Top \land F Fn X) \to J qTop F \in Top$
4	2 3	sylan	$⊢ (J \in ran 𝑘Gen \land F Fn X) \to J qTop F \in Top$
5		elssuni	$⊢ x \in 𝑘Gen (J qTop F) \to x \subseteq ⋃ 𝑘Gen (J qTop F)$
6	5	adantl	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to x \subseteq ⋃ 𝑘Gen (J qTop F)$
7	4	adantr	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to J qTop F \in Top$
8		eqid	$⊢ ⋃ (J qTop F) = ⋃ (J qTop F)$
9	8	kgenuni	$⊢ J qTop F \in Top \to ⋃ (J qTop F) = ⋃ 𝑘Gen (J qTop F)$
10	7 9	syl	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to ⋃ (J qTop F) = ⋃ 𝑘Gen (J qTop F)$
11	6 10	sseqtrrd	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to x \subseteq ⋃ (J qTop F)$
12		simpll	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to J \in ran 𝑘Gen$
13	12 2	syl	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to J \in Top$
14		simplr	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to F Fn X$
15		dffn4	$⊢ F Fn X \leftrightarrow F : X \underset{onto}{⟶} ran F$
16	14 15	sylib	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to F : X \underset{onto}{⟶} ran F$
17	1	qtopuni	$⊢ (J \in Top \land F : X \underset{onto}{⟶} ran F) \to ran F = ⋃ (J qTop F)$
18	13 16 17	syl2anc	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to ran F = ⋃ (J qTop F)$
19	11 18	sseqtrrd	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to x \subseteq ran F$
20	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
21	13 20	sylib	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to J \in TopOn (X)$
22		qtopid	$⊢ (J \in TopOn (X) \land F Fn X) \to F \in (J Cn (J qTop F))$
23	21 14 22	syl2anc	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to F \in (J Cn (J qTop F))$
24		kgencn3	$⊢ (J \in ran 𝑘Gen \land J qTop F \in Top) \to J Cn (J qTop F) = J Cn 𝑘Gen (J qTop F)$
25	12 7 24	syl2anc	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to J Cn (J qTop F) = J Cn 𝑘Gen (J qTop F)$
26	23 25	eleqtrd	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to F \in (J Cn 𝑘Gen (J qTop F))$
27		cnima	$⊢ (F \in (J Cn 𝑘Gen (J qTop F)) \land x \in 𝑘Gen (J qTop F)) \to F^{-1} [x] \in J$
28	26 27	sylancom	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to F^{-1} [x] \in J$
29	1	elqtop2	$⊢ (J \in ran 𝑘Gen \land F : X \underset{onto}{⟶} ran F) \to (x \in (J qTop F) \leftrightarrow (x \subseteq ran F \land F^{-1} [x] \in J))$
30	12 16 29	syl2anc	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to (x \in (J qTop F) \leftrightarrow (x \subseteq ran F \land F^{-1} [x] \in J))$
31	19 28 30	mpbir2and	$⊢ ((J \in ran 𝑘Gen \land F Fn X) \land x \in 𝑘Gen (J qTop F)) \to x \in (J qTop F)$
32	31	ex	$⊢ (J \in ran 𝑘Gen \land F Fn X) \to (x \in 𝑘Gen (J qTop F) \to x \in (J qTop F))$
33	32	ssrdv	$⊢ (J \in ran 𝑘Gen \land F Fn X) \to 𝑘Gen (J qTop F) \subseteq J qTop F$
34		iskgen2	$⊢ J qTop F \in ran 𝑘Gen \leftrightarrow (J qTop F \in Top \land 𝑘Gen (J qTop F) \subseteq J qTop F)$
35	4 33 34	sylanbrc	$⊢ (J \in ran 𝑘Gen \land F Fn X) \to J qTop F \in ran 𝑘Gen$

Metamath Proof Explorer

Theorem qtopkgen

Proof