Step |
Hyp |
Ref |
Expression |
1 |
|
ufilfil |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
2 |
|
ufilmax |
⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) → 𝐹 = 𝑓 ) |
3 |
2
|
3expia |
⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) |
4 |
3
|
ralrimiva |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) |
5 |
1 4
|
jca |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ) |
6 |
|
simpl |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
7 |
|
velpw |
⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 ) |
8 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
9 |
|
snex |
⊢ { 𝑥 } ∈ V |
10 |
|
unexg |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ { 𝑥 } ∈ V ) → ( 𝐹 ∪ { 𝑥 } ) ∈ V ) |
11 |
8 9 10
|
sylancl |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ∈ V ) |
12 |
|
ssfii |
⊢ ( ( 𝐹 ∪ { 𝑥 } ) ∈ V → ( 𝐹 ∪ { 𝑥 } ) ⊆ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) |
13 |
11 12
|
syl |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ⊆ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) |
14 |
|
filsspw |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ⊆ 𝒫 𝑋 ) |
16 |
7
|
biimpri |
⊢ ( 𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝒫 𝑋 ) |
17 |
16
|
ad2antlr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ∈ 𝒫 𝑋 ) |
18 |
17
|
snssd |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → { 𝑥 } ⊆ 𝒫 𝑋 ) |
19 |
15 18
|
unssd |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ⊆ 𝒫 𝑋 ) |
20 |
|
ssun2 |
⊢ { 𝑥 } ⊆ ( 𝐹 ∪ { 𝑥 } ) |
21 |
|
vex |
⊢ 𝑥 ∈ V |
22 |
21
|
snnz |
⊢ { 𝑥 } ≠ ∅ |
23 |
|
ssn0 |
⊢ ( ( { 𝑥 } ⊆ ( 𝐹 ∪ { 𝑥 } ) ∧ { 𝑥 } ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ) |
24 |
20 22 23
|
mp2an |
⊢ ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ |
25 |
24
|
a1i |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ) |
26 |
|
simpr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) |
27 |
|
ineq2 |
⊢ ( 𝑓 = 𝑥 → ( 𝑦 ∩ 𝑓 ) = ( 𝑦 ∩ 𝑥 ) ) |
28 |
27
|
neeq1d |
⊢ ( 𝑓 = 𝑥 → ( ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) ) |
29 |
21 28
|
ralsn |
⊢ ( ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) |
30 |
29
|
ralbii |
⊢ ( ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) |
31 |
26 30
|
sylibr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ) |
32 |
|
filfbas |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
34 |
|
simplr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ⊆ 𝑋 ) |
35 |
|
inss2 |
⊢ ( 𝑋 ∩ 𝑥 ) ⊆ 𝑥 |
36 |
|
filtop |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 ) |
37 |
36
|
adantr |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑋 ∈ 𝐹 ) |
38 |
|
ineq1 |
⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∩ 𝑥 ) = ( 𝑋 ∩ 𝑥 ) ) |
39 |
38
|
neeq1d |
⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) ) |
40 |
39
|
rspcva |
⊢ ( ( 𝑋 ∈ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) |
41 |
37 40
|
sylan |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) |
42 |
|
ssn0 |
⊢ ( ( ( 𝑋 ∩ 𝑥 ) ⊆ 𝑥 ∧ ( 𝑋 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ≠ ∅ ) |
43 |
35 41 42
|
sylancr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ≠ ∅ ) |
44 |
36
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑋 ∈ 𝐹 ) |
45 |
|
snfbas |
⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ ∅ ∧ 𝑋 ∈ 𝐹 ) → { 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) |
46 |
34 43 44 45
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → { 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) |
47 |
|
fbunfip |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ) ) |
48 |
33 46 47
|
syl2anc |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑓 ∈ { 𝑥 } ( 𝑦 ∩ 𝑓 ) ≠ ∅ ) ) |
49 |
31 48
|
mpbird |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) |
50 |
|
fsubbas |
⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
51 |
44 50
|
syl |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
52 |
19 25 49 51
|
mpbir3and |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ) |
53 |
|
ssfg |
⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) |
54 |
52 53
|
syl |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) |
55 |
13 54
|
sstrd |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 ∪ { 𝑥 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) |
56 |
55
|
unssad |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) |
57 |
|
fgcl |
⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ) |
58 |
|
sseq2 |
⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
59 |
|
eqeq2 |
⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝐹 = 𝑓 ↔ 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
60 |
58 59
|
imbi12d |
⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ↔ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) ) |
61 |
60
|
rspcv |
⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) ) |
62 |
52 57 61
|
3syl |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) ) |
63 |
56 62
|
mpid |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
64 |
|
vsnid |
⊢ 𝑥 ∈ { 𝑥 } |
65 |
20 64
|
sselii |
⊢ 𝑥 ∈ ( 𝐹 ∪ { 𝑥 } ) |
66 |
65
|
a1i |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ∈ ( 𝐹 ∪ { 𝑥 } ) ) |
67 |
55 66
|
sseldd |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → 𝑥 ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) |
68 |
|
eleq2 |
⊢ ( 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) ) ) |
69 |
67 68
|
syl5ibrcom |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( 𝐹 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 } ) ) ) → 𝑥 ∈ 𝐹 ) ) |
70 |
63 69
|
syld |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) → 𝑥 ∈ 𝐹 ) ) |
71 |
70
|
impancom |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → ( ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) |
72 |
71
|
an32s |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) |
73 |
72
|
con3d |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) ) |
74 |
|
rexnal |
⊢ ( ∃ 𝑦 ∈ 𝐹 ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ ) |
75 |
|
nne |
⊢ ( ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑦 ∩ 𝑥 ) = ∅ ) |
76 |
|
filelss |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 ) |
77 |
|
reldisj |
⊢ ( 𝑦 ⊆ 𝑋 → ( ( 𝑦 ∩ 𝑥 ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) ) |
78 |
76 77
|
syl |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑦 ∩ 𝑥 ) = ∅ ↔ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) ) |
79 |
|
difss |
⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 |
80 |
|
filss |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ∧ 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) |
81 |
80
|
3exp2 |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) ) |
82 |
79 81
|
mpii |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) |
83 |
82
|
imp |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 ⊆ ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
84 |
78 83
|
sylbid |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑦 ∩ 𝑥 ) = ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
85 |
75 84
|
syl5bi |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → ( ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
86 |
85
|
rexlimdva |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐹 ¬ ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
87 |
74 86
|
syl5bir |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
88 |
87
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝐹 ( 𝑦 ∩ 𝑥 ) ≠ ∅ → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
89 |
73 88
|
syld |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
90 |
89
|
orrd |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
91 |
7 90
|
sylan2b |
⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
92 |
91
|
ralrimiva |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
93 |
|
isufil |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) |
94 |
6 92 93
|
sylanbrc |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) ) |
95 |
5 94
|
impbii |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 → 𝐹 = 𝑓 ) ) ) |