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

Theorem flftg 23810
Description: Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypothesis
Ref Expression
flftg.l 𝐽 = (topGen‘𝐵)
Assertion
Ref Expression
flftg ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))))
Distinct variable groups:   𝑜,𝑠,𝐴   𝐵,𝑜   𝑜,𝐹,𝑠   𝐽,𝑠   𝑜,𝐿,𝑠   𝑋,𝑠   𝑌,𝑠
Allowed substitution hints:   𝐵(𝑠)   𝐽(𝑜)   𝑋(𝑜)   𝑌(𝑜)

Proof of Theorem flftg
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 isflf 23807 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))))
2 flftg.l . . . . 5 𝐽 = (topGen‘𝐵)
32raleqi 3315 . . . 4 (∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
4 simpl1 1188 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
5 topontop 22725 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
64, 5syl 17 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ Top)
72, 6eqeltrrid 2830 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (topGen‘𝐵) ∈ Top)
8 tgclb 22783 . . . . . . 7 (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top)
97, 8sylibr 233 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐵 ∈ TopBases)
10 bastg 22779 . . . . . 6 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
11 eleq2w 2809 . . . . . . . . 9 (𝑢 = 𝑜 → (𝐴𝑢𝐴𝑜))
12 sseq2 4000 . . . . . . . . . 10 (𝑢 = 𝑜 → ((𝐹𝑠) ⊆ 𝑢 ↔ (𝐹𝑠) ⊆ 𝑜))
1312rexbidv 3170 . . . . . . . . 9 (𝑢 = 𝑜 → (∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢 ↔ ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))
1411, 13imbi12d 344 . . . . . . . 8 (𝑢 = 𝑜 → ((𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
1514cbvralvw 3226 . . . . . . 7 (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜 ∈ (topGen‘𝐵)(𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))
16 ssralv 4042 . . . . . . 7 (𝐵 ⊆ (topGen‘𝐵) → (∀𝑜 ∈ (topGen‘𝐵)(𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
1715, 16biimtrid 241 . . . . . 6 (𝐵 ⊆ (topGen‘𝐵) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
189, 10, 173syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
19 tg2 22778 . . . . . . . 8 ((𝑢 ∈ (topGen‘𝐵) ∧ 𝐴𝑢) → ∃𝑜𝐵 (𝐴𝑜𝑜𝑢))
20 r19.29 3106 . . . . . . . . . 10 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ ∃𝑜𝐵 (𝐴𝑜𝑜𝑢)) → ∃𝑜𝐵 ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)))
21 simpl 482 . . . . . . . . . . . . 13 ((𝐴𝑜𝑜𝑢) → 𝐴𝑜)
22 simpr 484 . . . . . . . . . . . . . . 15 ((𝐴𝑜𝑜𝑢) → 𝑜𝑢)
23 sstr2 3981 . . . . . . . . . . . . . . 15 ((𝐹𝑠) ⊆ 𝑜 → (𝑜𝑢 → (𝐹𝑠) ⊆ 𝑢))
2422, 23syl5com 31 . . . . . . . . . . . . . 14 ((𝐴𝑜𝑜𝑢) → ((𝐹𝑠) ⊆ 𝑜 → (𝐹𝑠) ⊆ 𝑢))
2524reximdv 3162 . . . . . . . . . . . . 13 ((𝐴𝑜𝑜𝑢) → (∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
2621, 25embantd 59 . . . . . . . . . . . 12 ((𝐴𝑜𝑜𝑢) → ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
2726impcom 407 . . . . . . . . . . 11 (((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
2827rexlimivw 3143 . . . . . . . . . 10 (∃𝑜𝐵 ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
2920, 28syl 17 . . . . . . . . 9 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ ∃𝑜𝐵 (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
3029ex 412 . . . . . . . 8 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → (∃𝑜𝐵 (𝐴𝑜𝑜𝑢) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3119, 30syl5 34 . . . . . . 7 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝐴𝑢) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3231expdimp 452 . . . . . 6 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3332ralrimiva 3138 . . . . 5 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3418, 33impbid1 224 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
353, 34bitrid 283 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
3635pm5.32da 578 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝐴𝑋 ∧ ∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)) ↔ (𝐴𝑋 ∧ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))))
371, 36bitrd 279 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  wrex 3062  wss 3940  cima 5669  wf 6529  cfv 6533  (class class class)co 7401  topGenctg 17379  Topctop 22705  TopOnctopon 22722  TopBasesctb 22758  Filcfil 23659   fLimf cflf 23749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-map 8817  df-topgen 17385  df-fbas 21220  df-fg 21221  df-top 22706  df-topon 22723  df-bases 22759  df-ntr 22834  df-nei 22912  df-fil 23660  df-fm 23752  df-flim 23753  df-flf 23754
This theorem is referenced by:  txflf  23820
  Copyright terms: Public domain W3C validator