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

Theorem csdfil 17918
 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 3451 . . . . . 6
21breq1d 4214 . . . . 5
32elrab 3084 . . . 4
4 vex 2951 . . . . . 6
54elpw 3797 . . . . 5
65anbi1i 677 . . . 4
73, 6bitri 241 . . 3
87a1i 11 . 2
9 elex 2956 . . 3
11 difid 3688 . . . 4
12 infn0 7361 . . . . . 6
1312adantl 453 . . . . 5
14 0sdomg 7228 . . . . . 6
1514adantr 452 . . . . 5
1613, 15mpbird 224 . . . 4
1711, 16syl5eqbr 4237 . . 3
18 difeq2 3451 . . . . . 6
1918breq1d 4214 . . . . 5
2019sbcieg 3185 . . . 4
2217, 21mpbird 224 . 2
23 sdomirr 7236 . . 3
24 0ex 4331 . . . . 5
25 difeq2 3451 . . . . . . 7
26 dif0 3690 . . . . . . 7
2725, 26syl6eq 2483 . . . . . 6
2827breq1d 4214 . . . . 5
2924, 28sbcie 3187 . . . 4
3029a1i 11 . . 3
3123, 30mtbiri 295 . 2
32 simp1l 981 . . . . . 6
33 difexg 4343 . . . . . 6
3432, 33syl 16 . . . . 5
35 sscon 3473 . . . . . 6
36353ad2ant3 980 . . . . 5
37 ssdomg 7145 . . . . 5
3834, 36, 37sylc 58 . . . 4
39 domsdomtr 7234 . . . . 5
4039ex 424 . . . 4
4138, 40syl 16 . . 3
42 vex 2951 . . . 4
43 difeq2 3451 . . . . 5
4443breq1d 4214 . . . 4
4542, 44sbcie 3187 . . 3
46 vex 2951 . . . 4
47 difeq2 3451 . . . . 5
4847breq1d 4214 . . . 4
4946, 48sbcie 3187 . . 3
5041, 45, 493imtr4g 262 . 2
51 infunsdom 8086 . . . . . 6
5251ex 424 . . . . 5
53 difindi 3587 . . . . . 6
5453breq1i 4211 . . . . 5
5552, 54syl6ibr 219 . . . 4