fin1aufil

Description: There are no definable free ultrafilters in ZFC. However, there are free ultrafilters in some choice-denying constructions. Here we show that given an amorphous set (a.k.a. a Ia-finite I-infinite set) X , the set of infinite subsets of X is a free ultrafilter on X . (Contributed by Mario Carneiro, 20-May-2015)

		Ref	Expression
	Hypothesis	fin1aufil.1	⊢ 𝐹 = ( 𝒫 𝑋 ∖ Fin )
	Assertion	fin1aufil	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∩ 𝐹 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fin1aufil.1	⊢ 𝐹 = ( 𝒫 𝑋 ∖ Fin )
2	1	eleq2i	⊢ ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ ( 𝒫 𝑋 ∖ Fin ) )
3		eldif	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ( 𝑥 ∈ 𝒫 𝑋 ∧ ¬ 𝑥 ∈ Fin ) )
4		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 )
5	4	anbi1i	⊢ ( ( 𝑥 ∈ 𝒫 𝑋 ∧ ¬ 𝑥 ∈ Fin ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin ) )
6	2 3 5	3bitri	⊢ ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin ) )
7	6	a1i	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin ) ) )
8		id	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → 𝑋 ∈ ( Fin^Ia ∖ Fin ) )
9		eldifn	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ¬ 𝑋 ∈ Fin )
10		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ Fin ↔ 𝑋 ∈ Fin ) )
11	10	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin ) )
12	11	sbcieg	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( [ 𝑋 / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin ) )
13	9 12	mpbird	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → [ 𝑋 / 𝑥 ] ¬ 𝑥 ∈ Fin )
14		0fi	⊢ ∅ ∈ Fin
15		0ex	⊢ ∅ ∈ V
16		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ Fin ↔ ∅ ∈ Fin ) )
17	16	notbid	⊢ ( 𝑥 = ∅ → ( ¬ 𝑥 ∈ Fin ↔ ¬ ∅ ∈ Fin ) )
18	15 17	sbcie	⊢ ( [ ∅ / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ ∅ ∈ Fin )
19	18	con2bii	⊢ ( ∅ ∈ Fin ↔ ¬ [ ∅ / 𝑥 ] ¬ 𝑥 ∈ Fin )
20	14 19	mpbi	⊢ ¬ [ ∅ / 𝑥 ] ¬ 𝑥 ∈ Fin
21	20	a1i	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ¬ [ ∅ / 𝑥 ] ¬ 𝑥 ∈ Fin )
22		ssfi	⊢ ( ( 𝑦 ∈ Fin ∧ 𝑧 ⊆ 𝑦 ) → 𝑧 ∈ Fin )
23	22	expcom	⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑦 ∈ Fin → 𝑧 ∈ Fin ) )
24	23	3ad2ant3	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∈ Fin → 𝑧 ∈ Fin ) )
25	24	con3d	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) → ( ¬ 𝑧 ∈ Fin → ¬ 𝑦 ∈ Fin ) )
26		vex	⊢ 𝑧 ∈ V
27		eleq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ Fin ↔ 𝑧 ∈ Fin ) )
28	27	notbid	⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑥 ∈ Fin ↔ ¬ 𝑧 ∈ Fin ) )
29	26 28	sbcie	⊢ ( [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑧 ∈ Fin )
30		vex	⊢ 𝑦 ∈ V
31		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ Fin ↔ 𝑦 ∈ Fin ) )
32	31	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ Fin ↔ ¬ 𝑦 ∈ Fin ) )
33	30 32	sbcie	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑦 ∈ Fin )
34	25 29 33	3imtr4g	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) → ( [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin → [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ) )
35		eldifi	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → 𝑋 ∈ Fin^Ia )
36		fin1ai	⊢ ( ( 𝑋 ∈ Fin^Ia ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
37	35 36	sylan	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
38	37	3adant3	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
39		inundif	⊢ ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) = 𝑧
40		incom	⊢ ( 𝑧 ∩ 𝑦 ) = ( 𝑦 ∩ 𝑧 )
41		simprl	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑦 ∩ 𝑧 ) ∈ Fin )
42	40 41	eqeltrid	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∩ 𝑦 ) ∈ Fin )
43		simprr	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑋 ∖ 𝑦 ) ∈ Fin )
44		simpl3	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → 𝑧 ⊆ 𝑋 )
45	44	ssdifd	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∖ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑦 ) )
46	43 45	ssfid	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∖ 𝑦 ) ∈ Fin )
47		unfi	⊢ ( ( ( 𝑧 ∩ 𝑦 ) ∈ Fin ∧ ( 𝑧 ∖ 𝑦 ) ∈ Fin ) → ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∈ Fin )
48	42 46 47	syl2anc	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∈ Fin )
49	39 48	eqeltrrid	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → 𝑧 ∈ Fin )
50	49	expr	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) → ( ( 𝑋 ∖ 𝑦 ) ∈ Fin → 𝑧 ∈ Fin ) )
51	50	orim2d	⊢ ( ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) → ( ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) )
52	51	ex	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( 𝑦 ∩ 𝑧 ) ∈ Fin → ( ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) ) )
53	38 52	mpid	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( 𝑦 ∩ 𝑧 ) ∈ Fin → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) )
54	53	con3d	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ¬ ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) → ¬ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) )
55	33 29	anbi12i	⊢ ( ( [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ∧ [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin ) ↔ ( ¬ 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ Fin ) )
56		ioran	⊢ ( ¬ ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ↔ ( ¬ 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ Fin ) )
57	55 56	bitr4i	⊢ ( ( [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ∧ [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin ) ↔ ¬ ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) )
58	30	inex1	⊢ ( 𝑦 ∩ 𝑧 ) ∈ V
59		eleq1	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( 𝑥 ∈ Fin ↔ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) )
60	59	notbid	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( ¬ 𝑥 ∈ Fin ↔ ¬ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) )
61	58 60	sbcie	⊢ ( [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ ( 𝑦 ∩ 𝑧 ) ∈ Fin )
62	54 57 61	3imtr4g	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ∧ [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] ¬ 𝑥 ∈ Fin ) )
63	7 8 13 21 34 62	isfild	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
64	9	adantr	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ¬ 𝑋 ∈ Fin )
65		unfi	⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ( 𝑥 ∪ ( 𝑋 ∖ 𝑥 ) ) ∈ Fin )
66		ssun2	⊢ 𝑋 ⊆ ( 𝑥 ∪ 𝑋 )
67		undif2	⊢ ( 𝑥 ∪ ( 𝑋 ∖ 𝑥 ) ) = ( 𝑥 ∪ 𝑋 )
68	66 67	sseqtrri	⊢ 𝑋 ⊆ ( 𝑥 ∪ ( 𝑋 ∖ 𝑥 ) )
69		ssfi	⊢ ( ( ( 𝑥 ∪ ( 𝑋 ∖ 𝑥 ) ) ∈ Fin ∧ 𝑋 ⊆ ( 𝑥 ∪ ( 𝑋 ∖ 𝑥 ) ) ) → 𝑋 ∈ Fin )
70	65 68 69	sylancl	⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → 𝑋 ∈ Fin )
71	64 70	nsyl	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ¬ ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
72		ianor	⊢ ( ¬ ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) ↔ ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
73	71 72	sylib	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
74		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
75	74	adantl	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ⊆ 𝑋 )
76	6	baib	⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin ) )
77	75 76	syl	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin ) )
78	1	eleq2i	⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) )
79		difss	⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
80		elpw2g	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
81	80	adantr	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
82	79 81	mpbiri	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
83		eldif	⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ∧ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
84	83	baib	⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 → ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
85	82 84	syl	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
86	78 85	bitrid	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
87	77 86	orbi12d	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ↔ ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) ) )
88	73 87	mpbird	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
89	88	ralrimiva	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
90		isufil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
91	63 89 90	sylanbrc	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
92		snfi	⊢ { 𝑥 } ∈ Fin
93		eldifn	⊢ ( { 𝑥 } ∈ ( 𝒫 𝑋 ∖ Fin ) → ¬ { 𝑥 } ∈ Fin )
94	93 1	eleq2s	⊢ ( { 𝑥 } ∈ 𝐹 → ¬ { 𝑥 } ∈ Fin )
95	92 94	mt2	⊢ ¬ { 𝑥 } ∈ 𝐹
96		uffixsn	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → { 𝑥 } ∈ 𝐹 )
97	91 96	sylan	⊢ ( ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) ∧ 𝑥 ∈ ∩ 𝐹 ) → { 𝑥 } ∈ 𝐹 )
98	97	ex	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( 𝑥 ∈ ∩ 𝐹 → { 𝑥 } ∈ 𝐹 ) )
99	95 98	mtoi	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ¬ 𝑥 ∈ ∩ 𝐹 )
100	99	eq0rdv	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ∩ 𝐹 = ∅ )
101	91 100	jca	⊢ ( 𝑋 ∈ ( Fin^Ia ∖ Fin ) → ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∩ 𝐹 = ∅ ) )

Metamath Proof Explorer

Theorem fin1aufil

Proof