MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnpnei Structured version   Visualization version   GIF version

Theorem cnpnei 21116
Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
Hypotheses
Ref Expression
cnpnei.1 𝑋 = 𝐽
cnpnei.2 𝑌 = 𝐾
Assertion
Ref Expression
cnpnei (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹   𝑦,𝐽   𝑦,𝐾   𝑦,𝑋   𝑦,𝑌

Proof of Theorem cnpnei
Dummy variables 𝑔 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 5520 . . . . . . . 8 (𝐹𝑦) ⊆ dom 𝐹
2 fdm 6089 . . . . . . . 8 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
31, 2syl5sseq 3686 . . . . . . 7 (𝐹:𝑋𝑌 → (𝐹𝑦) ⊆ 𝑋)
433ad2ant3 1104 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝐹𝑦) ⊆ 𝑋)
54ad2antrr 762 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ⊆ 𝑋)
6 neii2 20960 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
763ad2antl2 1244 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
87ad2ant2rl 800 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
9 simpll 805 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
10 simprl 809 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝑔𝐾)
11 fvex 6239 . . . . . . . . . . . . . 14 (𝐹𝐴) ∈ V
1211snss 4348 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ 𝑔 ↔ {(𝐹𝐴)} ⊆ 𝑔)
1312biimpri 218 . . . . . . . . . . . 12 ({(𝐹𝐴)} ⊆ 𝑔 → (𝐹𝐴) ∈ 𝑔)
1413adantr 480 . . . . . . . . . . 11 (({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦) → (𝐹𝐴) ∈ 𝑔)
1514ad2antll 765 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹𝐴) ∈ 𝑔)
169, 10, 153jca 1261 . . . . . . . . 9 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
1716adantll 750 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
18 cnpimaex 21108 . . . . . . . 8 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
1917, 18syl 17 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
20 sstr2 3643 . . . . . . . . . . . . 13 ((𝐹𝑜) ⊆ 𝑔 → (𝑔𝑦 → (𝐹𝑜) ⊆ 𝑦))
2120com12 32 . . . . . . . . . . . 12 (𝑔𝑦 → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2221ad2antll 765 . . . . . . . . . . 11 ((𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦)) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2322ad2antlr 763 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
24 ffun 6086 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
25243ad2ant3 1104 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → Fun 𝐹)
2625ad2antrr 762 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → Fun 𝐹)
2726ad2antrr 762 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → Fun 𝐹)
28 cnpnei.1 . . . . . . . . . . . . . . . . . 18 𝑋 = 𝐽
2928eltopss 20760 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑜𝐽) → 𝑜𝑋)
3029adantlr 751 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜𝑋)
312sseq2d 3666 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋𝑌 → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3231ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3330, 32mpbird 247 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
34333adantl2 1238 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3534adantlr 751 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3635adantlr 751 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3736adantlr 751 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
38 funimass3 6373 . . . . . . . . . . 11 ((Fun 𝐹𝑜 ⊆ dom 𝐹) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
3927, 37, 38syl2anc 694 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
4023, 39sylibd 229 . . . . . . . . 9 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔𝑜 ⊆ (𝐹𝑦)))
4140anim2d 588 . . . . . . . 8 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4241reximdva 3046 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4319, 42mpd 15 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
448, 43rexlimddv 3064 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
4528isneip 20957 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
46453ad2antl1 1243 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
4746adantr 480 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
485, 44, 47mpbir2and 977 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
4948exp32 630 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
5049ralrimdv 2997 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
51 simpll3 1122 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋𝑌)
52 opnneip 20971 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))
53 imaeq2 5497 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑜 → (𝐹𝑦) = (𝐹𝑜))
5453eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑦 = 𝑜 → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5554rspcv 3336 . . . . . . . . . . . . . 14 (𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5652, 55syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57563com23 1291 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ (𝐹𝐴) ∈ 𝑜𝑜𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58573expb 1285 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
59583ad2antl2 1244 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
6059adantlr 751 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
61 neii2 20960 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)))
6261ex 449 . . . . . . . . . . 11 (𝐽 ∈ Top → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
63623ad2ant1 1102 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
6463ad2antrr 762 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
65 snssg 4347 . . . . . . . . . . . . 13 (𝐴𝑋 → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6665ad3antlr 767 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6725ad3antrrr 766 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → Fun 𝐹)
6828eltopss 20760 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑔𝐽) → 𝑔𝑋)
69683ad2antl1 1243 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔𝑋)
702sseq2d 3666 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑋𝑌 → (𝑔 ⊆ dom 𝐹𝑔𝑋))
71703ad2ant3 1104 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝑔 ⊆ dom 𝐹𝑔𝑋))
7271biimpar 501 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝑋) → 𝑔 ⊆ dom 𝐹)
7369, 72syldan 486 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
7473adantlr 751 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
7574adantlr 751 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
76 funimass3 6373 . . . . . . . . . . . . 13 ((Fun 𝐹𝑔 ⊆ dom 𝐹) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7767, 75, 76syl2anc 694 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7866, 77anbi12d 747 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
7978biimprd 238 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8079reximdva 3046 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8160, 64, 803syld 60 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8281exp32 630 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝐴) ∈ 𝑜 → (𝑜𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8382com24 95 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8483imp 444 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜))))
8584ralrimiv 2994 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
86 cnpnei.2 . . . . . . . . 9 𝑌 = 𝐾
8728, 86iscnp2 21091 . . . . . . . 8 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8887baib 964 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
89883expa 1284 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
90893adantl3 1239 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9190adantr 480 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9251, 85, 91mpbir2and 977 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
9392ex 449 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
9450, 93impbid 202 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  wss 3607  {csn 4210   cuni 4468  ccnv 5142  dom cdm 5143  cima 5146  Fun wfun 5920  wf 5922  cfv 5926  (class class class)co 6690  Topctop 20746  neicnei 20949   CnP ccnp 21077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-top 20747  df-topon 20764  df-nei 20950  df-cnp 21080
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator