Theorem iscnp4 15242

Description: The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃 " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)

Assertion

Ref	Expression
iscnp4	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦   𝑥,𝑃,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Proof of Theorem iscnp4

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnpf2 15231	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
2	1	3expa 1234	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
3	2	3adantl3 1186	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
4		simpll1 1067	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐽 ∈ (TopOn‘𝑋))
5		simpll2 1068	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐾 ∈ (TopOn‘𝑌))
6		simpll3 1069	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑃 ∈ 𝑋)
7		simplr 533	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
8		topontop 15038	. . . . . . . . 9 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
9	5, 8	syl 14	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐾 ∈ Top)
10		eqid 2238	. . . . . . . . . 10 ⊢ ∪ 𝐾 = ∪ 𝐾
11	10	neii1 15171	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑦 ⊆ ∪ 𝐾)
12	9, 11	sylancom 424	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑦 ⊆ ∪ 𝐾)
13	10	ntropn 15141	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾) → ((int‘𝐾)‘𝑦) ∈ 𝐾)
14	9, 12, 13	syl2anc 415	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ((int‘𝐾)‘𝑦) ∈ 𝐾)
15		simpr 110	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}))
16	3	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐹:𝑋⟶𝑌)
17	16, 6	ffvelcdmd 5835	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ 𝑌)
18		toponuni 15039	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
19	5, 18	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑌 = ∪ 𝐾)
20	17, 19	eleqtrd 2317	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ ∪ 𝐾)
21	20	snssd 3855	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → {(𝐹‘𝑃)} ⊆ ∪ 𝐾)
22	10	neiint 15169	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Top ∧ {(𝐹‘𝑃)} ⊆ ∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
23	9, 21, 12, 22	syl3anc 1278	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
24	15, 23	mpbid 147	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦))
25		fvexg 5709	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑃 ∈ 𝑋) → (𝐹‘𝑃) ∈ V)
26	7, 6, 25	syl2anc 415	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ V)
27		snssg 3844	. . . . . . . . 9 ⊢ ((𝐹‘𝑃) ∈ V → ((𝐹‘𝑃) ∈ ((int‘𝐾)‘𝑦) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
28	26, 27	syl 14	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ((𝐹‘𝑃) ∈ ((int‘𝐾)‘𝑦) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
29	24, 28	mpbird 167	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ ((int‘𝐾)‘𝑦))
30		icnpimaex 15235	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ ((int‘𝐾)‘𝑦) ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ ((int‘𝐾)‘𝑦))) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))
31	4, 5, 6, 7, 14, 29, 30	syl33anc 1293	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))
32		simpl1 1031	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
33	32	ad2antrr 492	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ (TopOn‘𝑋))
34		topontop 15038	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
35	33, 34	syl 14	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ Top)
36		simprl 535	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥 ∈ 𝐽)
37		simprrl 545	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑃 ∈ 𝑥)
38		opnneip 15183	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
39	35, 36, 37, 38	syl3anc 1278	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
40		simprrr 546	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦))
41	10	ntrss2 15145	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
42	9, 12, 41	syl2anc 415	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
43	42	adantr 276	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
44	40, 43	sstrd 3258	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹 “ 𝑥) ⊆ 𝑦)
45	31, 39, 44	reximssdv 2654	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)
46	45	ralrimiva 2623	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)
47	3, 46	jca 306	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦))
48	47	ex 115	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)))
49		simpll2 1068	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝐾 ∈ (TopOn‘𝑌))
50	49, 8	syl 14	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝐾 ∈ Top)
51		simprl 535	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑦 ∈ 𝐾)
52		simprr 537	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → (𝐹‘𝑃) ∈ 𝑦)
53		opnneip 15183	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}))
54	50, 51, 52, 53	syl3anc 1278	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}))
55		simpl1 1031	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → 𝐽 ∈ (TopOn‘𝑋))
56	55	ad2antrr 492	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝐽 ∈ (TopOn‘𝑋))
57	56, 34	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝐽 ∈ Top)
58		simprl 535	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
59		eqid 2238	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
60	59	neii1 15171	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑥 ⊆ ∪ 𝐽)
61	57, 58, 60	syl2anc 415	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑥 ⊆ ∪ 𝐽)
62	59	ntropn 15141	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
63	57, 61, 62	syl2anc 415	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
64		simpll3 1069	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑃 ∈ 𝑋)
65	64	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑃 ∈ 𝑋)
66		toponuni 15039	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
67	56, 66	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑋 = ∪ 𝐽)
68	65, 67	eleqtrd 2317	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑃 ∈ ∪ 𝐽)
69	68	snssd 3855	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → {𝑃} ⊆ ∪ 𝐽)
70	59	neiint 15169	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ {𝑃} ⊆ ∪ 𝐽 ∧ 𝑥 ⊆ ∪ 𝐽) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
71	57, 69, 61, 70	syl3anc 1278	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
72	58, 71	mpbid 147	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → {𝑃} ⊆ ((int‘𝐽)‘𝑥))
73		snssg 3844	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ ((int‘𝐽)‘𝑥) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
74	65, 73	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝑃 ∈ ((int‘𝐽)‘𝑥) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
75	72, 74	mpbird 167	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑃 ∈ ((int‘𝐽)‘𝑥))
76	59	ntrss2 15145	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
77	57, 61, 76	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
78		imass2 5158	. . . . . . . . . . . . 13 ⊢ (((int‘𝐽)‘𝑥) ⊆ 𝑥 → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹 “ 𝑥))
79	77, 78	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹 “ 𝑥))
80		simprr 537	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ 𝑥) ⊆ 𝑦)
81	79, 80	sstrd 3258	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)
82		eleq2 2302	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ ((int‘𝐽)‘𝑥)))
83		imaeq2 5117	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → (𝐹 “ 𝑧) = (𝐹 “ ((int‘𝐽)‘𝑥)))
84	83	sseq1d 3277	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦))
85	82, 84	anbi12d 477	. . . . . . . . . . . 12 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)))
86	85	rspcev 2929	. . . . . . . . . . 11 ⊢ ((((int‘𝐽)‘𝑥) ∈ 𝐽 ∧ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
87	63, 75, 81, 86	syl12anc 1276	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
88	87	rexlimdvaa 2669	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → (∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
89	54, 88	embantd 56	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))
90	89	ex 115	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))))
91	90	com23 78	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → ((𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))))
92	91	exp4a 366	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → ((𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → (𝑦 ∈ 𝐾 → ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))))
93	92	ralimdv2 2620	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦 → ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))))
94	93	imdistanda 452	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))))
95		iscnp 15223	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))))
96	94, 95	sylibrd 169	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)))
97	48, 96	impbid 129	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  ∀wral 2528  ∃wrex 2529  Vcvv 2821   ⊆ wss 3220  {csn 3705  ∪ cuni 3930   “ cima 4772  ⟶wf 5368  ‘cfv 5372  (class class class)co 6075  Topctop 15021  TopOnctopon 15034  intcnt 15117  neicnei 15162   CnP ccnp 15210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4241  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-ov 6078  df-oprab 6079  df-mpo 6080  df-1st 6364  df-2nd 6365  df-map 6914  df-top 15022  df-topon 15035  df-ntr 15120  df-nei 15163  df-cnp 15213

This theorem is referenced by:  cnnei  15256