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 e. V /\ A C_ X /\ -. A e. Fin ) -> { x e. ~P X | ( A \ x ) e. Fin } e. ( Fil ` X ) )

Proof

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