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

Theorem csdfil 20987
 Description: The set of all elements whose complement is dominated by the base set is a filter. (Contributed by Mario Carneiro, 14-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
csdfil
Distinct variable group:   ,

Proof of Theorem csdfil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difeq2 3534 . . . . . 6
21breq1d 4405 . . . . 5
32elrab 3184 . . . 4
4 selpw 3949 . . . . 5
54anbi1i 709 . . . 4
63, 5bitri 257 . . 3
76a1i 11 . 2
8 elex 3040 . . 3
10 difid 3747 . . . 4
11 infn0 7851 . . . . . 6
1211adantl 473 . . . . 5
13 0sdomg 7719 . . . . . 6
1413adantr 472 . . . . 5
1512, 14mpbird 240 . . . 4
1610, 15syl5eqbr 4429 . . 3
17 difeq2 3534 . . . . . 6
1817breq1d 4405 . . . . 5
1918sbcieg 3288 . . . 4
2116, 20mpbird 240 . 2
22 sdomirr 7727 . . 3
23 0ex 4528 . . . . 5
24 difeq2 3534 . . . . . . 7
25 dif0 3749 . . . . . . 7
2624, 25syl6eq 2521 . . . . . 6
2726breq1d 4405 . . . . 5
2823, 27sbcie 3290 . . . 4
2928a1i 11 . . 3
3022, 29mtbiri 310 . 2
31 simp1l 1054 . . . . . 6
32 difexg 4545 . . . . . 6
3331, 32syl 17 . . . . 5
34 sscon 3556 . . . . . 6
35343ad2ant3 1053 . . . . 5
36 ssdomg 7633 . . . . 5
3733, 35, 36sylc 61 . . . 4
38 domsdomtr 7725 . . . . 5
3938ex 441 . . . 4
4037, 39syl 17 . . 3
41 vex 3034 . . . 4
42 difeq2 3534 . . . . 5
4342breq1d 4405 . . . 4
4441, 43sbcie 3290 . . 3
45 vex 3034 . . . 4
46 difeq2 3534 . . . . 5
4746breq1d 4405 . . . 4
4845, 47sbcie 3290 . . 3
4940, 44, 483imtr4g 278 . 2
50 infunsdom 8662 . . . . . 6
5150ex 441 . . . . 5
52 difindi 3688 . . . . . 6
5352breq1i 4402 . . . . 5
5451, 53syl6ibr 235 . . . 4