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

Theorem filuni 17870
 Description: The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
filuni
Distinct variable groups:   ,,   ,,

Proof of Theorem filuni
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni2 3979 . . . 4
2 ssel2 3303 . . . . . . 7
3 filelss 17837 . . . . . . . 8
43ex 424 . . . . . . 7
52, 4syl 16 . . . . . 6
65rexlimdva 2790 . . . . 5
763ad2ant1 978 . . . 4
81, 7syl5bi 209 . . 3
98pm4.71rd 617 . 2
10 ssn0 3620 . . . 4
11 fvprc 5681 . . . . 5
1211necon1ai 2609 . . . 4
1310, 12syl 16 . . 3
15 filtop 17840 . . . . . . . . 9
162, 15syl 16 . . . . . . . 8
1716a1d 23 . . . . . . 7
1817ralimdva 2744 . . . . . 6
19 r19.2z 3677 . . . . . . 7
2019ex 424 . . . . . 6
2118, 20sylan9 639 . . . . 5
22213impia 1150 . . . 4
23 eluni2 3979 . . . 4
2422, 23sylibr 204 . . 3
25 sbcel1gv 3180 . . . 4
2614, 25syl 16 . . 3
2724, 26mpbird 224 . 2
28 0nelfil 17834 . . . . . 6
292, 28syl 16 . . . . 5
3029ralrimiva 2749 . . . 4
32 0ex 4299 . . . . . . 7
33 sbcel1gv 3180 . . . . . . 7
3432, 33ax-mp 8 . . . . . 6
35 eluni2 3979 . . . . . 6
3634, 35bitri 241 . . . . 5
3736notbii 288 . . . 4
38 ralnex 2676 . . . 4
3937, 38bitr4i 244 . . 3
4031, 39sylibr 204 . 2
41 simp13 989 . . . . 5
42 r19.29 2806 . . . . . 6
4342ex 424 . . . . 5
4441, 43syl 16 . . . 4
45 simp1 957 . . . . 5
46 simp1 957 . . . . . . . . 9
47 simpl 444 . . . . . . . . 9
4846, 47, 2syl2an 464 . . . . . . . 8
49 simprrr 742 . . . . . . . 8
50 simpl2 961 . . . . . . . 8
51 simpl3 962 . . . . . . . 8
52 filss 17838 . . . . . . . 8
5348, 49, 50, 51, 52syl13anc 1186 . . . . . . 7
5453expr 599 . . . . . 6
5554reximdva 2778 . . . . 5
5645, 55syl3an1 1217 . . . 4
5744, 56syld 42 . . 3
58 sbcid 3137 . . . 4
5958, 1bitri 241 . . 3
60 vex 2919 . . . . 5
61 sbcel1gv 3180 . . . . 5
6260, 61ax-mp 8 . . . 4
63 eluni2 3979 . . . 4
6462, 63bitri 241 . . 3
6557, 59, 643imtr4g 262 . 2
66 simp13 989 . . . . 5
67 r19.29 2806 . . . . . 6
6867ex 424 . . . . 5
6966, 68syl 16 . . . 4
70 simp11 987 . . . . 5
71 r19.29 2806 . . . . . . . . . . 11
7271ex 424 . . . . . . . . . 10
73 elun1 3474 . . . . . . . . . . . . . . . 16
74 elun2 3475 . . . . . . . . . . . . . . . 16
7573, 74anim12i 550 . . . . . . . . . . . . . . 15
76 eleq2 2465 . . . . . . . . . . . . . . . . 17
77 eleq2 2465 . . . . . . . . . . . . . . . . 17
7876, 77anbi12d 692 . . . . . . . . . . . . . . . 16
7978rspcev 3012 . . . . . . . . . . . . . . 15
8075, 79sylan2 461 . . . . . . . . . . . . . 14
8180an12s 777 . . . . . . . . . . . . 13
8281ex 424 . . . . . . . . . . . 12
8382ad2antlr 708 . . . . . . . . . . 11
8483rexlimdva 2790 . . . . . . . . . 10
8572, 84syl9r 69 . . . . . . . . 9
8685impr 603 . . . . . . . 8
8786ancom2s 778 . . . . . . 7
8887rexlimiva 2785 . . . . . 6
8988imp 419 . . . . 5
90 ssel2 3303 . . . . . . 7
91 filin 17839 . . . . . . . 8
92913expib 1156 . . . . . . 7
9390, 92syl 16 . . . . . 6
9493reximdva 2778 . . . . 5
9570, 89, 94syl2im 36 . . . 4
9669, 95syland 468 . . 3
97 eluni2 3979 . . . . 5
9858, 97bitri 241 . . . 4
9964, 98anbi12i 679 . . 3
10060inex1 4304 . . . . 5
101 sbcel1gv 3180 . . . . 5
102100, 101ax-mp 8 . . . 4
103 eluni2 3979 . . . 4
104102, 103bitri 241 . . 3
10596, 99, 1043imtr4g 262 . 2
1069, 14, 27, 40, 65, 105isfild 17843 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  cvv 2916  wsbc 3121   cun 3278   cin 3279   wss 3280  c0 3588  cuni 3975  cfv 5413  cfil 17830 This theorem is referenced by:  filssufilg  17896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fv 5421  df-fbas 16654  df-fil 17831
 Copyright terms: Public domain W3C validator