Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lly1stc Structured version   Unicode version

Theorem lly1stc 20453
 Description: First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
lly1stc Locally

Proof of Theorem lly1stc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 llytop 20429 . . . 4 Locally
2 simprr 764 . . . . . . . . 9 Locally t t
3 simprl 762 . . . . . . . . . 10 Locally t
41ad3antrrr 734 . . . . . . . . . . 11 Locally t
5 elssuni 4191 . . . . . . . . . . . 12
65ad2antlr 731 . . . . . . . . . . 11 Locally t
7 eqid 2428 . . . . . . . . . . . 12
87restuni 20120 . . . . . . . . . . 11 t
94, 6, 8syl2anc 665 . . . . . . . . . 10 Locally t t
103, 9eleqtrd 2508 . . . . . . . . 9 Locally t t
11 eqid 2428 . . . . . . . . . 10 t t
12111stcclb 20401 . . . . . . . . 9 t t t t
132, 10, 12syl2anc 665 . . . . . . . 8 Locally t t t
14 elpwi 3933 . . . . . . . . . . . . . . . . . 18 t t
1514adantl 467 . . . . . . . . . . . . . . . . 17 Locally t t t
1615sselda 3407 . . . . . . . . . . . . . . . 16 Locally t t t
174adantr 466 . . . . . . . . . . . . . . . . . 18 Locally t t
18 simpllr 767 . . . . . . . . . . . . . . . . . 18 Locally t t
19 restopn2 20135 . . . . . . . . . . . . . . . . . 18 t
2017, 18, 19syl2anc 665 . . . . . . . . . . . . . . . . 17 Locally t t t
2120simplbda 628 . . . . . . . . . . . . . . . 16 Locally t t t
2216, 21syldan 472 . . . . . . . . . . . . . . 15 Locally t t
23 df-ss 3393 . . . . . . . . . . . . . . 15
2422, 23sylib 199 . . . . . . . . . . . . . 14 Locally t t
2520simprbda 627 . . . . . . . . . . . . . . 15 Locally t t t
2616, 25syldan 472 . . . . . . . . . . . . . 14 Locally t t
2724, 26eqeltrd 2506 . . . . . . . . . . . . 13 Locally t t
28 ineq1 3600 . . . . . . . . . . . . . 14
2928cbvmptv 4459 . . . . . . . . . . . . 13
3027, 29fmptd 6005 . . . . . . . . . . . 12 Locally t t
31 frn 5695 . . . . . . . . . . . 12
3230, 31syl 17 . . . . . . . . . . 11 Locally t t
3332adantrr 721 . . . . . . . . . 10 Locally t t t
34 vex 3025 . . . . . . . . . . 11
3534elpw2 4531 . . . . . . . . . 10
3633, 35sylibr 215 . . . . . . . . 9 Locally t t t
37 simprrl 772 . . . . . . . . . 10 Locally t t t
38 1stcrestlem 20409 . . . . . . . . . 10
3937, 38syl 17 . . . . . . . . 9 Locally t t t
404ad2antrr 730 . . . . . . . . . . . . . 14 Locally t t t
41 simpllr 767 . . . . . . . . . . . . . . 15 Locally t t t
4241adantr 466 . . . . . . . . . . . . . 14 Locally t t t
43 simprl 762 . . . . . . . . . . . . . 14 Locally t t t
44 elrestr 15270 . . . . . . . . . . . . . 14 t
4540, 42, 43, 44syl3anc 1264 . . . . . . . . . . . . 13 Locally t t t t
46 simprrr 773 . . . . . . . . . . . . . 14 Locally t t t t
4746adantr 466 . . . . . . . . . . . . 13 Locally t t t t
48 simprr 764 . . . . . . . . . . . . . 14 Locally t t t
493ad2antrr 730 . . . . . . . . . . . . . 14 Locally t t t
5048, 49elind 3593 . . . . . . . . . . . . 13 Locally t t t
51 eleq2 2495 . . . . . . . . . . . . . . 15
52 sseq2 3429 . . . . . . . . . . . . . . . . 17
5352anbi2d 708 . . . . . . . . . . . . . . . 16
5453rexbidv 2878 . . . . . . . . . . . . . . 15
5551, 54imbi12d 321 . . . . . . . . . . . . . 14
5655rspcv 3121 . . . . . . . . . . . . 13 t t
5745, 47, 50, 56syl3c 63 . . . . . . . . . . . 12 Locally t t t
583ad2antrr 730 . . . . . . . . . . . . . . . . . 18 Locally t t
59 elin 3592 . . . . . . . . . . . . . . . . . . 19
6059simplbi2com 631 . . . . . . . . . . . . . . . . . 18
6158, 60syl 17 . . . . . . . . . . . . . . . . 17 Locally t t
6222biantrud 509 . . . . . . . . . . . . . . . . . . 19 Locally t t
63 ssin 3627 . . . . . . . . . . . . . . . . . . 19
6462, 63syl6bb 264 . . . . . . . . . . . . . . . . . 18 Locally t t
65 ssinss1 3633 . . . . . . . . . . . . . . . . . 18
6664, 65syl6bir 232 . . . . . . . . . . . . . . . . 17 Locally t t
6761, 66anim12d 565 . . . . . . . . . . . . . . . 16 Locally t t
6867reximdva 2839 . . . . . . . . . . . . . . 15 Locally t t
69 vex 3025 . . . . . . . . . . . . . . . . . 18
7069inex1 4508 . . . . . . . . . . . . . . . . 17
7170rgenw 2726 . . . . . . . . . . . . . . . 16
72 eleq2 2495 . . . . . . . . . . . . . . . . . 18
73 sseq1 3428 . . . . . . . . . . . . . . . . . 18
7472, 73anbi12d 715 . . . . . . . . . . . . . . . . 17
7529, 74rexrnmpt 5991 . . . . . . . . . . . . . . . 16
7671, 75ax-mp 5 . . . . . . . . . . . . . . 15
7768, 76syl6ibr 230 . . . . . . . . . . . . . 14 Locally t t
7877adantrr 721 . . . . . . . . . . . . 13 Locally t t t
7978adantr 466 . . . . . . . . . . . 12 Locally t t t
8057, 79mpd 15 . . . . . . . . . . 11 Locally t t t
8180expr 618 . . . . . . . . . 10 Locally t t t
8281ralrimiva 2779 . . . . . . . . 9 Locally t t t
83 breq1 4369 . . . . . . . . . . 11
84 rexeq 2965 . . . . . . . . . . . . 13
8584imbi2d 317 . . . . . . . . . . . 12
8685ralbidv 2804 . . . . . . . . . . 11
8783, 86anbi12d 715 . . . . . . . . . 10
8887rspcev 3125 . . . . . . . . 9
8936, 39, 82, 88syl12anc 1262 . . . . . . . 8 Locally t t t
9013, 89rexlimddv 2860 . . . . . . 7 Locally t
91903adantr1 1164 . . . . . 6 Locally t
92 simpl 458 . . . . . . 7 Locally Locally
931adantr 466 . . . . . . . 8 Locally
947topopn 19878 . . . . . . . 8
9593, 94syl 17 . . . . . . 7 Locally
96 simpr 462 . . . . . . 7 Locally
97 llyi 20431 . . . . . . 7 Locally t
9892, 95, 96, 97syl3anc 1264 . . . . . 6 Locally t
9991, 98r19.29a 2909 . . . . 5 Locally
10099ralrimiva 2779 . . . 4 Locally
1017is1stc2 20399 . . . 4
1021, 100, 101sylanbrc 668 . . 3 Locally
103102ssriv 3411 . 2 Locally
104 1stcrest 20410 . . . . 5 t
105104adantl 467 . . . 4 t
106 1stctop 20400 . . . . . 6
107106ssriv 3411 . . . . 5
108107a1i 11 . . . 4
109105, 108restlly 20440 . . 3 Locally
110109trud 1446 . 2 Locally
111103, 110eqssi 3423 1 Locally
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wtru 1438   wcel 1872  wral 2714  wrex 2715  cvv 3022   cin 3378   wss 3379  cpw 3924  cuni 4162   class class class wbr 4366   cmpt 4425   crn 4797  wf 5540  (class class class)co 6249  com 6650   cdom 7522   ↾t crest 15262  ctop 19859  c1stc 20394  Locally clly 20421 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-isom 5553  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-oadd 7141  df-er 7318  df-map 7429  df-en 7525  df-dom 7526  df-fin 7528  df-fi 7878  df-card 8325  df-acn 8328  df-rest 15264  df-topgen 15285  df-top 19863  df-bases 19864  df-topon 19865  df-1stc 20396  df-lly 20423 This theorem is referenced by:  dis1stc  20456
 Copyright terms: Public domain W3C validator