Metamath Proof Explorer

Theorem cnpnei

Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009)

Ref Expression
Hypotheses cnpnei.1 ⊢ 𝑋 = ∪ 𝐽
cnpnei.2 ⊢ 𝑌 = ∪ 𝐾
Assertion cnpnei ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 cnpnei.1 ⊢ 𝑋 = ∪ 𝐽
2 cnpnei.2 ⊢ 𝑌 = ∪ 𝐾
3 cnvimass ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
4 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
5 3 4 sseqtrid ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
6 5 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
7 6 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
8 neii2 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) → ∃ 𝑔 ∈ 𝐾 ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) )
9 8 3ad2antl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) → ∃ 𝑔 ∈ 𝐾 ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) )
10 9 ad2ant2rl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → ∃ 𝑔 ∈ 𝐾 ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) )
11 simpll ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
12 simprl ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → 𝑔 ∈ 𝐾 )
13 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
14 13 snss ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 )
15 14 biranri ⊢ ( ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 )
16 15 ad2antll ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 )
17 11 12 16 3jca ⊢ ( ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑔 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 ) )
18 17 adantll ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑔 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 ) )
19 cnpimaex ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑔 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑔 ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ( 𝐹 “ 𝑜 ) ⊆ 𝑔 ) )
20 18 19 syl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ( 𝐹 “ 𝑜 ) ⊆ 𝑔 ) )
21 sstr2 ⊢ ( ( 𝐹 “ 𝑜 ) ⊆ 𝑔 → ( 𝑔 ⊆ 𝑦 → ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ) )
22 21 com12 ⊢ ( 𝑔 ⊆ 𝑦 → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑔 → ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ) )
23 22 ad2antll ⊢ ( ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑔 → ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ) )
24 23 ad2antlr ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑔 → ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ) )
25 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
26 25 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → Fun 𝐹 )
27 26 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → Fun 𝐹 )
28 27 ad2antrr ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → Fun 𝐹 )
29 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ 𝑋 )
30 29 adantlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ 𝑋 )
31 4 sseq2d ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋 ) )
32 31 ad2antlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑜 ⊆ dom 𝐹 ↔ 𝑜 ⊆ 𝑋 ) )
33 30 32 mpbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ dom 𝐹 )
34 33 3adantl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ dom 𝐹 )
35 34 adantlr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ dom 𝐹 )
36 35 ad4ant14 ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ dom 𝐹 )
37 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑜 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ↔ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
38 28 36 37 syl2anc ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑦 ↔ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
39 24 38 sylibd ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑜 ) ⊆ 𝑔 → 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
40 39 anim2d ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑜 ∧ ( 𝐹 “ 𝑜 ) ⊆ 𝑔 ) → ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
41 40 reximdva ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ( ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ ( 𝐹 “ 𝑜 ) ⊆ 𝑔 ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) )
42 20 41 mpd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) ∧ ( 𝑔 ∈ 𝐾 ∧ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦 ) ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
43 10 42 rexlimddv ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) )
44 1 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 ∧ ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
45 44 3ad2antl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 ∧ ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
46 45 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 ∧ ∃ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
47 7 43 46 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
48 47 exp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ( 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
49 48 ralrimdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
50 simpll3 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
51 opnneip ⊢ ( ( 𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ) → 𝑜 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) )
52 imaeq2 ⊢ ( 𝑦 = 𝑜 → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ 𝑜 ) )
53 52 eleq1d ⊢ ( 𝑦 = 𝑜 → ( ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
54 53 rspcv ⊢ ( 𝑜 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
55 51 54 syl ⊢ ( ( 𝐾 ∈ Top ∧ 𝑜 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
56 55 3com23 ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
57 56 3expb ⊢ ( ( 𝐾 ∈ Top ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
58 57 3ad2antl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
59 58 adantlr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
60 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∃ 𝑔 ∈ 𝐽 ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) )
61 60 ex ⊢ ( 𝐽 ∈ Top → ( ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑔 ∈ 𝐽 ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) ) )
62 61 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑔 ∈ 𝐽 ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) ) )
63 62 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ( ◡ 𝐹 “ 𝑜 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑔 ∈ 𝐽 ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) ) )
64 snssg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑔 ↔ { 𝐴 } ⊆ 𝑔 ) )
65 64 ad3antlr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑔 ↔ { 𝐴 } ⊆ 𝑔 ) )
66 26 ad3antrrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → Fun 𝐹 )
67 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑔 ∈ 𝐽 ) → 𝑔 ⊆ 𝑋 )
68 67 3ad2antl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑔 ∈ 𝐽 ) → 𝑔 ⊆ 𝑋 )
69 4 sseq2d ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋 ) )
70 69 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑔 ⊆ dom 𝐹 ↔ 𝑔 ⊆ 𝑋 ) )
71 70 biimpar ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑔 ⊆ 𝑋 ) → 𝑔 ⊆ dom 𝐹 )
72 68 71 syldan ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑔 ∈ 𝐽 ) → 𝑔 ⊆ dom 𝐹 )
73 72 ad4ant14 ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → 𝑔 ⊆ dom 𝐹 )
74 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑔 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ↔ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) )
75 66 73 74 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ↔ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) )
76 65 75 anbi12d ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ↔ ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) ) )
77 76 biimprd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) ∧ 𝑔 ∈ 𝐽 ) → ( ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) → ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) )
78 77 reximdva ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ∃ 𝑔 ∈ 𝐽 ( { 𝐴 } ⊆ 𝑔 ∧ 𝑔 ⊆ ( ◡ 𝐹 “ 𝑜 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) )
79 59 63 78 3syld ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 ∧ 𝑜 ∈ 𝐾 ) ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) )
80 79 exp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ( 𝑜 ∈ 𝐾 → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
81 80 com24 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝑜 ∈ 𝐾 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
82 81 imp ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑜 ∈ 𝐾 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) )
83 82 ralrimiv ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) )
84 1 2 iscnp2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
85 84 baib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
86 85 3expa ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
87 86 3adantl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
88 87 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑜 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑜 → ∃ 𝑔 ∈ 𝐽 ( 𝐴 ∈ 𝑔 ∧ ( 𝐹 “ 𝑔 ) ⊆ 𝑜 ) ) ) ) )
89 50 83 88 mpbir2and ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
90 89 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) )
91 49 90 impbid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐾 ) ‘ { ( 𝐹 ‘ 𝐴 ) } ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )