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

Theorem fcfnei 24026
Description: The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
Assertion
Ref Expression
fcfnei ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅)))
Distinct variable groups:   𝐴,𝑛   𝑛,𝑠,𝐽   𝑛,𝐿,𝑠   𝑛,𝐹,𝑠   𝑛,𝑋,𝑠   𝑛,𝑌,𝑠
Allowed substitution hint:   𝐴(𝑠)

Proof of Theorem fcfnei
Dummy variable 𝑜 is distinct from all other variables.
StepHypRef Expression
1 isfcf 24025 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))))
2 simpll1 1209 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝐽 ∈ (TopOn‘𝑋))
3 topontop 22902 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
42, 3syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝐽 ∈ Top)
5 simpr 483 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 ∈ ((nei‘𝐽)‘{𝐴}))
6 eqid 2726 . . . . . . . . 9 𝐽 = 𝐽
76neii1 23097 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 𝐽)
84, 5, 7syl2anc 582 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 𝐽)
96ntrss2 23048 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑛 𝐽) → ((int‘𝐽)‘𝑛) ⊆ 𝑛)
104, 8, 9syl2anc 582 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → ((int‘𝐽)‘𝑛) ⊆ 𝑛)
11 simplr 767 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝐴𝑋)
12 toponuni 22903 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
132, 12syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑋 = 𝐽)
1411, 13eleqtrd 2828 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝐴 𝐽)
1514snssd 4810 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → {𝐴} ⊆ 𝐽)
166neiint 23095 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ {𝐴} ⊆ 𝐽𝑛 𝐽) → (𝑛 ∈ ((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑛)))
174, 15, 8, 16syl3anc 1368 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑛 ∈ ((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑛)))
185, 17mpbid 231 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → {𝐴} ⊆ ((int‘𝐽)‘𝑛))
19 snssg 4784 . . . . . . . . 9 (𝐴𝑋 → (𝐴 ∈ ((int‘𝐽)‘𝑛) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑛)))
2011, 19syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (𝐴 ∈ ((int‘𝐽)‘𝑛) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑛)))
2118, 20mpbird 256 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝐴 ∈ ((int‘𝐽)‘𝑛))
226ntropn 23040 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑛 𝐽) → ((int‘𝐽)‘𝑛) ∈ 𝐽)
234, 8, 22syl2anc 582 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → ((int‘𝐽)‘𝑛) ∈ 𝐽)
24 eleq2 2815 . . . . . . . . . 10 (𝑜 = ((int‘𝐽)‘𝑛) → (𝐴𝑜𝐴 ∈ ((int‘𝐽)‘𝑛)))
25 ineq1 4205 . . . . . . . . . . . 12 (𝑜 = ((int‘𝐽)‘𝑛) → (𝑜 ∩ (𝐹𝑠)) = (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)))
2625neeq1d 2990 . . . . . . . . . . 11 (𝑜 = ((int‘𝐽)‘𝑛) → ((𝑜 ∩ (𝐹𝑠)) ≠ ∅ ↔ (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅))
2726ralbidv 3168 . . . . . . . . . 10 (𝑜 = ((int‘𝐽)‘𝑛) → (∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅ ↔ ∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅))
2824, 27imbi12d 343 . . . . . . . . 9 (𝑜 = ((int‘𝐽)‘𝑛) → ((𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) ↔ (𝐴 ∈ ((int‘𝐽)‘𝑛) → ∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅)))
2928rspcv 3605 . . . . . . . 8 (((int‘𝐽)‘𝑛) ∈ 𝐽 → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝐴 ∈ ((int‘𝐽)‘𝑛) → ∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅)))
3023, 29syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝐴 ∈ ((int‘𝐽)‘𝑛) → ∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅)))
3121, 30mpid 44 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → ∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅))
32 ssrin 4234 . . . . . . . 8 (((int‘𝐽)‘𝑛) ⊆ 𝑛 → (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ⊆ (𝑛 ∩ (𝐹𝑠)))
33 ssn0 4400 . . . . . . . . 9 (((((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ⊆ (𝑛 ∩ (𝐹𝑠)) ∧ (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅) → (𝑛 ∩ (𝐹𝑠)) ≠ ∅)
3433ex 411 . . . . . . . 8 ((((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ⊆ (𝑛 ∩ (𝐹𝑠)) → ((((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅ → (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
3532, 34syl 17 . . . . . . 7 (((int‘𝐽)‘𝑛) ⊆ 𝑛 → ((((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅ → (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
3635ralimdv 3159 . . . . . 6 (((int‘𝐽)‘𝑛) ⊆ 𝑛 → (∀𝑠𝐿 (((int‘𝐽)‘𝑛) ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
3710, 31, 36sylsyld 61 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → ∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
3837ralrimdva 3144 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
39 simpl1 1188 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
4039, 3syl 17 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ Top)
41 opnneip 23110 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑜𝐽𝐴𝑜) → 𝑜 ∈ ((nei‘𝐽)‘{𝐴}))
42413expb 1117 . . . . . . . . 9 ((𝐽 ∈ Top ∧ (𝑜𝐽𝐴𝑜)) → 𝑜 ∈ ((nei‘𝐽)‘{𝐴}))
4340, 42sylan 578 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ (𝑜𝐽𝐴𝑜)) → 𝑜 ∈ ((nei‘𝐽)‘{𝐴}))
44 ineq1 4205 . . . . . . . . . . 11 (𝑛 = 𝑜 → (𝑛 ∩ (𝐹𝑠)) = (𝑜 ∩ (𝐹𝑠)))
4544neeq1d 2990 . . . . . . . . . 10 (𝑛 = 𝑜 → ((𝑛 ∩ (𝐹𝑠)) ≠ ∅ ↔ (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
4645ralbidv 3168 . . . . . . . . 9 (𝑛 = 𝑜 → (∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ ↔ ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
4746rspcv 3605 . . . . . . . 8 (𝑜 ∈ ((nei‘𝐽)‘{𝐴}) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
4843, 47syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ (𝑜𝐽𝐴𝑜)) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
4948expr 455 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → (𝐴𝑜 → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)))
5049com23 86 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) ∧ 𝑜𝐽) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ → (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)))
5150ralrimdva 3144 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)))
5238, 51impbid 211 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅))
5352pm5.32da 577 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)) ↔ (𝐴𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅)))
541, 53bitrd 278 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠𝐿 (𝑛 ∩ (𝐹𝑠)) ≠ ∅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  cin 3947  wss 3948  c0 4324  {csn 4625   cuni 4907  cima 5677  wf 6541  cfv 6545  (class class class)co 7415  Topctop 22882  TopOnctopon 22899  intcnt 23008  neicnei 23088  Filcfil 23836   fClusf cfcf 23928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4908  df-int 4949  df-iun 4997  df-iin 4998  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-ov 7418  df-oprab 7419  df-mpo 7420  df-map 8848  df-fbas 21335  df-fg 21336  df-top 22883  df-topon 22900  df-cld 23010  df-ntr 23011  df-cls 23012  df-nei 23089  df-fil 23837  df-fm 23929  df-fcls 23932  df-fcf 23933
This theorem is referenced by:  fcfneii  24028
  Copyright terms: Public domain W3C validator