cnprest - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnprest		Structured version Visualization version GIF version

Theorem cnprest 23498

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

**Hypotheses**
Ref	Expression
cnprest.1	⊢ 𝑋 = ∪ 𝐽
cnprest.2	⊢ 𝑌 = ∪ 𝐾

**Assertion**
Ref	Expression
cnprest	⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃)))

Proof of Theorem cnprest Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnptop2 23452	. . 3 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top)
2	1	a1i 11	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top))
3		cnptop2 23452	. . 3 ⊢ ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃) → 𝐾 ∈ Top)
4	3	a1i 11	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃) → 𝐾 ∈ Top))
5		cnprest.1	. . . . . . . . . . . 12 ⊢ 𝑋 = ∪ 𝐽
6	5	ntrss2 23266	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ⊆ 𝐴)
7	6	3ad2ant1 1151	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((int‘𝐽)‘𝐴) ⊆ 𝐴)
8		simp2l 1218	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝑃 ∈ ((int‘𝐽)‘𝐴))
9	7, 8	sseldd 3939	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝑃 ∈ 𝐴)
10	9	fvresd 6905	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 ↾ 𝐴)‘𝑃) = (𝐹‘𝑃))
11	10	eqcomd 2771	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹‘𝑃) = ((𝐹 ↾ 𝐴)‘𝑃))
12	11	eleq1d 2850	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹‘𝑃) ∈ 𝑦 ↔ ((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦))
13		inss1 4189	. . . . . . . . . . 11 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥
14		imass2 6106	. . . . . . . . . . 11 ⊢ ((𝑥 ∩ 𝐴) ⊆ 𝑥 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ (𝐹 “ 𝑥))
15		sstr2 3945	. . . . . . . . . . 11 ⊢ ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ (𝐹 “ 𝑥) → ((𝐹 “ 𝑥) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
16	13, 14, 15	mp2b 10	. . . . . . . . . 10 ⊢ ((𝐹 “ 𝑥) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)
17	16	anim2i 629	. . . . . . . . 9 ⊢ ((𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
18	17	reximi 3105	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
19		simp1l 1216	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐽 ∈ Top)
20	5	ntropn 23258	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
21	20	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
22		inopn 23108	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽) → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽)
23	22	3com23 1144	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽 ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽)
24	23	3expia 1139	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽) → (𝑥 ∈ 𝐽 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽))
25	19, 21, 24	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝑥 ∈ 𝐽 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽))
26		elin 3922	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ↔ (𝑃 ∈ 𝑥 ∧ 𝑃 ∈ ((int‘𝐽)‘𝐴)))
27	26	simplbi2com 508	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ((int‘𝐽)‘𝐴) → (𝑃 ∈ 𝑥 → 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
28	8, 27	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝑃 ∈ 𝑥 → 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
29		sslin 4195	. . . . . . . . . . . . . . . . 17 ⊢ (((int‘𝐽)‘𝐴) ⊆ 𝐴 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ⊆ (𝑥 ∩ 𝐴))
30	7, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ⊆ (𝑥 ∩ 𝐴))
31		imass2 6106	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ((int‘𝐽)‘𝐴)) ⊆ (𝑥 ∩ 𝐴) → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)))
32	30, 31	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)))
33		sstr2 3945	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)) → ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
34	32, 33	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
35	28, 34	anim12d 621	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)))
36	25, 35	anim12d 621	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)) → ((𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))))
37		eleq2 2854	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
38		imaeq2 6060	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → (𝐹 “ 𝑧) = (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
39	38	sseq1d 3969	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
40	37, 39	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)))
41	40	rspcev 3583	. . . . . . . . . . . 12 ⊢ (((𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
42	36, 41	syl6 36	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
43	42	expdimp 458	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑥 ∈ 𝐽) → ((𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
44	43	rexlimdva 3168	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
45		eleq2 2854	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥))
46		imaeq2 6060	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝐹 “ 𝑧) = (𝐹 “ 𝑥))
47	46	sseq1d 3969	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ 𝑥) ⊆ 𝑦))
48	45, 47	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))
49	48	cbvrexvw 3246	. . . . . . . . 9 ⊢ (∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))
50	44, 49	imbitrdi 254	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))
51	18, 50	impbid2 229	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
52		vex 3461	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
53	52	inex1 5288	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ∈ V
54	53	a1i 11	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ V)
55	19	uniexd 7750	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ∪ 𝐽 ∈ V)
56		simp1r 1217	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐴 ⊆ 𝑋)
57	56, 5	sseqtrdi 3978	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐴 ⊆ ∪ 𝐽)
58	55, 57	ssexd 5297	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐴 ∈ V)
59		elrest 17504	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾_t 𝐴) ↔ ∃𝑥 ∈ 𝐽 𝑧 = (𝑥 ∩ 𝐴)))
60	19, 58, 59	syl2anc 596	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝑧 ∈ (𝐽 ↾_t 𝐴) ↔ ∃𝑥 ∈ 𝐽 𝑧 = (𝑥 ∩ 𝐴)))
61		eleq2 2854	. . . . . . . . . 10 ⊢ (𝑧 = (𝑥 ∩ 𝐴) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ (𝑥 ∩ 𝐴)))
62		elin 3922	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ (𝑃 ∈ 𝑥 ∧ 𝑃 ∈ 𝐴))
63	62	rbaib 548	. . . . . . . . . . 11 ⊢ (𝑃 ∈ 𝐴 → (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ 𝑃 ∈ 𝑥))
64	9, 63	syl 18	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ 𝑃 ∈ 𝑥))
65	61, 64	sylan9bbr 520	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥))
66		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → 𝑧 = (𝑥 ∩ 𝐴))
67	66	imaeq2d 6064	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴) “ 𝑧) = ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)))
68		inss2 4190	. . . . . . . . . . . 12 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
69		resima2 6017	. . . . . . . . . . . 12 ⊢ ((𝑥 ∩ 𝐴) ⊆ 𝐴 → ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)) = (𝐹 “ (𝑥 ∩ 𝐴)))
70	68, 69	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)) = (𝐹 “ (𝑥 ∩ 𝐴))
71	67, 70	eqtrdi 2816	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴) “ 𝑧) = (𝐹 “ (𝑥 ∩ 𝐴)))
72	71	sseq1d 3969	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → (((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
73	65, 72	anbi12d 644	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
74	54, 60, 73	rexxfr2d 5384	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
75	51, 74	bitr4d 285	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) ↔ ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))
76	12, 75	imbi12d 347	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) ↔ (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
77	76	ralbidv 3190	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) ↔ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
78		simp2r 1219	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐹:𝑋⟶𝑌)
79		simp3 1156	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐾 ∈ Top)
80	56, 9	sseldd 3939	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝑃 ∈ 𝑋)
81		cnprest.2	. . . . . . . 8 ⊢ 𝑌 = ∪ 𝐾
82	5, 81	iscnp2 23448	. . . . . . 7 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
83	82	baib 545	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
84	19, 79, 80, 83	syl3anc 1398	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
85	78, 84	mpbirand 720	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))
86	78, 56	fssresd 6749	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 ↾ 𝐴):𝐴⟶𝑌)
87	5	toptopon 23126	. . . . . . . 8 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
88	19, 87	sylib 221	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐽 ∈ (TopOn‘𝑋))
89		resttopon 23370	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾_t 𝐴) ∈ (TopOn‘𝐴))
90	88, 56, 89	syl2anc 596	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐽 ↾_t 𝐴) ∈ (TopOn‘𝐴))
91	81	toptopon 23126	. . . . . . 7 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
92	79, 91	sylib 221	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐾 ∈ (TopOn‘𝑌))
93		iscnp 23446	. . . . . 6 ⊢ (((𝐽 ↾_t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝐴) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹 ↾ 𝐴):𝐴⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))))
94	90, 92, 9, 93	syl3anc 1398	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹 ↾ 𝐴):𝐴⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))))
95	86, 94	mpbirand 720	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃) ↔ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾_t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
96	77, 85, 95	3bitr4d 314	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃)))
97	96	3expia 1139	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐾 ∈ Top → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃))))
98	2, 4, 97	pm5.21ndd 382	1 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾_t 𝐴) CnP 𝐾)‘𝑃)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ∩ cin 3905 ⊆ wss 3906 ∪ cuni 4874 ↾ cres 5665 “ cima 5666 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ↾_t crest 17497 Topctop 23102 TopOnctopon 23119 intcnt 23226 CnP ccnp 23434

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-map 8832 df-en 8950 df-fin 8953 df-fi 9378 df-rest 17499 df-topgen 17520 df-top 23103 df-topon 23120 df-bases 23155 df-ntr 23229 df-cnp 23437

This theorem is used by: limcres 26098 dvcnvrelem2 26230 psercn 26642 abelth 26657 cxpcn3 26966 efrlim 27187 cvmlift2lem11 35844 cvmlift2lem12 35845 cvmlift3lem7 35856 cncfuni 46660 cncfiooicclem1 46667 dirkercncflem4 46880 fourierdlem62 46942

W3C validator