Metamath Proof Explorer

Theorem ufileu

Description: If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion ufileu ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
2 ufilmax ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) → 𝐹 = 𝑓 )
3 2 3expa ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑓 ) → 𝐹 = 𝑓 )
4 3 eqcomd ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑓 ) → 𝑓 = 𝐹 )
5 4 ex ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝐹 ) )
6 1 5 sylan2 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝐹 ) )
7 6 ralrimiva ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝐹 ) )
8 ssid ⊢ 𝐹 ⊆ 𝐹
9 sseq2 ⊢ ( 𝑓 = 𝐹 → ( 𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝐹 ) )
10 9 eqreu ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝐹 ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝐹 ) ) → ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
11 8 10 mp3an2 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝐹 ) ) → ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
12 7 11 mpdan ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 )
13 reu6 ⊢ ( ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ↔ ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) )
14 ibibr ⊢ ( ( 𝑓 = 𝑔 → 𝐹 ⊆ 𝑓 ) ↔ ( 𝑓 = 𝑔 → ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) )
15 14 pm5.74ri ⊢ ( 𝑓 = 𝑔 → ( 𝐹 ⊆ 𝑓 ↔ ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) )
16 sseq2 ⊢ ( 𝑓 = 𝑔 → ( 𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ 𝑔 ) )
17 15 16 bitr3d ⊢ ( 𝑓 = 𝑔 → ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ↔ 𝐹 ⊆ 𝑔 ) )
18 17 rspcva ⊢ ( ( 𝑔 ∈ ( UFil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝐹 ⊆ 𝑔 )
19 18 adantll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝐹 ⊆ 𝑔 )
20 ufilfil ⊢ ( 𝑔 ∈ ( UFil ‘ 𝑋 ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
21 filelss ⊢ ( ( 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑔 ) → 𝑥 ⊆ 𝑋 )
22 21 ex ⊢ ( 𝑔 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋 ) )
23 20 22 syl ⊢ ( 𝑔 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋 ) )
24 23 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ 𝑔 → 𝑥 ⊆ 𝑋 ) )
25 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
26 25 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝐹 ⊆ 𝒫 𝑋 )
27 difss ⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
28 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
29 28 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝑋 ∈ 𝐹 )
30 difexg ⊢ ( 𝑋 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ V )
31 29 30 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ V )
32 elpwg ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
33 31 32 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
34 27 33 mpbiri ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
35 34 snssd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → { ( 𝑋 ∖ 𝑥 ) } ⊆ 𝒫 𝑋 )
36 26 35 unssd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 )
37 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } )
38 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
39 38 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝐹 ≠ ∅ )
40 ssn0 ⊢ ( ( 𝐹 ⊆ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∧ 𝐹 ≠ ∅ ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ )
41 37 39 40 sylancr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ )
42 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑓 ∈ 𝐹 ) → 𝑓 ⊆ 𝑋 )
43 42 ad2ant2rl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → 𝑓 ⊆ 𝑋 )
44 df-ss ⊢ ( 𝑓 ⊆ 𝑋 ↔ ( 𝑓 ∩ 𝑋 ) = 𝑓 )
45 43 44 sylib ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → ( 𝑓 ∩ 𝑋 ) = 𝑓 )
46 45 sseq1d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → ( ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑥 ) )
47 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑓 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐹 )
48 47 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑓 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( 𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )
49 48 impcomd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) → ( 𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
50 49 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) → ( ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) → ( 𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
51 50 imp ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → ( 𝑓 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
52 46 51 sylbid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → ( ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
53 52 con3d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ 𝐹 ) ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) )
54 53 expr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑓 ∈ 𝐹 → ( ¬ 𝑥 ∈ 𝐹 → ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) ) )
55 54 com23 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑓 ∈ 𝐹 → ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) ) )
56 55 impr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑓 ∈ 𝐹 → ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) )
57 56 imp ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) ∧ 𝑓 ∈ 𝐹 ) → ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 )
58 ineq2 ⊢ ( 𝑔 = ( 𝑋 ∖ 𝑥 ) → ( 𝑓 ∩ 𝑔 ) = ( 𝑓 ∩ ( 𝑋 ∖ 𝑥 ) ) )
59 58 neeq1d ⊢ ( 𝑔 = ( 𝑋 ∖ 𝑥 ) → ( ( 𝑓 ∩ 𝑔 ) ≠ ∅ ↔ ( 𝑓 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) )
60 59 ralsng ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ↔ ( 𝑓 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ ) )
61 inssdif0 ⊢ ( ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ↔ ( 𝑓 ∩ ( 𝑋 ∖ 𝑥 ) ) = ∅ )
62 61 necon3bbii ⊢ ( ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ↔ ( 𝑓 ∩ ( 𝑋 ∖ 𝑥 ) ) ≠ ∅ )
63 60 62 bitr4di ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ↔ ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) )
64 31 63 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ↔ ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) )
65 64 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ↔ ¬ ( 𝑓 ∩ 𝑋 ) ⊆ 𝑥 ) )
66 57 65 mpbird ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) ∧ 𝑓 ∈ 𝐹 ) → ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ )
67 66 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ )
68 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
69 68 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
70 difssd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 )
71 ssdif0 ⊢ ( 𝑋 ⊆ 𝑥 ↔ ( 𝑋 ∖ 𝑥 ) = ∅ )
72 eqss ⊢ ( 𝑥 = 𝑋 ↔ ( 𝑥 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝑥 ) )
73 72 simplbi2 ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑋 ⊆ 𝑥 → 𝑥 = 𝑋 ) )
74 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹 ) )
75 74 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ 𝐹 ↔ ¬ 𝑋 ∈ 𝐹 ) )
76 75 biimpcd ⊢ ( ¬ 𝑥 ∈ 𝐹 → ( 𝑥 = 𝑋 → ¬ 𝑋 ∈ 𝐹 ) )
77 73 76 sylan9 ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) → ( 𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹 ) )
78 77 adantl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ⊆ 𝑥 → ¬ 𝑋 ∈ 𝐹 ) )
79 71 78 syl5bir ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( 𝑋 ∖ 𝑥 ) = ∅ → ¬ 𝑋 ∈ 𝐹 ) )
80 79 necon2ad ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ≠ ∅ ) )
81 29 80 mpd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ≠ ∅ )
82 snfbas ⊢ ( ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑥 ) ≠ ∅ ∧ 𝑋 ∈ 𝐹 ) → { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) )
83 70 81 29 82 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) )
84 fbunfip ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ { ( 𝑋 ∖ 𝑥 ) } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ↔ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ) )
85 69 83 84 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ↔ ∀ 𝑓 ∈ 𝐹 ∀ 𝑔 ∈ { ( 𝑋 ∖ 𝑥 ) } ( 𝑓 ∩ 𝑔 ) ≠ ∅ ) )
86 67 85 mpbird ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
87 fsubbas ⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ) )
88 29 87 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ) )
89 36 41 86 88 mpbir3and ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) )
90 fgcl ⊢ ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
91 89 90 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
92 filssufil ⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 )
93 91 92 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 )
94 r19.29 ⊢ ( ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ∧ ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) )
95 biimp ⊢ ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) → ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝑔 ) )
96 simpll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
97 snex ⊢ { ( 𝑋 ∖ 𝑥 ) } ∈ V
98 unexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ { ( 𝑋 ∖ 𝑥 ) } ∈ V ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V )
99 96 97 98 sylancl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V )
100 ssfii ⊢ ( ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ∈ V → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
101 99 100 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) )
102 ssfg ⊢ ( ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
103 89 102 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
104 101 103 sstrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
105 104 unssad ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
106 sstr2 ⊢ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → 𝐹 ⊆ 𝑓 ) )
107 105 106 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → 𝐹 ⊆ 𝑓 ) )
108 107 imim1d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( 𝐹 ⊆ 𝑓 → 𝑓 = 𝑔 ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → 𝑓 = 𝑔 ) ) )
109 sseq2 ⊢ ( 𝑓 = 𝑔 → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ↔ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
110 109 biimpcd ⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → ( 𝑓 = 𝑔 → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
111 110 a2i ⊢ ( ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → 𝑓 = 𝑔 ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
112 95 108 111 syl56 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) → ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) ) )
113 112 impd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
114 113 rexlimdvw ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ∧ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
115 94 114 syl5 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ∧ ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑓 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
116 93 115 mpan2d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 ) )
117 116 imp ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 )
118 117 an32s ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) ⊆ 𝑔 )
119 snidg ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ V → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
120 31 119 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } )
121 elun2 ⊢ ( ( 𝑋 ∖ 𝑥 ) ∈ { ( 𝑋 ∖ 𝑥 ) } → ( 𝑋 ∖ 𝑥 ) ∈ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) )
122 120 121 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) )
123 104 122 sseldd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
124 123 adantlr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { ( 𝑋 ∖ 𝑥 ) } ) ) ) )
125 118 124 sseldd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝑔 )
126 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝑔 ∈ ( UFil ‘ 𝑋 ) )
127 simprl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → 𝑥 ⊆ 𝑋 )
128 ufilb ⊢ ( ( 𝑔 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝑔 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝑔 ) )
129 126 127 128 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ( ¬ 𝑥 ∈ 𝑔 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝑔 ) )
130 125 129 mpbird ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ ( 𝑥 ⊆ 𝑋 ∧ ¬ 𝑥 ∈ 𝐹 ) ) → ¬ 𝑥 ∈ 𝑔 )
131 130 expr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ 𝑔 ) )
132 131 con4d ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹 ) )
133 132 ex ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹 ) ) )
134 133 com23 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ 𝑔 → ( 𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝐹 ) ) )
135 24 134 mpdd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ 𝑔 → 𝑥 ∈ 𝐹 ) )
136 135 ssrdv ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝑔 ⊆ 𝐹 )
137 19 136 eqssd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝐹 = 𝑔 )
138 simplr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝑔 ∈ ( UFil ‘ 𝑋 ) )
139 137 138 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ∈ ( UFil ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
140 139 rexlimdva2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ↔ 𝑓 = 𝑔 ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) ) )
141 13 140 syl5bi ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 → 𝐹 ∈ ( UFil ‘ 𝑋 ) ) )
142 12 141 impbid2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ∃! 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝐹 ⊆ 𝑓 ) )