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

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

Proof of Theorem isfcf
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fcfval 21884 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿)))
21eleq2d 2716 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ 𝐴 ∈ (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿))))
3 simp1 1081 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝐽 ∈ (TopOn‘𝑋))
4 toponmax 20778 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
5 filfbas 21699 . . . 4 (𝐿 ∈ (Fil‘𝑌) → 𝐿 ∈ (fBas‘𝑌))
6 id 22 . . . 4 (𝐹:𝑌𝑋𝐹:𝑌𝑋)
7 fmfil 21795 . . . 4 ((𝑋𝐽𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋))
84, 5, 6, 7syl3an 1408 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋))
9 fclsopn 21865 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿)) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅))))
103, 8, 9syl2anc 694 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿)) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅))))
11 simpll1 1120 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝐽 ∈ (TopOn‘𝑋))
1211, 4syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝑋𝐽)
13 simpll2 1121 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝐿 ∈ (Fil‘𝑌))
1413, 5syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝐿 ∈ (fBas‘𝑌))
15 simpll3 1122 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝐹:𝑌𝑋)
16 simpl2 1085 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → 𝐿 ∈ (Fil‘𝑌))
17 fgfil 21726 . . . . . . . . . . . 12 (𝐿 ∈ (Fil‘𝑌) → (𝑌filGen𝐿) = 𝐿)
1816, 17syl 17 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (𝑌filGen𝐿) = 𝐿)
1918eleq2d 2716 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (𝑠 ∈ (𝑌filGen𝐿) ↔ 𝑠𝐿))
2019biimpar 501 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → 𝑠 ∈ (𝑌filGen𝐿))
21 eqid 2651 . . . . . . . . . 10 (𝑌filGen𝐿) = (𝑌filGen𝐿)
2221imaelfm 21802 . . . . . . . . 9 (((𝑋𝐽𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐿)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐿))
2312, 14, 15, 20, 22syl31anc 1369 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐿))
24 ineq2 3841 . . . . . . . . . 10 (𝑥 = (𝐹𝑠) → (𝑜𝑥) = (𝑜 ∩ (𝐹𝑠)))
2524neeq1d 2882 . . . . . . . . 9 (𝑥 = (𝐹𝑠) → ((𝑜𝑥) ≠ ∅ ↔ (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
2625rspcv 3336 . . . . . . . 8 ((𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐿) → (∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅ → (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
2723, 26syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑠𝐿) → (∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅ → (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
2827ralrimdva 2998 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅ → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
29 elfm 21798 . . . . . . . . . . 11 ((𝑋𝐽𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ (𝑥𝑋 ∧ ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥)))
304, 5, 6, 29syl3an 1408 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ (𝑥𝑋 ∧ ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥)))
3130adantr 480 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ (𝑥𝑋 ∧ ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥)))
3231simplbda 653 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥)
33 r19.29r 3102 . . . . . . . . . 10 ((∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥 ∧ ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → ∃𝑠𝐿 ((𝐹𝑠) ⊆ 𝑥 ∧ (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
34 sslin 3872 . . . . . . . . . . . 12 ((𝐹𝑠) ⊆ 𝑥 → (𝑜 ∩ (𝐹𝑠)) ⊆ (𝑜𝑥))
35 ssn0 4009 . . . . . . . . . . . 12 (((𝑜 ∩ (𝐹𝑠)) ⊆ (𝑜𝑥) ∧ (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝑜𝑥) ≠ ∅)
3634, 35sylan 487 . . . . . . . . . . 11 (((𝐹𝑠) ⊆ 𝑥 ∧ (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝑜𝑥) ≠ ∅)
3736rexlimivw 3058 . . . . . . . . . 10 (∃𝑠𝐿 ((𝐹𝑠) ⊆ 𝑥 ∧ (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝑜𝑥) ≠ ∅)
3833, 37syl 17 . . . . . . . . 9 ((∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥 ∧ ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅) → (𝑜𝑥) ≠ ∅)
3938ex 449 . . . . . . . 8 (∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑥 → (∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅ → (𝑜𝑥) ≠ ∅))
4032, 39syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) ∧ 𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)) → (∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅ → (𝑜𝑥) ≠ ∅))
4140ralrimdva 2998 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅ → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅))
4228, 41impbid 202 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → (∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅ ↔ ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))
4342imbi2d 329 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑜𝐽) → ((𝐴𝑜 → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅) ↔ (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)))
4443ralbidva 3014 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (∀𝑜𝐽 (𝐴𝑜 → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅) ↔ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅)))
4544anbi2d 740 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑥 ∈ ((𝑋 FilMap 𝐹)‘𝐿)(𝑜𝑥) ≠ ∅)) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))))
462, 10, 453bitrd 294 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜 → ∀𝑠𝐿 (𝑜 ∩ (𝐹𝑠)) ≠ ∅))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948   “ cima 5146  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  fBascfbas 19782  filGencfg 19783  TopOnctopon 20763  Filcfil 21696   FilMap cfm 21784   fClus cfcls 21787   fClusf cfcf 21788 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-nel 2927  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-int 4508  df-iun 4554  df-iin 4555  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-map 7901  df-fbas 19791  df-fg 19792  df-top 20747  df-topon 20764  df-cld 20871  df-ntr 20872  df-cls 20873  df-fil 21697  df-fm 21789  df-fcls 21792  df-fcf 21793 This theorem is referenced by:  fcfnei  21886
 Copyright terms: Public domain W3C validator