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 simp1 ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin → X ∈ V
9 ssdif0 ⊢ A ⊆ X ↔ A ∖ X = ∅
10 0fi ⊢ ∅ ∈ Fin
11 eleq1 ⊢ A ∖ X = ∅ → A ∖ X ∈ Fin ↔ ∅ ∈ Fin
12 10 11 mpbiri ⊢ A ∖ X = ∅ → A ∖ X ∈ Fin
13 9 12 sylbi ⊢ A ⊆ X → A ∖ X ∈ Fin
14 difeq2 ⊢ y = X → A ∖ y = A ∖ X
15 14 eleq1d ⊢ y = X → A ∖ y ∈ Fin ↔ A ∖ X ∈ Fin
16 15 sbcieg ⊢ X ∈ V → [˙X / y]˙ A ∖ y ∈ Fin ↔ A ∖ X ∈ Fin
17 16 biimpar ⊢ X ∈ V ∧ A ∖ X ∈ Fin → [˙X / y]˙ A ∖ y ∈ Fin
18 13 17 sylan2 ⊢ X ∈ V ∧ A ⊆ X → [˙X / y]˙ A ∖ y ∈ Fin
19 18 3adant3 ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin → [˙X / y]˙ A ∖ y ∈ Fin
20 0ex ⊢ ∅ ∈ V
21 difeq2 ⊢ y = ∅ → A ∖ y = A ∖ ∅
22 21 eleq1d ⊢ y = ∅ → A ∖ y ∈ Fin ↔ A ∖ ∅ ∈ Fin
23 20 22 sbcie ⊢ [˙∅ / y]˙ A ∖ y ∈ Fin ↔ A ∖ ∅ ∈ Fin
24 dif0 ⊢ A ∖ ∅ = A
25 24 eleq1i ⊢ A ∖ ∅ ∈ Fin ↔ A ∈ Fin
26 23 25 sylbb ⊢ [˙∅ / y]˙ A ∖ y ∈ Fin → A ∈ Fin
27 26 con3i ⊢ ¬ A ∈ Fin → ¬ [˙∅ / y]˙ A ∖ y ∈ Fin
28 27 3ad2ant3 ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin → ¬ [˙∅ / y]˙ A ∖ y ∈ Fin
29 sscon ⊢ w ⊆ z → A ∖ z ⊆ A ∖ w
30 ssfi ⊢ A ∖ w ∈ Fin ∧ A ∖ z ⊆ A ∖ w → A ∖ z ∈ Fin
31 30 expcom ⊢ A ∖ z ⊆ A ∖ w → A ∖ w ∈ Fin → A ∖ z ∈ Fin
32 29 31 syl ⊢ w ⊆ z → A ∖ w ∈ Fin → A ∖ z ∈ Fin
33 vex ⊢ w ∈ V
34 difeq2 ⊢ y = w → A ∖ y = A ∖ w
35 34 eleq1d ⊢ y = w → A ∖ y ∈ Fin ↔ A ∖ w ∈ Fin
36 33 35 sbcie ⊢ [˙w / y]˙ A ∖ y ∈ Fin ↔ A ∖ w ∈ Fin
37 vex ⊢ z ∈ V
38 difeq2 ⊢ y = z → A ∖ y = A ∖ z
39 38 eleq1d ⊢ y = z → A ∖ y ∈ Fin ↔ A ∖ z ∈ Fin
40 37 39 sbcie ⊢ [˙z / y]˙ A ∖ y ∈ Fin ↔ A ∖ z ∈ Fin
41 32 36 40 3imtr4g ⊢ w ⊆ z → [˙w / y]˙ A ∖ y ∈ Fin → [˙z / y]˙ A ∖ y ∈ Fin
42 41 3ad2ant3 ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ⊆ X ∧ w ⊆ z → [˙w / y]˙ A ∖ y ∈ Fin → [˙z / y]˙ A ∖ y ∈ Fin
43 difindi ⊢ A ∖ z ∩ w = A ∖ z ∪ A ∖ w
44 unfi ⊢ A ∖ z ∈ Fin ∧ A ∖ w ∈ Fin → A ∖ z ∪ A ∖ w ∈ Fin
45 43 44 eqeltrid ⊢ A ∖ z ∈ Fin ∧ A ∖ w ∈ Fin → A ∖ z ∩ w ∈ Fin
46 45 a1i ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ⊆ X ∧ w ⊆ X → A ∖ z ∈ Fin ∧ A ∖ w ∈ Fin → A ∖ z ∩ w ∈ Fin
47 40 36 anbi12i ⊢ [˙z / y]˙ A ∖ y ∈ Fin ∧ [˙w / y]˙ A ∖ y ∈ Fin ↔ A ∖ z ∈ Fin ∧ A ∖ w ∈ Fin
48 37 inex1 ⊢ z ∩ w ∈ V
49 difeq2 ⊢ y = z ∩ w → A ∖ y = A ∖ z ∩ w
50 49 eleq1d ⊢ y = z ∩ w → A ∖ y ∈ Fin ↔ A ∖ z ∩ w ∈ Fin
51 48 50 sbcie ⊢ [˙ z ∩ w / y]˙ A ∖ y ∈ Fin ↔ A ∖ z ∩ w ∈ Fin
52 46 47 51 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
53 7 8 19 28 42 52 isfild ⊢ X ∈ V ∧ A ⊆ X ∧ ¬ A ∈ Fin → x ∈ 𝒫 X | A ∖ x ∈ Fin ∈ Fil ⁡ X