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

Theorem tsmsfbas 21220
 Description: The collection of all sets of the form , which can be read as the set of all finite subsets of which contain as a subset, for each finite subset of , form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
tsmsfbas.s
tsmsfbas.f
tsmsfbas.l
tsmsfbas.a
Assertion
Ref Expression
tsmsfbas
Distinct variable groups:   ,   ,,
Allowed substitution hints:   (,)   ()   (,)   (,)   (,)

Proof of Theorem tsmsfbas
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsfbas.a . 2
2 elex 3040 . 2
3 tsmsfbas.l . . 3
4 ssrab2 3500 . . . . . . 7
5 tsmsfbas.s . . . . . . . . . 10
6 pwexg 4585 . . . . . . . . . . 11
7 inex1g 4539 . . . . . . . . . . 11
86, 7syl 17 . . . . . . . . . 10
95, 8syl5eqel 2553 . . . . . . . . 9
109adantr 472 . . . . . . . 8
11 elpw2g 4564 . . . . . . . 8
1210, 11syl 17 . . . . . . 7
134, 12mpbiri 241 . . . . . 6
14 tsmsfbas.f . . . . . 6
1513, 14fmptd 6061 . . . . 5
16 frn 5747 . . . . 5
1715, 16syl 17 . . . 4
18 0ss 3766 . . . . . . . . . 10
19 0fin 7817 . . . . . . . . . 10
20 elfpw 7894 . . . . . . . . . 10
2118, 19, 20mpbir2an 934 . . . . . . . . 9
2221, 5eleqtrri 2548 . . . . . . . 8
23 0ss 3766 . . . . . . . . 9
2423rgenw 2768 . . . . . . . 8
25 rabid2 2954 . . . . . . . . . 10
26 sseq1 3439 . . . . . . . . . . 11
2726ralbidv 2829 . . . . . . . . . 10
2825, 27syl5bb 265 . . . . . . . . 9
2928rspcev 3136 . . . . . . . 8
3022, 24, 29mp2an 686 . . . . . . 7
3114elrnmpt 5087 . . . . . . . 8
329, 31syl 17 . . . . . . 7
3330, 32mpbiri 241 . . . . . 6
34 ne0i 3728 . . . . . 6
3533, 34syl 17 . . . . 5
36 simpr 468 . . . . . . . . . . . 12
37 ssid 3437 . . . . . . . . . . . 12
38 sseq2 3440 . . . . . . . . . . . . 13
3938rspcev 3136 . . . . . . . . . . . 12
4036, 37, 39sylancl 675 . . . . . . . . . . 11
41 rabn0 3755 . . . . . . . . . . 11
4240, 41sylibr 217 . . . . . . . . . 10
4342necomd 2698 . . . . . . . . 9
4443neneqd 2648 . . . . . . . 8
4544nrexdv 2842 . . . . . . 7
46 0ex 4528 . . . . . . . 8
4714elrnmpt 5087 . . . . . . . 8
4846, 47ax-mp 5 . . . . . . 7
4945, 48sylnibr 312 . . . . . 6
50 df-nel 2644 . . . . . 6
5149, 50sylibr 217 . . . . 5
52 elfpw 7894 . . . . . . . . . . . . . . . . . 18
5352simplbi 467 . . . . . . . . . . . . . . . . 17
5453, 5eleq2s 2567 . . . . . . . . . . . . . . . 16
55 elfpw 7894 . . . . . . . . . . . . . . . . . 18
5655simplbi 467 . . . . . . . . . . . . . . . . 17
5756, 5eleq2s 2567 . . . . . . . . . . . . . . . 16
5854, 57anim12i 576 . . . . . . . . . . . . . . 15
59 unss 3599 . . . . . . . . . . . . . . 15
6058, 59sylib 201 . . . . . . . . . . . . . 14
6152simprbi 471 . . . . . . . . . . . . . . . 16
6261, 5eleq2s 2567 . . . . . . . . . . . . . . 15
6355simprbi 471 . . . . . . . . . . . . . . . 16
6463, 5eleq2s 2567 . . . . . . . . . . . . . . 15
65 unfi 7856 . . . . . . . . . . . . . . 15
6662, 64, 65syl2an 485 . . . . . . . . . . . . . 14
67 elfpw 7894 . . . . . . . . . . . . . 14
6860, 66, 67sylanbrc 677 . . . . . . . . . . . . 13
6968adantl 473 . . . . . . . . . . . 12
7069, 5syl6eleqr 2560 . . . . . . . . . . 11
71 eqidd 2472 . . . . . . . . . . 11
72 sseq1 3439 . . . . . . . . . . . . . 14
7372rabbidv 3022 . . . . . . . . . . . . 13
7473eqeq2d 2481 . . . . . . . . . . . 12
7574rspcev 3136 . . . . . . . . . . 11
7670, 71, 75syl2anc 673 . . . . . . . . . 10
779adantr 472 . . . . . . . . . . . 12
78 rabexg 4549 . . . . . . . . . . . 12
7977, 78syl 17 . . . . . . . . . . 11
80 sseq1 3439 . . . . . . . . . . . . . . 15
8180rabbidv 3022 . . . . . . . . . . . . . 14
8281cbvmptv 4488 . . . . . . . . . . . . 13
8314, 82eqtri 2493 . . . . . . . . . . . 12
8483elrnmpt 5087 . . . . . . . . . . 11
8579, 84syl 17 . . . . . . . . . 10
8676, 85mpbird 240 . . . . . . . . 9
87 pwidg 3955 . . . . . . . . . 10
8879, 87syl 17 . . . . . . . . 9
89 inelcm 3823 . . . . . . . . 9
9086, 88, 89syl2anc 673 . . . . . . . 8
9190ralrimivva 2814 . . . . . . 7
92 rabexg 4549 . . . . . . . . . 10
939, 92syl 17 . . . . . . . . 9
9493ralrimivw 2810 . . . . . . . 8
95 sseq1 3439 . . . . . . . . . . . 12
9695rabbidv 3022 . . . . . . . . . . 11
9796cbvmptv 4488 . . . . . . . . . 10
9814, 97eqtri 2493 . . . . . . . . 9
99 ineq1 3618 . . . . . . . . . . . . . 14
100 inrab 3706 . . . . . . . . . . . . . . 15
101 unss 3599 . . . . . . . . . . . . . . . . 17
102101a1i 11 . . . . . . . . . . . . . . . 16
103102rabbiia 3019 . . . . . . . . . . . . . . 15
104100, 103eqtri 2493 . . . . . . . . . . . . . 14
10599, 104syl6eq 2521 . . . . . . . . . . . . 13
106105pweqd 3947 . . . . . . . . . . . 12
107106ineq2d 3625 . . . . . . . . . . 11
108107neeq1d 2702 . . . . . . . . . 10
109108ralbidv 2829 . . . . . . . . 9
11098, 109ralrnmpt 6046 . . . . . . . 8
11194, 110syl 17 . . . . . . 7
11291, 111mpbird 240 . . . . . 6
113 rabexg 4549 . . . . . . . . . 10
1149, 113syl 17 . . . . . . . . 9
115114ralrimivw 2810 . . . . . . . 8
116 sseq1 3439 . . . . . . . . . . . 12
117116rabbidv 3022 . . . . . . . . . . 11
118117cbvmptv 4488 . . . . . . . . . 10
11914, 118eqtri 2493 . . . . . . . . 9
120 ineq2 3619 . . . . . . . . . . . 12
121120pweqd 3947 . . . . . . . . . . 11
122121ineq2d 3625 . . . . . . . . . 10
123122neeq1d 2702 . . . . . . . . 9
124119, 123ralrnmpt 6046 . . . . . . . 8
125115, 124syl 17 . . . . . . 7
126125ralbidv 2829 . . . . . 6
127112, 126mpbird 240 . . . . 5
12835, 51, 1273jca 1210 . . . 4
129 isfbas 20922 . . . . 5
1309, 129syl 17 . . . 4
13117, 128, 130mpbir2and 936 . . 3
1323, 131syl5eqel 2553 . 2
1331, 2, 1323syl 18 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641   wnel 2642  wral 2756  wrex 2757  crab 2760  cvv 3031   cun 3388   cin 3389   wss 3390  c0 3722  cpw 3942   cmpt 4454   crn 4840  wf 5585  cfv 5589  cfn 7587  cfbas 19035 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-oadd 7204  df-er 7381  df-en 7588  df-fin 7591  df-fbas 19044 This theorem is referenced by:  eltsms  21225  haustsms  21228  tsmscls  21230  tsmsmhm  21238  tsmsadd  21239
 Copyright terms: Public domain W3C validator