kgencn

Description: A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	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))))$

Proof

Step	Hyp	Ref	Expression
1		kgentopon	$⊢ J \in TopOn (X) \to 𝑘Gen (J) \in TopOn (X)$
2		iscn	$⊢ (𝑘Gen (J) \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (𝑘Gen (J) Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in 𝑘Gen (J)))$
3	1 2	sylan	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (𝑘Gen (J) Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in 𝑘Gen (J)))$
4		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
5		fdm	$⊢ F : X ⟶ Y \to dom F = X$
6	5	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to dom F = X$
7	4 6	sseqtrid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to F^{-1} [x] \subseteq X$
8		elkgen	$⊢ J \in TopOn (X) \to (F^{-1} [x] \in 𝑘Gen (J) \leftrightarrow (F^{-1} [x] \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k))))$
9	8	ad2antrr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (F^{-1} [x] \in 𝑘Gen (J) \leftrightarrow (F^{-1} [x] \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k))))$
10	7 9	mpbirand	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (F^{-1} [x] \in 𝑘Gen (J) \leftrightarrow \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)))$
11	10	ralbidv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in K F^{-1} [x] \in 𝑘Gen (J) \leftrightarrow \forall x \in K \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)))$
12		simpr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to F : X ⟶ Y$
13		elpwi	$⊢ k \in 𝒫 X \to k \subseteq X$
14		fssres	$⊢ (F : X ⟶ Y \land k \subseteq X) \to ({F ↾}_{k}) : k ⟶ Y$
15	12 13 14	syl2an	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ({F ↾}_{k}) : k ⟶ Y$
16		simpll	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to J \in TopOn (X)$
17		resttopon	$⊢ (J \in TopOn (X) \land k \subseteq X) \to J ↾_{𝑡} k \in TopOn (k)$
18	16 13 17	syl2an	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to J ↾_{𝑡} k \in TopOn (k)$
19		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to K \in TopOn (Y)$
20		iscn	$⊢ (J ↾_{𝑡} k \in TopOn (k) \land K \in TopOn (Y)) \to ({F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow (({F ↾}_{k}) : k ⟶ Y \land \forall x \in K {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k)))$
21	18 19 20	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ({F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow (({F ↾}_{k}) : k ⟶ Y \land \forall x \in K {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k)))$
22	15 21	mpbirand	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ({F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow \forall x \in K {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k))$
23		cnvresima	$⊢ {({F ↾}_{k})}^{-1} [x] = F^{-1} [x] \cap k$
24	23	eleq1i	$⊢ {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k) \leftrightarrow F^{-1} [x] \cap k \in (J ↾_{𝑡} k)$
25	24	ralbii	$⊢ \forall x \in K {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k) \leftrightarrow \forall x \in K F^{-1} [x] \cap k \in (J ↾_{𝑡} k)$
26	22 25	syl6bb	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ({F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K) \leftrightarrow \forall x \in K F^{-1} [x] \cap k \in (J ↾_{𝑡} k))$
27	26	imbi2d	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ((J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \leftrightarrow (J ↾_{𝑡} k \in Comp \to \forall x \in K F^{-1} [x] \cap k \in (J ↾_{𝑡} k)))$
28		r19.21v	$⊢ \forall x \in K (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)) \leftrightarrow (J ↾_{𝑡} k \in Comp \to \forall x \in K F^{-1} [x] \cap k \in (J ↾_{𝑡} k))$
29	27 28	syl6bbr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ((J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)) \leftrightarrow \forall x \in K (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)))$
30	29	ralbidva	$⊢ ((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 k \in 𝒫 X \forall x \in K (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)))$
31		ralcom	$⊢ \forall x \in K \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)) \leftrightarrow \forall k \in 𝒫 X \forall x \in K (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k))$
32	30 31	syl6rbbr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in K \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to F^{-1} [x] \cap k \in (J ↾_{𝑡} k)) \leftrightarrow \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)))$
33	11 32	bitrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to (\forall x \in K F^{-1} [x] \in 𝑘Gen (J) \leftrightarrow \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K)))$
34	33	pm5.32da	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F : X ⟶ Y \land \forall x \in K F^{-1} [x] \in 𝑘Gen (J)) \leftrightarrow (F : X ⟶ Y \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to {F ↾}_{k} \in ((J ↾_{𝑡} k) Cn K))))$
35	3 34	bitrd	$⊢ (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))))$

Metamath Proof Explorer

Theorem kgencn

Proof