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

Theorem cfinfil 17927
 Description: Relative complements of the finite parts of an infinite set is a filter. When the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence. (Contributed by FL, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
cfinfil
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem cfinfil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difeq2 3461 . . . . . 6
21eleq1d 2504 . . . . 5
32elrab 3094 . . . 4
4 vex 2961 . . . . . 6
54elpw 3807 . . . . 5
65anbi1i 678 . . . 4
73, 6bitri 242 . . 3
87a1i 11 . 2
9 elex 2966 . . 3
11 ssdif0 3688 . . . . 5
12 0fin 7338 . . . . . 6
13 eleq1 2498 . . . . . 6
1412, 13mpbiri 226 . . . . 5
1511, 14sylbi 189 . . . 4
16 difeq2 3461 . . . . . . 7
1716eleq1d 2504 . . . . . 6
1817sbcieg 3195 . . . . 5
1918biimpar 473 . . . 4
2015, 19sylan2 462 . . 3
22 0ex 4341 . . . . . . 7
23 difeq2 3461 . . . . . . . 8
2423eleq1d 2504 . . . . . . 7
2522, 24sbcie 3197 . . . . . 6
26 dif0 3700 . . . . . . 7
2726eleq1i 2501 . . . . . 6
2825, 27bitri 242 . . . . 5
2928biimpi 188 . . . 4
3029con3i 130 . . 3
32 sscon 3483 . . . . 5
33 ssfi 7331 . . . . . 6
3433expcom 426 . . . . 5
3532, 34syl 16 . . . 4
36 vex 2961 . . . . 5
37 difeq2 3461 . . . . . 6
3837eleq1d 2504 . . . . 5
3936, 38sbcie 3197 . . . 4
40 vex 2961 . . . . 5
41 difeq2 3461 . . . . . 6
4241eleq1d 2504 . . . . 5
4340, 42sbcie 3197 . . . 4
4435, 39, 433imtr4g 263 . . 3