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

Theorem flftg 21610
 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 21607 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))))
2 flftg.l . . . . 5 𝐽 = (topGen‘𝐵)
32raleqi 3119 . . . 4 (∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
4 simpl1 1057 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
5 topontop 20541 . . . . . . . . 9 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
64, 5syl 17 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐽 ∈ Top)
72, 6syl5eqelr 2693 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (topGen‘𝐵) ∈ Top)
8 tgclb 20585 . . . . . . 7 (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top)
97, 8sylibr 223 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → 𝐵 ∈ TopBases)
10 bastg 20581 . . . . . 6 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
11 eleq2 2677 . . . . . . . . 9 (𝑢 = 𝑜 → (𝐴𝑢𝐴𝑜))
12 sseq2 3590 . . . . . . . . . 10 (𝑢 = 𝑜 → ((𝐹𝑠) ⊆ 𝑢 ↔ (𝐹𝑠) ⊆ 𝑜))
1312rexbidv 3034 . . . . . . . . 9 (𝑢 = 𝑜 → (∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢 ↔ ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))
1411, 13imbi12d 333 . . . . . . . 8 (𝑢 = 𝑜 → ((𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
1514cbvralv 3147 . . . . . . 7 (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜 ∈ (topGen‘𝐵)(𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))
16 ssralv 3629 . . . . . . 7 (𝐵 ⊆ (topGen‘𝐵) → (∀𝑜 ∈ (topGen‘𝐵)(𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
1715, 16syl5bi 231 . . . . . 6 (𝐵 ⊆ (topGen‘𝐵) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
189, 10, 173syl 18 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) → ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
19 tg2 20580 . . . . . . . 8 ((𝑢 ∈ (topGen‘𝐵) ∧ 𝐴𝑢) → ∃𝑜𝐵 (𝐴𝑜𝑜𝑢))
20 r19.29 3054 . . . . . . . . . 10 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ ∃𝑜𝐵 (𝐴𝑜𝑜𝑢)) → ∃𝑜𝐵 ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)))
21 simpl 472 . . . . . . . . . . . . 13 ((𝐴𝑜𝑜𝑢) → 𝐴𝑜)
22 simpr 476 . . . . . . . . . . . . . . 15 ((𝐴𝑜𝑜𝑢) → 𝑜𝑢)
23 sstr2 3575 . . . . . . . . . . . . . . 15 ((𝐹𝑠) ⊆ 𝑜 → (𝑜𝑢 → (𝐹𝑠) ⊆ 𝑢))
2422, 23syl5com 31 . . . . . . . . . . . . . 14 ((𝐴𝑜𝑜𝑢) → ((𝐹𝑠) ⊆ 𝑜 → (𝐹𝑠) ⊆ 𝑢))
2524reximdv 2999 . . . . . . . . . . . . 13 ((𝐴𝑜𝑜𝑢) → (∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
2621, 25embantd 57 . . . . . . . . . . . 12 ((𝐴𝑜𝑜𝑢) → ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
2726impcom 445 . . . . . . . . . . 11 (((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
2827rexlimivw 3011 . . . . . . . . . 10 (∃𝑜𝐵 ((𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
2920, 28syl 17 . . . . . . . . 9 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ ∃𝑜𝐵 (𝐴𝑜𝑜𝑢)) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)
3029ex 449 . . . . . . . 8 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → (∃𝑜𝐵 (𝐴𝑜𝑜𝑢) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3119, 30syl5 33 . . . . . . 7 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝐴𝑢) → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3231expdimp 452 . . . . . 6 ((∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3332ralrimiva 2949 . . . . 5 (∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜) → ∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢))
3418, 33impbid1 214 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢 ∈ (topGen‘𝐵)(𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
353, 34syl5bb 271 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝐴𝑋) → (∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢) ↔ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜)))
3635pm5.32da 671 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝐴𝑋 ∧ ∀𝑢𝐽 (𝐴𝑢 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑢)) ↔ (𝐴𝑋 ∧ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))))
371, 36bitrd 267 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐵 (𝐴𝑜 → ∃𝑠𝐿 (𝐹𝑠) ⊆ 𝑜))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540   “ cima 5041  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  topGenctg 15921  Topctop 20517  TopOnctopon 20518  TopBasesctb 20520  Filcfil 21459   fLimf cflf 21549 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-topgen 15927  df-fbas 19564  df-fg 19565  df-top 20521  df-bases 20522  df-topon 20523  df-ntr 20634  df-nei 20712  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554 This theorem is referenced by:  txflf  21620
 Copyright terms: Public domain W3C validator