cnprest

Description: Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014)

	Ref	Expression
Hypotheses	cnprest.1	$⊢ X = ⋃ J$
	cnprest.2	$⊢ Y = ⋃ K$
Assertion	cnprest	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y)) \to (F \in (J CnP K) (P) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P))$

Proof

Step	Hyp	Ref	Expression
1		cnprest.1	$⊢ X = ⋃ J$
2		cnprest.2	$⊢ Y = ⋃ K$
3		cnptop2	$⊢ F \in (J CnP K) (P) \to K \in Top$
4	3	a1i	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y)) \to (F \in (J CnP K) (P) \to K \in Top)$
5		cnptop2	$⊢ {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \to K \in Top$
6	5	a1i	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y)) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \to K \in Top)$
7	1	ntrss2	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \subseteq A$
8	7	3ad2ant1	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to int (J) (A) \subseteq A$
9		simp2l	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to P \in int (J) (A)$
10	8 9	sseldd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to P \in A$
11	10	fvresd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ({F ↾}_{A}) (P) = F (P)$
12	11	eqcomd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to F (P) = ({F ↾}_{A}) (P)$
13	12	eleq1d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (F (P) \in y \leftrightarrow ({F ↾}_{A}) (P) \in y)$
14		inss1	$⊢ x \cap A \subseteq x$
15		imass2	$⊢ x \cap A \subseteq x \to F [x \cap A] \subseteq F [x]$
16		sstr2	$⊢ F [x \cap A] \subseteq F [x] \to (F [x] \subseteq y \to F [x \cap A] \subseteq y)$
17	14 15 16	mp2b	$⊢ F [x] \subseteq y \to F [x \cap A] \subseteq y$
18	17	anim2i	$⊢ (P \in x \land F [x] \subseteq y) \to (P \in x \land F [x \cap A] \subseteq y)$
19	18	reximi	$⊢ \exists x \in J (P \in x \land F [x] \subseteq y) \to \exists x \in J (P \in x \land F [x \cap A] \subseteq y)$
20		simp1l	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to J \in Top$
21	1	ntropn	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \in J$
22	21	3ad2ant1	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to int (J) (A) \in J$
23		inopn	$⊢ (J \in Top \land x \in J \land int (J) (A) \in J) \to x \cap int (J) (A) \in J$
24	23	3com23	$⊢ (J \in Top \land int (J) (A) \in J \land x \in J) \to x \cap int (J) (A) \in J$
25	24	3expia	$⊢ (J \in Top \land int (J) (A) \in J) \to (x \in J \to x \cap int (J) (A) \in J)$
26	20 22 25	syl2anc	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (x \in J \to x \cap int (J) (A) \in J)$
27		elin	$⊢ P \in (x \cap int (J) (A)) \leftrightarrow (P \in x \land P \in int (J) (A))$
28	27	simplbi2com	$⊢ P \in int (J) (A) \to (P \in x \to P \in (x \cap int (J) (A)))$
29	9 28	syl	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (P \in x \to P \in (x \cap int (J) (A)))$
30		sslin	$⊢ int (J) (A) \subseteq A \to x \cap int (J) (A) \subseteq x \cap A$
31	8 30	syl	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to x \cap int (J) (A) \subseteq x \cap A$
32		imass2	$⊢ x \cap int (J) (A) \subseteq x \cap A \to F [x \cap int (J) (A)] \subseteq F [x \cap A]$
33	31 32	syl	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to F [x \cap int (J) (A)] \subseteq F [x \cap A]$
34		sstr2	$⊢ F [x \cap int (J) (A)] \subseteq F [x \cap A] \to (F [x \cap A] \subseteq y \to F [x \cap int (J) (A)] \subseteq y)$
35	33 34	syl	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (F [x \cap A] \subseteq y \to F [x \cap int (J) (A)] \subseteq y)$
36	29 35	anim12d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ((P \in x \land F [x \cap A] \subseteq y) \to (P \in (x \cap int (J) (A)) \land F [x \cap int (J) (A)] \subseteq y))$
37	26 36	anim12d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ((x \in J \land (P \in x \land F [x \cap A] \subseteq y)) \to (x \cap int (J) (A) \in J \land (P \in (x \cap int (J) (A)) \land F [x \cap int (J) (A)] \subseteq y)))$
38		eleq2	$⊢ z = x \cap int (J) (A) \to (P \in z \leftrightarrow P \in (x \cap int (J) (A)))$
39		imaeq2	$⊢ z = x \cap int (J) (A) \to F [z] = F [x \cap int (J) (A)]$
40	39	sseq1d	$⊢ z = x \cap int (J) (A) \to (F [z] \subseteq y \leftrightarrow F [x \cap int (J) (A)] \subseteq y)$
41	38 40	anbi12d	$⊢ z = x \cap int (J) (A) \to ((P \in z \land F [z] \subseteq y) \leftrightarrow (P \in (x \cap int (J) (A)) \land F [x \cap int (J) (A)] \subseteq y))$
42	41	rspcev	$⊢ (x \cap int (J) (A) \in J \land (P \in (x \cap int (J) (A)) \land F [x \cap int (J) (A)] \subseteq y)) \to \exists z \in J (P \in z \land F [z] \subseteq y)$
43	37 42	syl6	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ((x \in J \land (P \in x \land F [x \cap A] \subseteq y)) \to \exists z \in J (P \in z \land F [z] \subseteq y))$
44	43	expdimp	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land x \in J) \to ((P \in x \land F [x \cap A] \subseteq y) \to \exists z \in J (P \in z \land F [z] \subseteq y))$
45	44	rexlimdva	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\exists x \in J (P \in x \land F [x \cap A] \subseteq y) \to \exists z \in J (P \in z \land F [z] \subseteq y))$
46		eleq2	$⊢ z = x \to (P \in z \leftrightarrow P \in x)$
47		imaeq2	$⊢ z = x \to F [z] = F [x]$
48	47	sseq1d	$⊢ z = x \to (F [z] \subseteq y \leftrightarrow F [x] \subseteq y)$
49	46 48	anbi12d	$⊢ z = x \to ((P \in z \land F [z] \subseteq y) \leftrightarrow (P \in x \land F [x] \subseteq y))$
50	49	cbvrexvw	$⊢ \exists z \in J (P \in z \land F [z] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land F [x] \subseteq y)$
51	45 50	syl6ib	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\exists x \in J (P \in x \land F [x \cap A] \subseteq y) \to \exists x \in J (P \in x \land F [x] \subseteq y))$
52	19 51	impbid2	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land F [x \cap A] \subseteq y))$
53		vex	$⊢ x \in V$
54	53	inex1	$⊢ x \cap A \in V$
55	54	a1i	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land x \in J) \to x \cap A \in V$
56	20	uniexd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ⋃ J \in V$
57		simp1r	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to A \subseteq X$
58	57 1	sseqtrdi	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to A \subseteq ⋃ J$
59	56 58	ssexd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to A \in V$
60		elrest	$⊢ (J \in Top \land A \in V) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J z = x \cap A)$
61	20 59 60	syl2anc	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J z = x \cap A)$
62		eleq2	$⊢ z = x \cap A \to (P \in z \leftrightarrow P \in (x \cap A))$
63		elin	$⊢ P \in (x \cap A) \leftrightarrow (P \in x \land P \in A)$
64	63	rbaib	$⊢ P \in A \to (P \in (x \cap A) \leftrightarrow P \in x)$
65	10 64	syl	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (P \in (x \cap A) \leftrightarrow P \in x)$
66	62 65	sylan9bbr	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to (P \in z \leftrightarrow P \in x)$
67		simpr	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to z = x \cap A$
68	67	imaeq2d	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to ({F ↾}_{A}) [z] = ({F ↾}_{A}) [x \cap A]$
69		inss2	$⊢ x \cap A \subseteq A$
70		resima2	$⊢ x \cap A \subseteq A \to ({F ↾}_{A}) [x \cap A] = F [x \cap A]$
71	69 70	ax-mp	$⊢ ({F ↾}_{A}) [x \cap A] = F [x \cap A]$
72	68 71	eqtrdi	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to ({F ↾}_{A}) [z] = F [x \cap A]$
73	72	sseq1d	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to (({F ↾}_{A}) [z] \subseteq y \leftrightarrow F [x \cap A] \subseteq y)$
74	66 73	anbi12d	$⊢ (((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \land z = x \cap A) \to ((P \in z \land ({F ↾}_{A}) [z] \subseteq y) \leftrightarrow (P \in x \land F [x \cap A] \subseteq y))$
75	55 61 74	rexxfr2d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land F [x \cap A] \subseteq y))$
76	52 75	bitr4d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \leftrightarrow \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
77	13 76	imbi12d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ((F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \leftrightarrow (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y)))$
78	77	ralbidv	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (\forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)) \leftrightarrow \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y)))$
79		simp2r	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to F : X ⟶ Y$
80		simp3	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to K \in Top$
81	57 10	sseldd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to P \in X$
82	1 2	iscnp2	$⊢ F \in (J CnP K) (P) \leftrightarrow ((J \in Top \land K \in Top \land P \in X) \land (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
83	82	baib	$⊢ (J \in Top \land K \in Top \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
84	20 80 81 83	syl3anc	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
85	79 84	mpbirand	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (F \in (J CnP K) (P) \leftrightarrow \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)))$
86	79 57	fssresd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ({F ↾}_{A}) : A ⟶ Y$
87	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
88	20 87	sylib	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to J \in TopOn (X)$
89		resttopon	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$
90	88 57 89	syl2anc	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to J ↾_{𝑡} A \in TopOn (A)$
91	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
92	80 91	sylib	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to K \in TopOn (Y)$
93		iscnp	$⊢ (J ↾_{𝑡} A \in TopOn (A) \land K \in TopOn (Y) \land P \in A) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \leftrightarrow (({F ↾}_{A}) : A ⟶ Y \land \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))))$
94	90 92 10 93	syl3anc	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \leftrightarrow (({F ↾}_{A}) : A ⟶ Y \land \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))))$
95	86 94	mpbirand	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \leftrightarrow \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y)))$
96	78 85 95	3bitr4d	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y) \land K \in Top) \to (F \in (J CnP K) (P) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P))$
97	96	3expia	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y)) \to (K \in Top \to (F \in (J CnP K) (P) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P)))$
98	4 6 97	pm5.21ndd	$⊢ ((J \in Top \land A \subseteq X) \land (P \in int (J) (A) \land F : X ⟶ Y)) \to (F \in (J CnP K) (P) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P))$

Metamath Proof Explorer

Theorem cnprest

Proof