This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )