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

Theorem cnpnei 22615
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 6033 . . . . . . . 8 (𝐹𝑦) ⊆ dom 𝐹
2 fdm 6677 . . . . . . . 8 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
31, 2sseqtrid 3996 . . . . . . 7 (𝐹:𝑋𝑌 → (𝐹𝑦) ⊆ 𝑋)
433ad2ant3 1135 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝐹𝑦) ⊆ 𝑋)
54ad2antrr 724 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ⊆ 𝑋)
6 neii2 22459 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
763ad2antl2 1186 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
87ad2ant2rl 747 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑔𝐾 ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))
9 simpll 765 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
10 simprl 769 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → 𝑔𝐾)
11 fvex 6855 . . . . . . . . . . . . . 14 (𝐹𝐴) ∈ V
1211snss 4746 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ 𝑔 ↔ {(𝐹𝐴)} ⊆ 𝑔)
1312biimpri 227 . . . . . . . . . . . 12 ({(𝐹𝐴)} ⊆ 𝑔 → (𝐹𝐴) ∈ 𝑔)
1413adantr 481 . . . . . . . . . . 11 (({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦) → (𝐹𝐴) ∈ 𝑔)
1514ad2antll 727 . . . . . . . . . 10 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹𝐴) ∈ 𝑔)
169, 10, 153jca 1128 . . . . . . . . 9 (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
1716adantll 712 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔))
18 cnpimaex 22607 . . . . . . . 8 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑔𝐾 ∧ (𝐹𝐴) ∈ 𝑔) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
1917, 18syl 17 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔))
20 sstr2 3951 . . . . . . . . . . . . 13 ((𝐹𝑜) ⊆ 𝑔 → (𝑔𝑦 → (𝐹𝑜) ⊆ 𝑦))
2120com12 32 . . . . . . . . . . . 12 (𝑔𝑦 → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2221ad2antll 727 . . . . . . . . . . 11 ((𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦)) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
2322ad2antlr 725 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔 → (𝐹𝑜) ⊆ 𝑦))
24 ffun 6671 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌 → Fun 𝐹)
25243ad2ant3 1135 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → Fun 𝐹)
2625ad2antrr 724 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → Fun 𝐹)
2726ad2antrr 724 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → Fun 𝐹)
28 cnpnei.1 . . . . . . . . . . . . . . . . 17 𝑋 = 𝐽
2928eltopss 22256 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑜𝐽) → 𝑜𝑋)
3029adantlr 713 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜𝑋)
312sseq2d 3976 . . . . . . . . . . . . . . . 16 (𝐹:𝑋𝑌 → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3231ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → (𝑜 ⊆ dom 𝐹𝑜𝑋))
3330, 32mpbird 256 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
34333adantl2 1167 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3534adantlr 713 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
3635ad4ant14 750 . . . . . . . . . . 11 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → 𝑜 ⊆ dom 𝐹)
37 funimass3 7004 . . . . . . . . . . 11 ((Fun 𝐹𝑜 ⊆ dom 𝐹) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
3827, 36, 37syl2anc 584 . . . . . . . . . 10 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑦𝑜 ⊆ (𝐹𝑦)))
3923, 38sylibd 238 . . . . . . . . 9 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐹𝑜) ⊆ 𝑔𝑜 ⊆ (𝐹𝑦)))
4039anim2d 612 . . . . . . . 8 ((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) ∧ 𝑜𝐽) → ((𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4140reximdva 3165 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → (∃𝑜𝐽 (𝐴𝑜 ∧ (𝐹𝑜) ⊆ 𝑔) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦))))
4219, 41mpd 15 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) ∧ (𝑔𝐾 ∧ ({(𝐹𝐴)} ⊆ 𝑔𝑔𝑦))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
438, 42rexlimddv 3158 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))
4428isneip 22456 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
45443ad2antl1 1185 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
4645adantr 481 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ ((𝐹𝑦) ⊆ 𝑋 ∧ ∃𝑜𝐽 (𝐴𝑜𝑜 ⊆ (𝐹𝑦)))))
475, 43, 46mpbir2and 711 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))
4847exp32 421 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}))))
4948ralrimdv 3149 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
50 simpll3 1214 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹:𝑋𝑌)
51 opnneip 22470 . . . . . . . . . . . . . 14 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → 𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}))
52 imaeq2 6009 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑜 → (𝐹𝑦) = (𝐹𝑜))
5352eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑦 = 𝑜 → ((𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) ↔ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5453rspcv 3577 . . . . . . . . . . . . . 14 (𝑜 ∈ ((nei‘𝐾)‘{(𝐹𝐴)}) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5551, 54syl 17 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝑜𝐾 ∧ (𝐹𝐴) ∈ 𝑜) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
56553com23 1126 . . . . . . . . . . . 12 ((𝐾 ∈ Top ∧ (𝐹𝐴) ∈ 𝑜𝑜𝐾) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
57563expb 1120 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
58573ad2antl2 1186 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
5958adantlr 713 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})))
60 neii2 22459 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)))
6160ex 413 . . . . . . . . . . 11 (𝐽 ∈ Top → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
62613ad2ant1 1133 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
6362ad2antrr 724 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → ((𝐹𝑜) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
64 snssg 4744 . . . . . . . . . . . . 13 (𝐴𝑋 → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6564ad3antlr 729 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (𝐴𝑔 ↔ {𝐴} ⊆ 𝑔))
6625ad3antrrr 728 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → Fun 𝐹)
6728eltopss 22256 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑔𝐽) → 𝑔𝑋)
68673ad2antl1 1185 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔𝑋)
692sseq2d 3976 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋𝑌 → (𝑔 ⊆ dom 𝐹𝑔𝑋))
70693ad2ant3 1135 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) → (𝑔 ⊆ dom 𝐹𝑔𝑋))
7170biimpar 478 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝑋) → 𝑔 ⊆ dom 𝐹)
7268, 71syldan 591 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
7372ad4ant14 750 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → 𝑔 ⊆ dom 𝐹)
74 funimass3 7004 . . . . . . . . . . . . 13 ((Fun 𝐹𝑔 ⊆ dom 𝐹) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7566, 73, 74syl2anc 584 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐹𝑔) ⊆ 𝑜𝑔 ⊆ (𝐹𝑜)))
7665, 75anbi12d 631 . . . . . . . . . . 11 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → ((𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜) ↔ ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜))))
7776biimprd 247 . . . . . . . . . 10 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) ∧ 𝑔𝐽) → (({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
7877reximdva 3165 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∃𝑔𝐽 ({𝐴} ⊆ 𝑔𝑔 ⊆ (𝐹𝑜)) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
7959, 63, 783syld 60 . . . . . . . 8 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ((𝐹𝐴) ∈ 𝑜𝑜𝐾)) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
8079exp32 421 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → ((𝐹𝐴) ∈ 𝑜 → (𝑜𝐾 → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8180com24 95 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8281imp 407 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝑜𝐾 → ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜))))
8382ralrimiv 3142 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))
84 cnpnei.2 . . . . . . . . 9 𝑌 = 𝐾
8528, 84iscnp2 22590 . . . . . . . 8 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8685baib 536 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
87863expa 1118 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
88873adantl3 1168 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
8988adantr 481 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑜𝐾 ((𝐹𝐴) ∈ 𝑜 → ∃𝑔𝐽 (𝐴𝑔 ∧ (𝐹𝑔) ⊆ 𝑜)))))
9050, 83, 89mpbir2and 711 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
9190ex 413 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴}) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
9249, 91impbid 211 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹𝐴)})(𝐹𝑦) ∈ ((nei‘𝐽)‘{𝐴})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  wss 3910  {csn 4586   cuni 4865  ccnv 5632  dom cdm 5633  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  Topctop 22242  neicnei 22448   CnP ccnp 22576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-top 22243  df-topon 22260  df-nei 22449  df-cnp 22579
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator