# 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 ${⊢}\left({X}\in {V}\wedge {A}\subseteq {X}\wedge ¬{A}\in \mathrm{Fin}\right)\to \left\{{x}\in 𝒫{X}|{A}\setminus {x}\in \mathrm{Fin}\right\}\in \mathrm{Fil}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 difeq2 ${⊢}{x}={y}\to {A}\setminus {x}={A}\setminus {y}$
2 1 eleq1d ${⊢}{x}={y}\to \left({A}\setminus {x}\in \mathrm{Fin}↔{A}\setminus {y}\in \mathrm{Fin}\right)$
3 2 elrab ${⊢}{y}\in \left\{{x}\in 𝒫{X}|{A}\setminus {x}\in \mathrm{Fin}\right\}↔\left({y}\in 𝒫{X}\wedge {A}\setminus {y}\in \mathrm{Fin}\right)$
4 velpw ${⊢}{y}\in 𝒫{X}↔{y}\subseteq {X}$
5 4 anbi1i ${⊢}\left({y}\in 𝒫{X}\wedge {A}\setminus {y}\in \mathrm{Fin}\right)↔\left({y}\subseteq {X}\wedge {A}\setminus {y}\in \mathrm{Fin}\right)$
6 3 5 bitri ${⊢}{y}\in \left\{{x}\in 𝒫{X}|{A}\setminus {x}\in \mathrm{Fin}\right\}↔\left({y}\subseteq {X}\wedge {A}\setminus {y}\in \mathrm{Fin}\right)$
7 6 a1i ${⊢}\left({X}\in {V}\wedge {A}\subseteq {X}\wedge ¬{A}\in \mathrm{Fin}\right)\to \left({y}\in \left\{{x}\in 𝒫{X}|{A}\setminus {x}\in \mathrm{Fin}\right\}↔\left({y}\subseteq {X}\wedge {A}\setminus {y}\in \mathrm{Fin}\right)\right)$
8 elex ${⊢}{X}\in {V}\to {X}\in \mathrm{V}$
9 8 3ad2ant1 ${⊢}\left({X}\in {V}\wedge {A}\subseteq {X}\wedge ¬{A}\in \mathrm{Fin}\right)\to {X}\in \mathrm{V}$
10 ssdif0 ${⊢}{A}\subseteq {X}↔{A}\setminus {X}=\varnothing$
11 0fin ${⊢}\varnothing \in \mathrm{Fin}$
12 eleq1 ${⊢}{A}\setminus {X}=\varnothing \to \left({A}\setminus {X}\in \mathrm{Fin}↔\varnothing \in \mathrm{Fin}\right)$
13 11 12 mpbiri ${⊢}{A}\setminus {X}=\varnothing \to {A}\setminus {X}\in \mathrm{Fin}$
14 10 13 sylbi ${⊢}{A}\subseteq {X}\to {A}\setminus {X}\in \mathrm{Fin}$
15 difeq2 ${⊢}{y}={X}\to {A}\setminus {y}={A}\setminus {X}$
16 15 eleq1d ${⊢}{y}={X}\to \left({A}\setminus {y}\in \mathrm{Fin}↔{A}\setminus {X}\in \mathrm{Fin}\right)$
17 16 sbcieg
18 17 biimpar
19 14 18 sylan2
21 0ex ${⊢}\varnothing \in \mathrm{V}$
22 difeq2 ${⊢}{y}=\varnothing \to {A}\setminus {y}={A}\setminus \varnothing$
23 22 eleq1d ${⊢}{y}=\varnothing \to \left({A}\setminus {y}\in \mathrm{Fin}↔{A}\setminus \varnothing \in \mathrm{Fin}\right)$
24 21 23 sbcie
25 dif0 ${⊢}{A}\setminus \varnothing ={A}$
26 25 eleq1i ${⊢}{A}\setminus \varnothing \in \mathrm{Fin}↔{A}\in \mathrm{Fin}$
27 24 26 sylbb
28 27 con3i
30 sscon ${⊢}{w}\subseteq {z}\to {A}\setminus {z}\subseteq {A}\setminus {w}$
31 ssfi ${⊢}\left({A}\setminus {w}\in \mathrm{Fin}\wedge {A}\setminus {z}\subseteq {A}\setminus {w}\right)\to {A}\setminus {z}\in \mathrm{Fin}$
32 31 expcom ${⊢}{A}\setminus {z}\subseteq {A}\setminus {w}\to \left({A}\setminus {w}\in \mathrm{Fin}\to {A}\setminus {z}\in \mathrm{Fin}\right)$
33 30 32 syl ${⊢}{w}\subseteq {z}\to \left({A}\setminus {w}\in \mathrm{Fin}\to {A}\setminus {z}\in \mathrm{Fin}\right)$
34 vex ${⊢}{w}\in \mathrm{V}$
35 difeq2 ${⊢}{y}={w}\to {A}\setminus {y}={A}\setminus {w}$
36 35 eleq1d ${⊢}{y}={w}\to \left({A}\setminus {y}\in \mathrm{Fin}↔{A}\setminus {w}\in \mathrm{Fin}\right)$
37 34 36 sbcie
38 vex ${⊢}{z}\in \mathrm{V}$
39 difeq2 ${⊢}{y}={z}\to {A}\setminus {y}={A}\setminus {z}$
40 39 eleq1d ${⊢}{y}={z}\to \left({A}\setminus {y}\in \mathrm{Fin}↔{A}\setminus {z}\in \mathrm{Fin}\right)$
41 38 40 sbcie
42 33 37 41 3imtr4g
44 difindi ${⊢}{A}\setminus \left({z}\cap {w}\right)=\left({A}\setminus {z}\right)\cup \left({A}\setminus {w}\right)$
45 unfi ${⊢}\left({A}\setminus {z}\in \mathrm{Fin}\wedge {A}\setminus {w}\in \mathrm{Fin}\right)\to \left({A}\setminus {z}\right)\cup \left({A}\setminus {w}\right)\in \mathrm{Fin}$
46 44 45 eqeltrid ${⊢}\left({A}\setminus {z}\in \mathrm{Fin}\wedge {A}\setminus {w}\in \mathrm{Fin}\right)\to {A}\setminus \left({z}\cap {w}\right)\in \mathrm{Fin}$
47 46 a1i ${⊢}\left(\left({X}\in {V}\wedge {A}\subseteq {X}\wedge ¬{A}\in \mathrm{Fin}\right)\wedge {z}\subseteq {X}\wedge {w}\subseteq {X}\right)\to \left(\left({A}\setminus {z}\in \mathrm{Fin}\wedge {A}\setminus {w}\in \mathrm{Fin}\right)\to {A}\setminus \left({z}\cap {w}\right)\in \mathrm{Fin}\right)$
49 38 inex1 ${⊢}{z}\cap {w}\in \mathrm{V}$
50 difeq2 ${⊢}{y}={z}\cap {w}\to {A}\setminus {y}={A}\setminus \left({z}\cap {w}\right)$
51 50 eleq1d ${⊢}{y}={z}\cap {w}\to \left({A}\setminus {y}\in \mathrm{Fin}↔{A}\setminus \left({z}\cap {w}\right)\in \mathrm{Fin}\right)$
54 7 9 20 29 43 53 isfild ${⊢}\left({X}\in {V}\wedge {A}\subseteq {X}\wedge ¬{A}\in \mathrm{Fin}\right)\to \left\{{x}\in 𝒫{X}|{A}\setminus {x}\in \mathrm{Fin}\right\}\in \mathrm{Fil}\left({X}\right)$