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

Theorem cnpnei 21279
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 5695 . . . . . . . 8 (𝐹𝑦) ⊆ dom 𝐹
2 fdm 6260 . . . . . . . 8 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
31, 2syl5sseq 3850 . . . . . . 7 (𝐹:𝑋𝑌 → (𝐹𝑦) ⊆ 𝑋)
433ad2ant3 1158 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝐹𝑦) ⊆ 𝑋)
54ad2antrr 708 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ⊆ 𝑋)
6 neii2 21123 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
763ad2antl2 1230 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
87ad2ant2rl 746 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
9 simpll 774 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
10 simprl 778 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝑔𝐾)
11 fvex 6417 . . . . . . . . . . . . . 14 (𝐹𝐴) ∈ V
1211snss 4506 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ 𝑔 ↔ {(𝐹𝐴)} ⊆ 𝑔)
1312biimpri 219 . . . . . . . . . . . 12 ({(𝐹𝐴)} ⊆ 𝑔 → (𝐹𝐴) ∈ 𝑔)
1413adantr 468 . . . . . . . . . . 11 (({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦) → (𝐹𝐴) ∈ 𝑔)
1514ad2antll 711 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹𝐴) ∈ 𝑔)
169, 10, 153jca 1151 . . . . . . . . 9 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
1716adantll 696 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
18 cnpimaex 21271 . . . . . . . 8 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
1917, 18syl 17 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
20 sstr2 3805 . . . . . . . . . . . . 13 ((𝐹𝑜) ⊆ 𝑔 → (𝑔𝑦 → (𝐹𝑜) ⊆ 𝑦))
2120com12 32 . . . . . . . . . . . 12 (𝑔𝑦 → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2221ad2antll 711 . . . . . . . . . . 11 ((𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦)) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2322ad2antlr 709 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
24 ffun 6255 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
25243ad2ant3 1158 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → Fun 𝐹)
2625ad2antrr 708 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → Fun 𝐹)
2726ad2antrr 708 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → Fun 𝐹)
28 cnpnei.1 . . . . . . . . . . . . . . . . . 18 𝑋 = 𝐽
2928eltopss 20922 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑜𝐽) → 𝑜𝑋)
3029adantlr 697 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜𝑋)
312sseq2d 3830 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋𝑌 → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3231ad2antlr 709 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3330, 32mpbird 248 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
34333adantl2 1201 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3534adantlr 697 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3635adantlr 697 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3736adantlr 697 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
38 funimass3 6551 . . . . . . . . . . 11 ((Fun 𝐹𝑜 ⊆ dom 𝐹) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
3927, 37, 38syl2anc 575 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
4023, 39sylibd 230 . . . . . . . . 9 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔𝑜 ⊆ (𝐹𝑦)))
4140anim2d 601 . . . . . . . 8 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4241reximdva 3204 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4319, 42mpd 15 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
448, 43rexlimddv 3223 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
4528isneip 21120 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
46453ad2antl1 1229 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
4746adantr 468 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
485, 44, 47mpbir2and 695 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
4948exp32 409 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
5049ralrimdv 3156 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
51 simpll3 1266 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋𝑌)
52 opnneip 21134 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))
53 imaeq2 5672 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑜 → (𝐹𝑦) = (𝐹𝑜))
5453eleq1d 2870 . . . . . . . . . . . . . . 15 (𝑦 = 𝑜 → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5554rspcv 3498 . . . . . . . . . . . . . 14 (𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5652, 55syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57563com23 1149 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ (𝐹𝐴) ∈ 𝑜𝑜𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58573expb 1142 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
59583ad2antl2 1230 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
6059adantlr 697 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
61 neii2 21123 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)))
6261ex 399 . . . . . . . . . . 11 (𝐽 ∈ Top → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
63623ad2ant1 1156 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
6463ad2antrr 708 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
65 snssg 4505 . . . . . . . . . . . . 13 (𝐴𝑋 → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6665ad3antlr 713 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6725ad3antrrr 712 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → Fun 𝐹)
6828eltopss 20922 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑔𝐽) → 𝑔𝑋)
69683ad2antl1 1229 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔𝑋)
702sseq2d 3830 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑋𝑌 → (𝑔 ⊆ dom 𝐹𝑔𝑋))
71703ad2ant3 1158 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝑔 ⊆ dom 𝐹𝑔𝑋))
7271biimpar 465 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝑋) → 𝑔 ⊆ dom 𝐹)
7369, 72syldan 581 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
7473adantlr 697 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
7574adantlr 697 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
76 funimass3 6551 . . . . . . . . . . . . 13 ((Fun 𝐹𝑔 ⊆ dom 𝐹) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7767, 75, 76syl2anc 575 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7866, 77anbi12d 618 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
7978biimprd 239 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8079reximdva 3204 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8160, 64, 803syld 60 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8281exp32 409 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝐴) ∈ 𝑜 → (𝑜𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8382com24 95 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8483imp 395 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜))))
8584ralrimiv 3153 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
86 cnpnei.2 . . . . . . . . 9 𝑌 = 𝐾
8728, 86iscnp2 21254 . . . . . . . 8 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8887baib 527 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
89883expa 1140 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
90893adantl3 1202 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9190adantr 468 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9251, 85, 91mpbir2and 695 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
9392ex 399 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
9450, 93impbid 203 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  wss 3769  {csn 4370   cuni 4630  ccnv 5310  dom cdm 5311  cima 5314  Fun wfun 6091  wf 6093  cfv 6097  (class class class)co 6870  Topctop 20908  neicnei 21112   CnP ccnp 21240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-1st 7394  df-2nd 7395  df-map 8090  df-top 20909  df-topon 20926  df-nei 21113  df-cnp 21243
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator