Metamath Proof Explorer

Theorem 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 ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ Fin ) ) )
8 id ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → 𝑋 ∈ ( FinIa ∖ Fin ) )
9 eldifn ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ¬ 𝑋 ∈ Fin )
10 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ Fin ↔ 𝑋 ∈ Fin ) )
11 10 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin ) )
12 11 sbcieg ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ( [ 𝑋 / 𝑥 ] ¬ 𝑥 ∈ Fin ↔ ¬ 𝑋 ∈ Fin ) )
13 9 12 mpbird ⊢ ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ¬ [ ∅ / 𝑥 ] ¬ 𝑥 ∈ Fin )
22 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑧 ⊆ 𝑦 ) → 𝑧 ∈ Fin )
23 22 expcom ⊢ ( 𝑧 ⊆ 𝑦 → ( 𝑦 ∈ Fin → 𝑧 ∈ Fin ) )
24 23 3ad2ant3 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∈ Fin → 𝑧 ∈ Fin ) )
25 24 con3d ⊢ ( ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) → ( [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin → [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ) )
35 eldifi ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → 𝑋 ∈ FinIa )
36 fin1ai ⊢ ( ( 𝑋 ∈ FinIa ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
37 35 36 sylan ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
38 37 3adant3 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) )
39 inundif ⊢ ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) = 𝑧
40 incom ⊢ ( 𝑧 ∩ 𝑦 ) = ( 𝑦 ∩ 𝑧 )
41 simprl ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑦 ∩ 𝑧 ) ∈ Fin )
42 40 41 eqeltrid ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∩ 𝑦 ) ∈ Fin )
43 simprr ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑋 ∖ 𝑦 ) ∈ Fin )
44 simpl3 ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → 𝑧 ⊆ 𝑋 )
45 44 ssdifd ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∖ 𝑦 ) ⊆ ( 𝑋 ∖ 𝑦 ) )
46 43 45 ssfid ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( 𝑧 ∖ 𝑦 ) ∈ Fin )
47 unfi ⊢ ( ( ( 𝑧 ∩ 𝑦 ) ∈ Fin ∧ ( 𝑧 ∖ 𝑦 ) ∈ Fin ) → ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∈ Fin )
48 42 46 47 syl2anc ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → ( ( 𝑧 ∩ 𝑦 ) ∪ ( 𝑧 ∖ 𝑦 ) ) ∈ Fin )
49 39 48 eqeltrrid ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( ( 𝑦 ∩ 𝑧 ) ∈ Fin ∧ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) ) → 𝑧 ∈ Fin )
50 49 expr ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) → ( ( 𝑋 ∖ 𝑦 ) ∈ Fin → 𝑧 ∈ Fin ) )
51 50 orim2d ⊢ ( ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) ∧ ( 𝑦 ∩ 𝑧 ) ∈ Fin ) → ( ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) )
52 51 ex ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( 𝑦 ∩ 𝑧 ) ∈ Fin → ( ( 𝑦 ∈ Fin ∨ ( 𝑋 ∖ 𝑦 ) ∈ Fin ) → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) ) )
53 38 52 mpid ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( 𝑦 ∩ 𝑧 ) ∈ Fin → ( 𝑦 ∈ Fin ∨ 𝑧 ∈ Fin ) ) )
54 53 con3d ⊢ ( ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑋 ) → ( ( [ 𝑦 / 𝑥 ] ¬ 𝑥 ∈ Fin ∧ [ 𝑧 / 𝑥 ] ¬ 𝑥 ∈ Fin ) → [ ( 𝑦 ∩ 𝑧 ) / 𝑥 ] ¬ 𝑥 ∈ Fin ) )
63 7 8 13 21 34 62 isfild ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
64 9 adantr ⊢ ( ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ¬ ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
72 ianor ⊢ ( ¬ ( 𝑥 ∈ Fin ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) ↔ ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
73 71 72 sylib ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
74 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
75 74 adantl ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ⊆ 𝑋 )
76 6 baib ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin ) )
77 75 76 syl ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ↔ ¬ 𝑥 ∈ Fin ) )
78 1 eleq2i ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) )
79 difss ⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
80 elpw2g ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
81 80 adantr ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
82 79 81 mpbiri ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
83 eldif ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ∧ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
84 83 baib ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 → ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
85 82 84 syl ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
86 78 85 bitrid ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ↔ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) )
87 77 86 orbi12d ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ↔ ( ¬ 𝑥 ∈ Fin ∨ ¬ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) ) )
88 73 87 mpbird ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
89 88 ralrimiva ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
90 isufil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
91 63 89 90 sylanbrc ⊢ ( 𝑋 ∈ ( FinIa ∖ 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 ⊢ ( ( 𝑋 ∈ ( FinIa ∖ Fin ) ∧ 𝑥 ∈ ∩ 𝐹 ) → { 𝑥 } ∈ 𝐹 )
98 97 ex ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ( 𝑥 ∈ ∩ 𝐹 → { 𝑥 } ∈ 𝐹 ) )
99 95 98 mtoi ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ¬ 𝑥 ∈ ∩ 𝐹 )
100 99 eq0rdv ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ∩ 𝐹 = ∅ )
101 91 100 jca ⊢ ( 𝑋 ∈ ( FinIa ∖ Fin ) → ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∩ 𝐹 = ∅ ) )