Theorem iscnp4

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

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

Proof

Step	Hyp	Ref	Expression
1		cnpf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
2	1	3expa	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3	2	3adantl3	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
4		simplr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
5		simpll2	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
6		topontop	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
7	5 6	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝐾 ∈ Top )
8		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
9	8	neii1	⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝑦 ⊆ ∪ 𝐾 )
10	7 9	sylancom	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝑦 ⊆ ∪ 𝐾 )
11	8	ntropn	⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ∈ 𝐾 )
12	7 10 11	syl2anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ∈ 𝐾 )
13		simpr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) )
14	3	adantr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
15		simpll3	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝑃 ∈ 𝑋 )
16	14 15	ffvelcdmd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
17		toponuni	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
18	5 17	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → 𝑌 = ∪ 𝐾 )
19	16 18	eleqtrd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ∪ 𝐾 )
20	19	snssd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → { ( 𝐹 ‘ 𝑃 ) } ⊆ ∪ 𝐾 )
21	8	neiint	⊢ ( ( 𝐾 ∈ Top ∧ { ( 𝐹 ‘ 𝑃 ) } ⊆ ∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ↔ { ( 𝐹 ‘ 𝑃 ) } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) )
22	7 20 10 21	syl3anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ↔ { ( 𝐹 ‘ 𝑃 ) } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) )
23	13 22	mpbid	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → { ( 𝐹 ‘ 𝑃 ) } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) )
24		fvex	⊢ ( 𝐹 ‘ 𝑃 ) ∈ V
25	24	snss	⊢ ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ↔ { ( 𝐹 ‘ 𝑃 ) } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) )
26	23 25	sylibr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( 𝐹 ‘ 𝑃 ) ∈ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) )
27		cnpimaex	⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) )
28	4 12 26 27	syl3anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) )
29		simpl1	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
30	29	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
31		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
32	30 31	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → 𝐽 ∈ Top )
33		simprl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → 𝑥 ∈ 𝐽 )
34		simprrl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → 𝑃 ∈ 𝑥 )
35		opnneip	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑃 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
36	32 33 34 35	syl3anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
37		simprrr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) )
38	8	ntrss2	⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ⊆ 𝑦 )
39	7 10 38	syl2anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ⊆ 𝑦 )
40	39	adantr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ⊆ 𝑦 )
41	37 40	sstrd	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑦 )
42	28 36 41	reximssdv	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 )
43	42	ralrimiva	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 )
44	3 43	jca	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
45	44	ex	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )
46		simpll2	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
47	46 6	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → 𝐾 ∈ Top )
48		simprl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → 𝑦 ∈ 𝐾 )
49		simprr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 )
50		opnneip	⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) → 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) )
51	47 48 49 50	syl3anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) )
52		simpl1	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
53	52	ad2antrr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
54	53 31	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝐽 ∈ Top )
55		simprl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
56		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
57	56	neii1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → 𝑥 ⊆ ∪ 𝐽 )
58	54 55 57	syl2anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑥 ⊆ ∪ 𝐽 )
59	56	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐽 )
60	54 58 59	syl2anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐽 )
61		simpll3	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → 𝑃 ∈ 𝑋 )
62	61	adantr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑃 ∈ 𝑋 )
63		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
64	53 63	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑋 = ∪ 𝐽 )
65	62 64	eleqtrd	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑃 ∈ ∪ 𝐽 )
66	65	snssd	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → { 𝑃 } ⊆ ∪ 𝐽 )
67	56	neiint	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ ∪ 𝐽 ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
68	54 66 58 67	syl3anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
69	55 68	mpbid	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) )
70		snssg	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ↔ { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
71	62 70	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ↔ { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
72	69 71	mpbird	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) )
73	56	ntrss2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 )
74	54 58 73	syl2anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 )
75		imass2	⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑥 → ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( 𝐹 “ 𝑥 ) )
76	74 75	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( 𝐹 “ 𝑥 ) )
77		simprr	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑦 )
78	76 77	sstrd	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝑦 )
79		eleq2	⊢ ( 𝑧 = ( ( int ‘ 𝐽 ) ‘ 𝑥 ) → ( 𝑃 ∈ 𝑧 ↔ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
80		imaeq2	⊢ ( 𝑧 = ( ( int ‘ 𝐽 ) ‘ 𝑥 ) → ( 𝐹 “ 𝑧 ) = ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) )
81	80	sseq1d	⊢ ( 𝑧 = ( ( int ‘ 𝐽 ) ‘ 𝑥 ) → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ↔ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝑦 ) )
82	79 81	anbi12d	⊢ ( 𝑧 = ( ( int ‘ 𝐽 ) ‘ 𝑥 ) → ( ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∧ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝑦 ) ) )
83	82	rspcev	⊢ ( ( ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ∧ ( 𝐹 “ ( ( int ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) )
84	60 72 78 83	syl12anc	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) ∧ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) )
85	84	rexlimdvaa	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) )
86	51 85	embantd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) ) → ( ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) )
87	86	ex	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) → ( ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) )
88	87	com23	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( ( 𝑦 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) )
89	88	exp4a	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) → ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝑦 ∈ 𝐾 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
90	89	ralimdv2	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) )
91	90	imdistanda	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
92		iscnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝑃 ∈ 𝑧 ∧ ( 𝐹 “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
93	91 92	sylibrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) )
94	45 93	impbid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝑃 ) } ) ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )