Metamath Proof Explorer


Theorem cfinfil

Description: Relative complements of the finite parts of an infinite set is a filter. When A = NN 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)

Ref Expression
Assertion cfinfil X V A X ¬ A Fin x 𝒫 X | A x Fin Fil X

Proof

Step Hyp Ref Expression
1 difeq2 x = y A x = A y
2 1 eleq1d x = y A x Fin A y Fin
3 2 elrab y x 𝒫 X | A x Fin y 𝒫 X A y Fin
4 velpw y 𝒫 X y X
5 4 anbi1i y 𝒫 X A y Fin y X A y Fin
6 3 5 bitri y x 𝒫 X | A x Fin y X A y Fin
7 6 a1i X V A X ¬ A Fin y x 𝒫 X | A x Fin y X A y Fin
8 elex X V X V
9 8 3ad2ant1 X V A X ¬ A Fin X V
10 ssdif0 A X A X =
11 0fin Fin
12 eleq1 A X = A X Fin Fin
13 11 12 mpbiri A X = A X Fin
14 10 13 sylbi A X A X Fin
15 difeq2 y = X A y = A X
16 15 eleq1d y = X A y Fin A X Fin
17 16 sbcieg X V [˙X / y]˙ A y Fin A X Fin
18 17 biimpar X V A X Fin [˙X / y]˙ A y Fin
19 14 18 sylan2 X V A X [˙X / y]˙ A y Fin
20 19 3adant3 X V A X ¬ A Fin [˙X / y]˙ A y Fin
21 0ex V
22 difeq2 y = A y = A
23 22 eleq1d y = A y Fin A Fin
24 21 23 sbcie [˙ / y]˙ A y Fin A Fin
25 dif0 A = A
26 25 eleq1i A Fin A Fin
27 24 26 sylbb [˙ / y]˙ A y Fin A Fin
28 27 con3i ¬ A Fin ¬ [˙ / y]˙ A y Fin
29 28 3ad2ant3 X V A X ¬ A Fin ¬ [˙ / y]˙ A y Fin
30 sscon w z A z A w
31 ssfi A w Fin A z A w A z Fin
32 31 expcom A z A w A w Fin A z Fin
33 30 32 syl w z A w Fin A z Fin
34 vex w V
35 difeq2 y = w A y = A w
36 35 eleq1d y = w A y Fin A w Fin
37 34 36 sbcie [˙w / y]˙ A y Fin A w Fin
38 vex z V
39 difeq2 y = z A y = A z
40 39 eleq1d y = z A y Fin A z Fin
41 38 40 sbcie [˙z / y]˙ A y Fin A z Fin
42 33 37 41 3imtr4g w z [˙w / y]˙ A y Fin [˙z / y]˙ A y Fin
43 42 3ad2ant3 X V A X ¬ A Fin z X w z [˙w / y]˙ A y Fin [˙z / y]˙ A y Fin
44 difindi A z w = A z A w
45 unfi A z Fin A w Fin A z A w Fin
46 44 45 eqeltrid A z Fin A w Fin A z w Fin
47 46 a1i X V A X ¬ A Fin z X w X A z Fin A w Fin A z w Fin
48 41 37 anbi12i [˙z / y]˙ A y Fin [˙w / y]˙ A y Fin A z Fin A w Fin
49 38 inex1 z w V
50 difeq2 y = z w A y = A z w
51 50 eleq1d y = z w A y Fin A z w Fin
52 49 51 sbcie [˙ z w / y]˙ A y Fin A z w Fin
53 47 48 52 3imtr4g X V A X ¬ A Fin z X w X [˙z / y]˙ A y Fin [˙w / y]˙ A y Fin [˙ z w / y]˙ A y Fin
54 7 9 20 29 43 53 isfild X V A X ¬ A Fin x 𝒫 X | A x Fin Fil X