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 \in V \land A \subseteq X \land \neg A \in Fin) \to \{x \in 𝒫 X \| A ∖ x \in Fin\} \in Fil (X)$

Proof

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

Metamath Proof Explorer

Theorem cfinfil

Proof