kgencn3

Description: The set of continuous functions from J to K is unaffected by k-ification of K , if J is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	kgencn3	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to J Cn K = J Cn 𝑘Gen (K)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnf	$⊢ f \in (J Cn K) \to f : ⋃ J ⟶ ⋃ K$
4	3	adantl	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to f : ⋃ J ⟶ ⋃ K$
5		cnvimass	$⊢ f^{-1} [x] \subseteq dom f$
6	4	fdmd	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to dom f = ⋃ J$
7	6	adantr	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to dom f = ⋃ J$
8	5 7	sseqtrid	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to f^{-1} [x] \subseteq ⋃ J$
9		cnvresima	$⊢ {({f ↾}_{y})}^{-1} [x \cap f [y]] = f^{-1} [x \cap f [y]] \cap y$
10	4	ad2antrr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f : ⋃ J ⟶ ⋃ K$
11		ffun	$⊢ f : ⋃ J ⟶ ⋃ K \to Fun f$
12		inpreima	$⊢ Fun f \to f^{-1} [x \cap f [y]] = f^{-1} [x] \cap f^{-1} [f [y]]$
13	10 11 12	3syl	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f^{-1} [x \cap f [y]] = f^{-1} [x] \cap f^{-1} [f [y]]$
14	13	ineq1d	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f^{-1} [x \cap f [y]] \cap y = (f^{-1} [x] \cap f^{-1} [f [y]]) \cap y$
15		in32	$⊢ (f^{-1} [x] \cap f^{-1} [f [y]]) \cap y = (f^{-1} [x] \cap y) \cap f^{-1} [f [y]]$
16		ssrin	$⊢ f^{-1} [x] \subseteq dom f \to f^{-1} [x] \cap y \subseteq dom f \cap y$
17	5 16	ax-mp	$⊢ f^{-1} [x] \cap y \subseteq dom f \cap y$
18		dminss	$⊢ dom f \cap y \subseteq f^{-1} [f [y]]$
19	17 18	sstri	$⊢ f^{-1} [x] \cap y \subseteq f^{-1} [f [y]]$
20	19	a1i	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f^{-1} [x] \cap y \subseteq f^{-1} [f [y]]$
21		df-ss	$⊢ f^{-1} [x] \cap y \subseteq f^{-1} [f [y]] \leftrightarrow (f^{-1} [x] \cap y) \cap f^{-1} [f [y]] = f^{-1} [x] \cap y$
22	20 21	sylib	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to (f^{-1} [x] \cap y) \cap f^{-1} [f [y]] = f^{-1} [x] \cap y$
23	15 22	syl5eq	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to (f^{-1} [x] \cap f^{-1} [f [y]]) \cap y = f^{-1} [x] \cap y$
24	14 23	eqtrd	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f^{-1} [x \cap f [y]] \cap y = f^{-1} [x] \cap y$
25	9 24	syl5eq	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to {({f ↾}_{y})}^{-1} [x \cap f [y]] = f^{-1} [x] \cap y$
26		simpr	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to f \in (J Cn K)$
27	26	ad2antrr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f \in (J Cn K)$
28		elpwi	$⊢ y \in 𝒫 ⋃ J \to y \subseteq ⋃ J$
29	28	ad2antrl	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to y \subseteq ⋃ J$
30	1	cnrest	$⊢ (f \in (J Cn K) \land y \subseteq ⋃ J) \to {f ↾}_{y} \in ((J ↾_{𝑡} y) Cn K)$
31	27 29 30	syl2anc	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to {f ↾}_{y} \in ((J ↾_{𝑡} y) Cn K)$
32		simpr	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to K \in Top$
33	32	ad3antrrr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to K \in Top$
34		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
35	33 34	sylib	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to K \in TopOn (⋃ K)$
36		df-ima	$⊢ f [y] = ran ({f ↾}_{y})$
37	36	eqimss2i	$⊢ ran ({f ↾}_{y}) \subseteq f [y]$
38	37	a1i	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to ran ({f ↾}_{y}) \subseteq f [y]$
39		imassrn	$⊢ f [y] \subseteq ran f$
40	10	frnd	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to ran f \subseteq ⋃ K$
41	39 40	sstrid	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f [y] \subseteq ⋃ K$
42		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran ({f ↾}_{y}) \subseteq f [y] \land f [y] \subseteq ⋃ K) \to ({f ↾}_{y} \in ((J ↾_{𝑡} y) Cn K) \leftrightarrow {f ↾}_{y} \in ((J ↾_{𝑡} y) Cn (K ↾_{𝑡} f [y])))$
43	35 38 41 42	syl3anc	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to ({f ↾}_{y} \in ((J ↾_{𝑡} y) Cn K) \leftrightarrow {f ↾}_{y} \in ((J ↾_{𝑡} y) Cn (K ↾_{𝑡} f [y])))$
44	31 43	mpbid	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to {f ↾}_{y} \in ((J ↾_{𝑡} y) Cn (K ↾_{𝑡} f [y]))$
45		simplr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to x \in 𝑘Gen (K)$
46		simprr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to J ↾_{𝑡} y \in Comp$
47		imacmp	$⊢ (f \in (J Cn K) \land J ↾_{𝑡} y \in Comp) \to K ↾_{𝑡} f [y] \in Comp$
48	27 46 47	syl2anc	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to K ↾_{𝑡} f [y] \in Comp$
49		kgeni	$⊢ (x \in 𝑘Gen (K) \land K ↾_{𝑡} f [y] \in Comp) \to x \cap f [y] \in (K ↾_{𝑡} f [y])$
50	45 48 49	syl2anc	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to x \cap f [y] \in (K ↾_{𝑡} f [y])$
51		cnima	$⊢ ({f ↾}_{y} \in ((J ↾_{𝑡} y) Cn (K ↾_{𝑡} f [y])) \land x \cap f [y] \in (K ↾_{𝑡} f [y])) \to {({f ↾}_{y})}^{-1} [x \cap f [y]] \in (J ↾_{𝑡} y)$
52	44 50 51	syl2anc	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to {({f ↾}_{y})}^{-1} [x \cap f [y]] \in (J ↾_{𝑡} y)$
53	25 52	eqeltrrd	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land (y \in 𝒫 ⋃ J \land J ↾_{𝑡} y \in Comp)) \to f^{-1} [x] \cap y \in (J ↾_{𝑡} y)$
54	53	expr	$⊢ ((((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \land y \in 𝒫 ⋃ J) \to (J ↾_{𝑡} y \in Comp \to f^{-1} [x] \cap y \in (J ↾_{𝑡} y))$
55	54	ralrimiva	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to f^{-1} [x] \cap y \in (J ↾_{𝑡} y))$
56		kgentop	$⊢ J \in ran 𝑘Gen \to J \in Top$
57	56	ad3antrrr	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to J \in Top$
58		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
59	57 58	sylib	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to J \in TopOn (⋃ J)$
60		elkgen	$⊢ J \in TopOn (⋃ J) \to (f^{-1} [x] \in 𝑘Gen (J) \leftrightarrow (f^{-1} [x] \subseteq ⋃ J \land \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to f^{-1} [x] \cap y \in (J ↾_{𝑡} y))))$
61	59 60	syl	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to (f^{-1} [x] \in 𝑘Gen (J) \leftrightarrow (f^{-1} [x] \subseteq ⋃ J \land \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to f^{-1} [x] \cap y \in (J ↾_{𝑡} y))))$
62	8 55 61	mpbir2and	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to f^{-1} [x] \in 𝑘Gen (J)$
63		kgenidm	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) = J$
64	63	ad3antrrr	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to 𝑘Gen (J) = J$
65	62 64	eleqtrd	$⊢ (((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \land x \in 𝑘Gen (K)) \to f^{-1} [x] \in J$
66	65	ralrimiva	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to \forall x \in 𝑘Gen (K) f^{-1} [x] \in J$
67	56 58	sylib	$⊢ J \in ran 𝑘Gen \to J \in TopOn (⋃ J)$
68		kgentopon	$⊢ K \in TopOn (⋃ K) \to 𝑘Gen (K) \in TopOn (⋃ K)$
69	34 68	sylbi	$⊢ K \in Top \to 𝑘Gen (K) \in TopOn (⋃ K)$
70		iscn	$⊢ (J \in TopOn (⋃ J) \land 𝑘Gen (K) \in TopOn (⋃ K)) \to (f \in (J Cn 𝑘Gen (K)) \leftrightarrow (f : ⋃ J ⟶ ⋃ K \land \forall x \in 𝑘Gen (K) f^{-1} [x] \in J))$
71	67 69 70	syl2an	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to (f \in (J Cn 𝑘Gen (K)) \leftrightarrow (f : ⋃ J ⟶ ⋃ K \land \forall x \in 𝑘Gen (K) f^{-1} [x] \in J))$
72	71	adantr	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to (f \in (J Cn 𝑘Gen (K)) \leftrightarrow (f : ⋃ J ⟶ ⋃ K \land \forall x \in 𝑘Gen (K) f^{-1} [x] \in J))$
73	4 66 72	mpbir2and	$⊢ ((J \in ran 𝑘Gen \land K \in Top) \land f \in (J Cn K)) \to f \in (J Cn 𝑘Gen (K))$
74	73	ex	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to (f \in (J Cn K) \to f \in (J Cn 𝑘Gen (K)))$
75	74	ssrdv	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to J Cn K \subseteq J Cn 𝑘Gen (K)$
76	69	adantl	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to 𝑘Gen (K) \in TopOn (⋃ K)$
77		toponcom	$⊢ (K \in Top \land 𝑘Gen (K) \in TopOn (⋃ K)) \to K \in TopOn (⋃ 𝑘Gen (K))$
78	32 76 77	syl2anc	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to K \in TopOn (⋃ 𝑘Gen (K))$
79		kgenss	$⊢ K \in Top \to K \subseteq 𝑘Gen (K)$
80	79	adantl	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to K \subseteq 𝑘Gen (K)$
81		eqid	$⊢ ⋃ 𝑘Gen (K) = ⋃ 𝑘Gen (K)$
82	81	cnss2	$⊢ (K \in TopOn (⋃ 𝑘Gen (K)) \land K \subseteq 𝑘Gen (K)) \to J Cn 𝑘Gen (K) \subseteq J Cn K$
83	78 80 82	syl2anc	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to J Cn 𝑘Gen (K) \subseteq J Cn K$
84	75 83	eqssd	$⊢ (J \in ran 𝑘Gen \land K \in Top) \to J Cn K = J Cn 𝑘Gen (K)$

Metamath Proof Explorer

Theorem kgencn3

Proof