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

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