Theorem cnptoprest 13033

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

Hypotheses

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

Assertion

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

Proof of Theorem cnptoprest

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 995	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐽 ∈ Top)
2		simpl3 997	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐴 ⊆ 𝑋)
3		cnprest.1	. . . . . . . . . 10 ⊢ 𝑋 = ∪ 𝐽
4	3	ntrss2 12915	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ⊆ 𝐴)
5	1, 2, 4	syl2anc 409	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((int‘𝐽)‘𝐴) ⊆ 𝐴)
6		simprl 526	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝑃 ∈ ((int‘𝐽)‘𝐴))
7	5, 6	sseldd 3148	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝑃 ∈ 𝐴)
8		fvres 5520	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑃) = (𝐹‘𝑃))
9	7, 8	syl 14	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝐹 ↾ 𝐴)‘𝑃) = (𝐹‘𝑃))
10	9	eqcomd 2176	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹‘𝑃) = ((𝐹 ↾ 𝐴)‘𝑃))
11	10	eleq1d 2239	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝐹‘𝑃) ∈ 𝑦 ↔ ((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦))
12		inss1 3347	. . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥
13		imass2 4987	. . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ⊆ 𝑥 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ (𝐹 “ 𝑥))
14		sstr2 3154	. . . . . . . . 9 ⊢ ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ (𝐹 “ 𝑥) → ((𝐹 “ 𝑥) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
15	12, 13, 14	mp2b 8	. . . . . . . 8 ⊢ ((𝐹 “ 𝑥) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)
16	15	anim2i 340	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
17	16	reximi 2567	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
18	3	ntropn 12911	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
19	1, 2, 18	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((int‘𝐽)‘𝐴) ∈ 𝐽)
20		inopn 12795	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽) → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽)
21	20	3com23 1204	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽 ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽)
22	21	3expia 1200	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ ((int‘𝐽)‘𝐴) ∈ 𝐽) → (𝑥 ∈ 𝐽 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽))
23	1, 19, 22	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝑥 ∈ 𝐽 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽))
24		elin 3310	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ↔ (𝑃 ∈ 𝑥 ∧ 𝑃 ∈ ((int‘𝐽)‘𝐴)))
25	24	simplbi2com 1437	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ((int‘𝐽)‘𝐴) → (𝑃 ∈ 𝑥 → 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
26	6, 25	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝑃 ∈ 𝑥 → 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
27		sslin 3353	. . . . . . . . . . . . . 14 ⊢ (((int‘𝐽)‘𝐴) ⊆ 𝐴 → (𝑥 ∩ ((int‘𝐽)‘𝐴)) ⊆ (𝑥 ∩ 𝐴))
28		imass2 4987	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ ((int‘𝐽)‘𝐴)) ⊆ (𝑥 ∩ 𝐴) → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)))
29	5, 27, 28	3syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)))
30		sstr2 3154	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ (𝐹 “ (𝑥 ∩ 𝐴)) → ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
31	29, 30	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦 → (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
32	26, 31	anim12d 333	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)))
33	23, 32	anim12d 333	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)) → ((𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))))
34		eleq2 2234	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
35		imaeq2 4949	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → (𝐹 “ 𝑧) = (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))))
36	35	sseq1d 3176	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦))
37	34, 36	anbi12d 470	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑥 ∩ ((int‘𝐽)‘𝐴)) → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)))
38	37	rspcev 2834	. . . . . . . . . 10 ⊢ (((𝑥 ∩ ((int‘𝐽)‘𝐴)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑥 ∩ ((int‘𝐽)‘𝐴)) ∧ (𝐹 “ (𝑥 ∩ ((int‘𝐽)‘𝐴))) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
39	33, 38	syl6 33	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
40	39	expdimp 257	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑥 ∈ 𝐽) → ((𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
41	40	rexlimdva 2587	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
42		eleq2 2234	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥))
43		imaeq2 4949	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝐹 “ 𝑧) = (𝐹 “ 𝑥))
44	43	sseq1d 3176	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ 𝑥) ⊆ 𝑦))
45	42, 44	anbi12d 470	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))
46	45	cbvrexv 2697	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))
47	41, 46	syl6ib 160	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))
48	17, 47	impbid2 142	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
49		vex 2733	. . . . . . . 8 ⊢ 𝑥 ∈ V
50	49	inex1 4123	. . . . . . 7 ⊢ (𝑥 ∩ 𝐴) ∈ V
51	50	a1i 9	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ V)
52		uniexg 4424	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
53	1, 52	syl 14	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ∪ 𝐽 ∈ V)
54	2, 3	sseqtrdi 3195	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐴 ⊆ ∪ 𝐽)
55	53, 54	ssexd 4129	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐴 ∈ V)
56		elrest 12586	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑥 ∈ 𝐽 𝑧 = (𝑥 ∩ 𝐴)))
57	1, 55, 56	syl2anc 409	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑥 ∈ 𝐽 𝑧 = (𝑥 ∩ 𝐴)))
58		eleq2 2234	. . . . . . . 8 ⊢ (𝑧 = (𝑥 ∩ 𝐴) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ (𝑥 ∩ 𝐴)))
59		elin 3310	. . . . . . . . . 10 ⊢ (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ (𝑃 ∈ 𝑥 ∧ 𝑃 ∈ 𝐴))
60	59	rbaib 916	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐴 → (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ 𝑃 ∈ 𝑥))
61	7, 60	syl 14	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝑃 ∈ (𝑥 ∩ 𝐴) ↔ 𝑃 ∈ 𝑥))
62	58, 61	sylan9bbr 460	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ 𝑥))
63		simpr 109	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → 𝑧 = (𝑥 ∩ 𝐴))
64	63	imaeq2d 4953	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴) “ 𝑧) = ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)))
65		inss2 3348	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
66		resima2 4925	. . . . . . . . . 10 ⊢ ((𝑥 ∩ 𝐴) ⊆ 𝐴 → ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)) = (𝐹 “ (𝑥 ∩ 𝐴)))
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ ((𝐹 ↾ 𝐴) “ (𝑥 ∩ 𝐴)) = (𝐹 “ (𝑥 ∩ 𝐴))
68	64, 67	eqtrdi 2219	. . . . . . . 8 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴) “ 𝑧) = (𝐹 “ (𝑥 ∩ 𝐴)))
69	68	sseq1d 3176	. . . . . . 7 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → (((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦))
70	62, 69	anbi12d 470	. . . . . 6 ⊢ ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) ∧ 𝑧 = (𝑥 ∩ 𝐴)) → ((𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
71	51, 57, 70	rexxfr2d 4450	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ (𝑥 ∩ 𝐴)) ⊆ 𝑦)))
72	48, 71	bitr4d 190	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) ↔ ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))
73	11, 72	imbi12d 233	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) ↔ (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
74	73	ralbidv 2470	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) ↔ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
75	3	toptopon 12810	. . . . 5 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
76	1, 75	sylib 121	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐽 ∈ (TopOn‘𝑋))
77		simpl2 996	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐾 ∈ Top)
78		cnprest.2	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
79	78	toptopon 12810	. . . . 5 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
80	77, 79	sylib 121	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐾 ∈ (TopOn‘𝑌))
81	2, 7	sseldd 3148	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝑃 ∈ 𝑋)
82		iscnp 12993	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
83	76, 80, 81, 82	syl3anc 1233	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
84		simprr 527	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → 𝐹:𝑋⟶𝑌)
85	84	biantrurd 303	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
86	83, 85	bitr4d 190	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))
87		simp1l 1016	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐽 ∈ Top)
88	87, 75	sylib 121	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐽 ∈ (TopOn‘𝑋))
89		simp1r 1017	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐴 ⊆ 𝑋)
90		resttopon 12965	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
91	88, 89, 90	syl2anc 409	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
92		simp3 994	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐾 ∈ Top)
93	92, 79	sylib 121	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐾 ∈ (TopOn‘𝑌))
94	4	3ad2ant1 1013	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((int‘𝐽)‘𝐴) ⊆ 𝐴)
95		simp2l 1018	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝑃 ∈ ((int‘𝐽)‘𝐴))
96	94, 95	sseldd 3148	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝑃 ∈ 𝐴)
97		iscnp 12993	. . . . 5 ⊢ (((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝐴) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹 ↾ 𝐴):𝐴⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))))
98	91, 93, 96, 97	syl3anc 1233	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃) ↔ ((𝐹 ↾ 𝐴):𝐴⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))))
99		simp2r 1019	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → 𝐹:𝑋⟶𝑌)
100	99, 89	fssresd 5374	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (𝐹 ↾ 𝐴):𝐴⟶𝑌)
101	100	biantrurd 303	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → (∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦)))))
102	98, 101	bitr4d 190	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐾 ∈ Top) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃) ↔ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
103	1, 2, 6, 84, 77, 102	syl221anc 1244	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → ((𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃) ↔ ∀𝑦 ∈ 𝐾 (((𝐹 ↾ 𝐴)‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ (𝐽 ↾t 𝐴)(𝑃 ∈ 𝑧 ∧ ((𝐹 ↾ 𝐴) “ 𝑧) ⊆ 𝑦))))
104	74, 86, 103	3bitr4d 219	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 973   = wceq 1348   ∈ wcel 2141  ∀wral 2448  ∃wrex 2449  Vcvv 2730   ∩ cin 3120   ⊆ wss 3121  ∪ cuni 3796   ↾ cres 4613   “ cima 4614  ⟶wf 5194  ‘cfv 5198  (class class class)co 5853   ↾_t crest 12579  Topctop 12789  TopOnctopon 12802  intcnt 12887   CnP ccnp 12980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-map 6628  df-rest 12581  df-topgen 12600  df-top 12790  df-topon 12803  df-bases 12835  df-ntr 12890  df-cnp 12983

This theorem is referenced by: (None)