Theorem iscnp4 15012

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 15001	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
2	1	3expa 1230	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
3	2	3adantl3 1182	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
4		simpll1 1063	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐽 ∈ (TopOn‘𝑋))
5		simpll2 1064	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐾 ∈ (TopOn‘𝑌))
6		simpll3 1065	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑃 ∈ 𝑋)
7		simplr 529	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
8		topontop 14808	. . . . . . . . 9 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
9	5, 8	syl 14	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝐾 ∈ Top)
10		eqid 2231	. . . . . . . . . 10 ⊢ ∪ 𝐾 = ∪ 𝐾
11	10	neii1 14941	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑦 ⊆ ∪ 𝐾)
12	9, 11	sylancom 420	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑦 ⊆ ∪ 𝐾)
13	10	ntropn 14911	. . . . . . . 8 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾) → ((int‘𝐾)‘𝑦) ∈ 𝐾)
14	9, 12, 13	syl2anc 411	. . . . . . 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 5791	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ 𝑌)
18		toponuni 14809	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾)
19	5, 18	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → 𝑌 = ∪ 𝐾)
20	17, 19	eleqtrd 2310	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ ∪ 𝐾)
21	20	snssd 3823	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → {(𝐹‘𝑃)} ⊆ ∪ 𝐾)
22	10	neiint 14939	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Top ∧ {(𝐹‘𝑃)} ⊆ ∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
23	9, 21, 12, 22	syl3anc 1274	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}) ↔ {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦)))
24	15, 23	mpbid 147	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → {(𝐹‘𝑃)} ⊆ ((int‘𝐾)‘𝑦))
25		fvexg 5667	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑃 ∈ 𝑋) → (𝐹‘𝑃) ∈ V)
26	7, 6, 25	syl2anc 411	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → (𝐹‘𝑃) ∈ V)
27		snssg 3812	. . . . . . . . 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 15005	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ ((int‘𝐾)‘𝑦) ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ ((int‘𝐾)‘𝑦))) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))
31	4, 5, 6, 7, 14, 29, 30	syl33anc 1289	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))
32		simpl1 1027	. . . . . . . . 9 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐽 ∈ (TopOn‘𝑋))
33	32	ad2antrr 488	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ (TopOn‘𝑋))
34		topontop 14808	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
35	33, 34	syl 14	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝐽 ∈ Top)
36		simprl 531	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥 ∈ 𝐽)
37		simprrl 541	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑃 ∈ 𝑥)
38		opnneip 14953	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
39	35, 36, 37, 38	syl3anc 1274	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
40		simprrr 542	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦))
41	10	ntrss2 14915	. . . . . . . . 9 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
42	9, 12, 41	syl2anc 411	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
43	42	adantr 276	. . . . . . 7 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → ((int‘𝐾)‘𝑦) ⊆ 𝑦)
44	40, 43	sstrd 3238	. . . . . 6 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) ∧ (𝑥 ∈ 𝐽 ∧ (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ ((int‘𝐾)‘𝑦)))) → (𝐹 “ 𝑥) ⊆ 𝑦)
45	31, 39, 44	reximssdv 2637	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})) → ∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)
46	45	ralrimiva 2606	. . . 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 1064	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝐾 ∈ (TopOn‘𝑌))
50	49, 8	syl 14	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝐾 ∈ Top)
51		simprl 531	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑦 ∈ 𝐾)
52		simprr 533	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → (𝐹‘𝑃) ∈ 𝑦)
53		opnneip 14953	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Top ∧ 𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}))
54	50, 51, 52, 53	syl3anc 1274	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)}))
55		simpl1 1027	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → 𝐽 ∈ (TopOn‘𝑋))
56	55	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝐽 ∈ (TopOn‘𝑋))
57	56, 34	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝐽 ∈ Top)
58		simprl 531	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑥 ∈ ((nei‘𝐽)‘{𝑃}))
59		eqid 2231	. . . . . . . . . . . . . 14 ⊢ ∪ 𝐽 = ∪ 𝐽
60	59	neii1 14941	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑥 ⊆ ∪ 𝐽)
61	57, 58, 60	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑥 ⊆ ∪ 𝐽)
62	59	ntropn 14911	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
63	57, 61, 62	syl2anc 411	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ∈ 𝐽)
64		simpll3 1065	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) → 𝑃 ∈ 𝑋)
65	64	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑃 ∈ 𝑋)
66		toponuni 14809	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
67	56, 66	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑋 = ∪ 𝐽)
68	65, 67	eleqtrd 2310	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → 𝑃 ∈ ∪ 𝐽)
69	68	snssd 3823	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → {𝑃} ⊆ ∪ 𝐽)
70	59	neiint 14939	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ {𝑃} ⊆ ∪ 𝐽 ∧ 𝑥 ⊆ ∪ 𝐽) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
71	57, 69, 61, 70	syl3anc 1274	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ↔ {𝑃} ⊆ ((int‘𝐽)‘𝑥)))
72	58, 71	mpbid 147	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → {𝑃} ⊆ ((int‘𝐽)‘𝑥))
73		snssg 3812	. . . . . . . . . . . . 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 14915	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
77	57, 61, 76	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ((int‘𝐽)‘𝑥) ⊆ 𝑥)
78		imass2 5119	. . . . . . . . . . . . 13 ⊢ (((int‘𝐽)‘𝑥) ⊆ 𝑥 → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹 “ 𝑥))
79	77, 78	syl 14	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ (𝐹 “ 𝑥))
80		simprr 533	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ 𝑥) ⊆ 𝑦)
81	79, 80	sstrd 3238	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)
82		eleq2 2295	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ ((int‘𝐽)‘𝑥)))
83		imaeq2 5078	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → (𝐹 “ 𝑧) = (𝐹 “ ((int‘𝐽)‘𝑥)))
84	83	sseq1d 3257	. . . . . . . . . . . . 13 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → ((𝐹 “ 𝑧) ⊆ 𝑦 ↔ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦))
85	82, 84	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑧 = ((int‘𝐽)‘𝑥) → ((𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦) ↔ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)))
86	85	rspcev 2911	. . . . . . . . . . 11 ⊢ ((((int‘𝐽)‘𝑥) ∈ 𝐽 ∧ (𝑃 ∈ ((int‘𝐽)‘𝑥) ∧ (𝐹 “ ((int‘𝐽)‘𝑥)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
87	63, 75, 81, 86	syl12anc 1272	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦)) ∧ (𝑥 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))
88	87	rexlimdvaa 2652	. . . . . . . . 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 2603	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦 → ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦))))
94	93	imdistanda 448	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑧 ∈ 𝐽 (𝑃 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ 𝑦)))))
95		iscnp 14993	. . 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 1005   = wceq 1398   ∈ wcel 2202  ∀wral 2511  ∃wrex 2512  Vcvv 2803   ⊆ wss 3201  {csn 3673  ∪ cuni 3898   “ cima 4734  ⟶wf 5329  ‘cfv 5333  (class class class)co 6028  Topctop 14791  TopOnctopon 14804  intcnt 14887  neicnei 14932   CnP ccnp 14980

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4209  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-csb 3129  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-iun 3977  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340  df-fv 5341  df-ov 6031  df-oprab 6032  df-mpo 6033  df-1st 6312  df-2nd 6313  df-map 6862  df-top 14792  df-topon 14805  df-ntr 14890  df-nei 14933  df-cnp 14983

This theorem is referenced by:  cnnei  15026