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	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		difeq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
2	1	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
3	2	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
4		velpw	⊢ ( 𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋 )
5	4	anbi1i	⊢ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
6	3 5	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
7	6	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ) )
8		simp1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → 𝑋 ∈ 𝑉 )
9		ssdif0	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝐴 ∖ 𝑋 ) = ∅ )
10		0fi	⊢ ∅ ∈ Fin
11		eleq1	⊢ ( ( 𝐴 ∖ 𝑋 ) = ∅ → ( ( 𝐴 ∖ 𝑋 ) ∈ Fin ↔ ∅ ∈ Fin ) )
12	10 11	mpbiri	⊢ ( ( 𝐴 ∖ 𝑋 ) = ∅ → ( 𝐴 ∖ 𝑋 ) ∈ Fin )
13	9 12	sylbi	⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐴 ∖ 𝑋 ) ∈ Fin )
14		difeq2	⊢ ( 𝑦 = 𝑋 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ 𝑋 ) )
15	14	eleq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) )
16	15	sbcieg	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) )
17	16	biimpar	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∖ 𝑋 ) ∈ Fin ) → [ 𝑋 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin )
18	13 17	sylan2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ) → [ 𝑋 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin )
19	18	3adant3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → [ 𝑋 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin )
20		0ex	⊢ ∅ ∈ V
21		difeq2	⊢ ( 𝑦 = ∅ → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ∅ ) )
22	21	eleq1d	⊢ ( 𝑦 = ∅ → ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ ∅ ) ∈ Fin ) )
23	20 22	sbcie	⊢ ( [ ∅ / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ ∅ ) ∈ Fin )
24		dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴
25	24	eleq1i	⊢ ( ( 𝐴 ∖ ∅ ) ∈ Fin ↔ 𝐴 ∈ Fin )
26	23 25	sylbb	⊢ ( [ ∅ / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin → 𝐴 ∈ Fin )
27	26	con3i	⊢ ( ¬ 𝐴 ∈ Fin → ¬ [ ∅ / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin )
28	27	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ¬ [ ∅ / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin )
29		sscon	⊢ ( 𝑤 ⊆ 𝑧 → ( 𝐴 ∖ 𝑧 ) ⊆ ( 𝐴 ∖ 𝑤 ) )
30		ssfi	⊢ ( ( ( 𝐴 ∖ 𝑤 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑧 ) ⊆ ( 𝐴 ∖ 𝑤 ) ) → ( 𝐴 ∖ 𝑧 ) ∈ Fin )
31	30	expcom	⊢ ( ( 𝐴 ∖ 𝑧 ) ⊆ ( 𝐴 ∖ 𝑤 ) → ( ( 𝐴 ∖ 𝑤 ) ∈ Fin → ( 𝐴 ∖ 𝑧 ) ∈ Fin ) )
32	29 31	syl	⊢ ( 𝑤 ⊆ 𝑧 → ( ( 𝐴 ∖ 𝑤 ) ∈ Fin → ( 𝐴 ∖ 𝑧 ) ∈ Fin ) )
33		vex	⊢ 𝑤 ∈ V
34		difeq2	⊢ ( 𝑦 = 𝑤 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ 𝑤 ) )
35	34	eleq1d	⊢ ( 𝑦 = 𝑤 → ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑤 ) ∈ Fin ) )
36	33 35	sbcie	⊢ ( [ 𝑤 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑤 ) ∈ Fin )
37		vex	⊢ 𝑧 ∈ V
38		difeq2	⊢ ( 𝑦 = 𝑧 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ 𝑧 ) )
39	38	eleq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑧 ) ∈ Fin ) )
40	37 39	sbcie	⊢ ( [ 𝑧 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑧 ) ∈ Fin )
41	32 36 40	3imtr4g	⊢ ( 𝑤 ⊆ 𝑧 → ( [ 𝑤 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin → [ 𝑧 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
42	41	3ad2ant3	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( [ 𝑤 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin → [ 𝑧 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
43		difindi	⊢ ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) = ( ( 𝐴 ∖ 𝑧 ) ∪ ( 𝐴 ∖ 𝑤 ) )
44		unfi	⊢ ( ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑤 ) ∈ Fin ) → ( ( 𝐴 ∖ 𝑧 ) ∪ ( 𝐴 ∖ 𝑤 ) ) ∈ Fin )
45	43 44	eqeltrid	⊢ ( ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑤 ) ∈ Fin ) → ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) ∈ Fin )
46	45	a1i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑤 ) ∈ Fin ) → ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) ∈ Fin ) )
47	40 36	anbi12i	⊢ ( ( [ 𝑧 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ∧ [ 𝑤 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ) ↔ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑤 ) ∈ Fin ) )
48	37	inex1	⊢ ( 𝑧 ∩ 𝑤 ) ∈ V
49		difeq2	⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) )
50	49	eleq1d	⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) ∈ Fin ) )
51	48 50	sbcie	⊢ ( [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝑧 ∩ 𝑤 ) ) ∈ Fin )
52	46 47 51	3imtr4g	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( [ 𝑧 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ∧ [ 𝑤 / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ) → [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
53	7 8 19 28 42 52	isfild	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )