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		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))$
13		simpr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to F : X ⟶ Y$
14		elpwi	$⊢ k \in 𝒫 X \to k \subseteq X$
15		fssres	$⊢ (F : X ⟶ Y \land k \subseteq X) \to ({F ↾}_{k}) : k ⟶ Y$
16	13 14 15	syl2an	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to ({F ↾}_{k}) : k ⟶ Y$
17		simpll	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \to J \in TopOn (X)$
18		resttopon	$⊢ (J \in TopOn (X) \land k \subseteq X) \to J ↾_{𝑡} k \in TopOn (k)$
19	17 14 18	syl2an	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to J ↾_{𝑡} k \in TopOn (k)$
20		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y)) \land F : X ⟶ Y) \land k \in 𝒫 X) \to K \in TopOn (Y)$
21		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)))$
22	19 20 21	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)))$
23	16 22	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))$
24		cnvresima	$⊢ {({F ↾}_{k})}^{-1} [x] = F^{-1} [x] \cap k$
25	24	eleq1i	$⊢ {({F ↾}_{k})}^{-1} [x] \in (J ↾_{𝑡} k) \leftrightarrow F^{-1} [x] \cap k \in (J ↾_{𝑡} k)$
26	25	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)$
27	23 26	bitrdi	$⊢ (((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))$
28	27	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)))$
29		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))$
30	28 29	bitr4di	$⊢ (((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)))$
31	30	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)))$
32	12 31	bitr4id	$⊢ ((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