kgencn2

Description: A function F : J --> K from a compactly generated space is continuous iff for all compact spaces z and continuous g : z --> J , the composite F o. g : z --> K is continuous. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	kgencn2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (𝑘Gen (J) Cn K) \leftrightarrow (F : X ⟶ Y \land \forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K)))$

Proof

Step	Hyp	Ref	Expression
1		kgencn	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (𝑘Gen (J) Cn K) \leftrightarrow (F : X ⟶ Y \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K))))$
2		rncmp	$⊢ (z \in Comp \land g \in (z Cn J)) \to J ↾_{𝑡} ran g \in Comp$
3	2	adantl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to J ↾_{𝑡} ran g \in Comp$
4		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to g \in (z Cn J)$
5		eqid	$⊢ ⋃ z = ⋃ z$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	5 6	cnf	$⊢ g \in (z Cn J) \to g : ⋃ z ⟶ ⋃ J$
8		frn	$⊢ g : ⋃ z ⟶ ⋃ J \to ran g \subseteq ⋃ J$
9	4 7 8	3syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ran g \subseteq ⋃ J$
10		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
11	10	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to X = ⋃ J$
12	9 11	sseqtrrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ran g \subseteq X$
13		vex	$⊢ g \in V$
14	13	rnex	$⊢ ran g \in V$
15	14	elpw	$⊢ ran g \in 𝒫 X \leftrightarrow ran g \subseteq X$
16	12 15	sylibr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ran g \in 𝒫 X$
17		oveq2	$⊢ k = ran g \to J ↾_{𝑡} k = J ↾_{𝑡} ran g$
18	17	eleq1d	$⊢ k = ran g \to (J ↾_{𝑡} k \in Comp \leftrightarrow J ↾_{𝑡} ran g \in Comp)$
19		reseq2	$⊢ k = ran g \to {F ↾}_{k} = {F ↾}_{ran g}$
20	17	oveq1d	$⊢ k = ran g \to (J ↾_{𝑡} k) Cn K = (J ↾_{𝑡} ran g) Cn K$
21	19 20	eleq12d	$⊢ k = ran g \to ({F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K))$
22	18 21	imbi12d	$⊢ k = ran g \to ((J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \leftrightarrow (J ↾_{𝑡} ran g \in Comp \to {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K)))$
23	22	rspcv	$⊢ ran g \in 𝒫 X \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \to (J ↾_{𝑡} ran g \in Comp \to {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K)))$
24	16 23	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \to (J ↾_{𝑡} ran g \in Comp \to {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K)))$
25	3 24	mpid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \to {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K))$
26		simplll	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to J \in TopOn (X)$
27		ssidd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ran g \subseteq ran g$
28		cnrest2	$⊢ (J \in TopOn (X) \land ran g \subseteq ran g \land ran g \subseteq X) \to (g \in (z Cn J) \leftrightarrow g \in (z Cn (J ↾_{𝑡} ran g)))$
29	26 27 12 28	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to (g \in (z Cn J) \leftrightarrow g \in (z Cn (J ↾_{𝑡} ran g)))$
30	4 29	mpbid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to g \in (z Cn (J ↾_{𝑡} ran g))$
31		cnco	$⊢ (g \in (z Cn (J ↾_{𝑡} ran g)) \land {F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K)) \to ({F ↾}_{ran g}) \circ g \in (z Cn K)$
32	31	ex	$⊢ g \in (z Cn (J ↾_{𝑡} ran g)) \to ({F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K) \to ({F ↾}_{ran g}) \circ g \in (z Cn K))$
33	30 32	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ({F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K) \to ({F ↾}_{ran g}) \circ g \in (z Cn K))$
34		ssid	$⊢ ran g \subseteq ran g$
35		cores	$⊢ ran g \subseteq ran g \to ({F ↾}_{ran g}) \circ g = F \circ g$
36	34 35	ax-mp	$⊢ ({F ↾}_{ran g}) \circ g = F \circ g$
37	36	eleq1i	$⊢ ({F ↾}_{ran g}) \circ g \in (z Cn K) \leftrightarrow F \circ g \in (z Cn K)$
38	33 37	imbitrdi	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to ({F ↾}_{ran g} \in ((J ↾_{𝑡} ran g) Cn K) \to F \circ g \in (z Cn K))$
39	25 38	syld	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land (z \in Comp \land g \in (z Cn J))) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \to F \circ g \in (z Cn K))$
40	39	ralrimdvva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \to \forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K))$
41		oveq1	$⊢ z = J ↾_{𝑡} k \to z Cn J = (J ↾_{𝑡} k) Cn J$
42		oveq1	$⊢ z = J ↾_{𝑡} k \to z Cn K = (J ↾_{𝑡} k) Cn K$
43	42	eleq2d	$⊢ z = J ↾_{𝑡} k \to (F \circ g \in (z Cn K) \leftrightarrow F \circ g \in ((J ↾_{𝑡} k) Cn K))$
44	41 43	raleqbidv	$⊢ z = J ↾_{𝑡} k \to (\forall g \in (z Cn J) F \circ g \in (z Cn K) \leftrightarrow \forall g \in ((J ↾_{𝑡} k) Cn J) F \circ g \in ((J ↾_{𝑡} k) Cn K))$
45	44	rspcv	$⊢ J ↾_{𝑡} k \in Comp \to (\forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K) \to \forall g \in ((J ↾_{𝑡} k) Cn J) F \circ g \in ((J ↾_{𝑡} k) Cn K))$
46		elpwi	$⊢ k \in 𝒫 X \to k \subseteq X$
47	46	adantl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to k \subseteq X$
48	47	resabs1d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to {({I ↾}_{X}) ↾}_{k} = {I ↾}_{k}$
49		idcn	$⊢ J \in TopOn (X) \to {I ↾}_{X} \in (J Cn J)$
50	49	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to {I ↾}_{X} \in (J Cn J)$
51	10	ad3antrrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to X = ⋃ J$
52	47 51	sseqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to k \subseteq ⋃ J$
53	6	cnrest	$⊢ ({I ↾}_{X} \in (J Cn J) \land k \subseteq ⋃ J) \to {({I ↾}_{X}) ↾}_{k} \in ((J ↾_{𝑡} k) Cn J)$
54	50 52 53	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to {({I ↾}_{X}) ↾}_{k} \in ((J ↾_{𝑡} k) Cn J)$
55	48 54	eqeltrrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to {I ↾}_{k} \in ((J ↾_{𝑡} k) Cn J)$
56		coeq2	$⊢ g = {I ↾}_{k} \to F \circ g = F \circ ({I ↾}_{k})$
57	56	eleq1d	$⊢ g = {I ↾}_{k} \to (F \circ g \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow F \circ ({I ↾}_{k}) \in ((J ↾_{𝑡} k) Cn K))$
58	57	rspcv	$⊢ {I ↾}_{k} \in ((J ↾_{𝑡} k) Cn J) \to (\forall g \in ((J ↾_{𝑡} k) Cn J) F \circ g \in ((J ↾_{𝑡} k) Cn K) \to F \circ ({I ↾}_{k}) \in ((J ↾_{𝑡} k) Cn K))$
59	55 58	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to (\forall g \in ((J ↾_{𝑡} k) Cn J) F \circ g \in ((J ↾_{𝑡} k) Cn K) \to F \circ ({I ↾}_{k}) \in ((J ↾_{𝑡} k) Cn K))$
60		coires1	$⊢ F \circ ({I ↾}_{k}) = {F ↾}_{k}$
61	60	eleq1i	$⊢ F \circ ({I ↾}_{k}) \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)$
62	59 61	imbitrdi	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to (\forall g \in ((J ↾_{𝑡} k) Cn J) F \circ g \in ((J ↾_{𝑡} k) Cn K) \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K))$
63	45 62	syl9r	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to (J ↾_{𝑡} k \in Comp \to (\forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K) \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)))$
64	63	com23	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to (\forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K) \to (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)))$
65	64	ralrimdva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K) \to \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)))$
66	40 65	impbid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \leftrightarrow \forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K))$
67	66	pm5.32da	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K))) \leftrightarrow (F : X ⟶ Y \land \forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K)))$
68	1 67	bitrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (𝑘Gen (J) Cn K) \leftrightarrow (F : X ⟶ Y \land \forall z \in Comp \forall g \in (z Cn J) F \circ g \in (z Cn K)))$

Metamath Proof Explorer

Theorem kgencn2

Proof