Step | Hyp | Ref
| Expression |
1 | | ufilfil 22655 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
2 | | ufilmax 22658 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑓) → 𝐹 = 𝑓) |
3 | 2 | 3expia 1122 |
. . . 4
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) |
4 | 3 | ralrimiva 3096 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) |
5 | 1, 4 | jca 515 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓))) |
6 | | simpl 486 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) → 𝐹 ∈ (Fil‘𝑋)) |
7 | | velpw 4493 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
8 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝐹 ∈ (Fil‘𝑋)) |
9 | | snex 5298 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥} ∈ V |
10 | | unexg 7490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥} ∈ V) → (𝐹 ∪ {𝑥}) ∈ V) |
11 | 8, 9, 10 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 ∪ {𝑥}) ∈ V) |
12 | | ssfii 8956 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∪ {𝑥}) ∈ V → (𝐹 ∪ {𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥}))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 ∪ {𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥}))) |
14 | | filsspw 22602 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝐹 ⊆ 𝒫 𝑋) |
16 | 7 | biimpri 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ⊆ 𝑋 → 𝑥 ∈ 𝒫 𝑋) |
17 | 16 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑥 ∈ 𝒫 𝑋) |
18 | 17 | snssd 4697 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → {𝑥} ⊆ 𝒫 𝑋) |
19 | 15, 18 | unssd 4076 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 ∪ {𝑥}) ⊆ 𝒫 𝑋) |
20 | | ssun2 4063 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥} ⊆ (𝐹 ∪ {𝑥}) |
21 | | vex 3402 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
22 | 21 | snnz 4667 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥} ≠ ∅ |
23 | | ssn0 4289 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑥} ⊆ (𝐹 ∪ {𝑥}) ∧ {𝑥} ≠ ∅) → (𝐹 ∪ {𝑥}) ≠ ∅) |
24 | 20, 22, 23 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∪ {𝑥}) ≠ ∅ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 ∪ {𝑥}) ≠ ∅) |
26 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) |
27 | | ineq2 4097 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑥 → (𝑦 ∩ 𝑓) = (𝑦 ∩ 𝑥)) |
28 | 27 | neeq1d 2993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑥 → ((𝑦 ∩ 𝑓) ≠ ∅ ↔ (𝑦 ∩ 𝑥) ≠ ∅)) |
29 | 21, 28 | ralsn 4572 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑓 ∈
{𝑥} (𝑦 ∩ 𝑓) ≠ ∅ ↔ (𝑦 ∩ 𝑥) ≠ ∅) |
30 | 29 | ralbii 3080 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑦 ∈
𝐹 ∀𝑓 ∈ {𝑥} (𝑦 ∩ 𝑓) ≠ ∅ ↔ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) |
31 | 26, 30 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → ∀𝑦 ∈ 𝐹 ∀𝑓 ∈ {𝑥} (𝑦 ∩ 𝑓) ≠ ∅) |
32 | | filfbas 22599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
33 | 32 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝐹 ∈ (fBas‘𝑋)) |
34 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑥 ⊆ 𝑋) |
35 | | inss2 4120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∩ 𝑥) ⊆ 𝑥 |
36 | | filtop 22606 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
37 | 36 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑋 ∈ 𝐹) |
38 | | ineq1 4096 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑋 → (𝑦 ∩ 𝑥) = (𝑋 ∩ 𝑥)) |
39 | 38 | neeq1d 2993 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑋 → ((𝑦 ∩ 𝑥) ≠ ∅ ↔ (𝑋 ∩ 𝑥) ≠ ∅)) |
40 | 39 | rspcva 3524 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑋 ∈ 𝐹 ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝑋 ∩ 𝑥) ≠ ∅) |
41 | 37, 40 | sylan 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝑋 ∩ 𝑥) ≠ ∅) |
42 | | ssn0 4289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑋 ∩ 𝑥) ⊆ 𝑥 ∧ (𝑋 ∩ 𝑥) ≠ ∅) → 𝑥 ≠ ∅) |
43 | 35, 41, 42 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑥 ≠ ∅) |
44 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑋 ∈ 𝐹) |
45 | | snfbas 22617 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {𝑥} ∈ (fBas‘𝑋)) |
46 | 34, 43, 44, 45 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → {𝑥} ∈ (fBas‘𝑋)) |
47 | | fbunfip 22620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑓 ∈ {𝑥} (𝑦 ∩ 𝑓) ≠ ∅)) |
48 | 33, 46, 47 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {𝑥})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑓 ∈ {𝑥} (𝑦 ∩ 𝑓) ≠ ∅)) |
49 | 31, 48 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → ¬ ∅ ∈
(fi‘(𝐹 ∪ {𝑥}))) |
50 | | fsubbas 22618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {𝑥}))))) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → ((fi‘(𝐹 ∪ {𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {𝑥}))))) |
52 | 19, 25, 49, 51 | mpbir3and 1343 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (fi‘(𝐹 ∪ {𝑥})) ∈ (fBas‘𝑋)) |
53 | | ssfg 22623 |
. . . . . . . . . . . . . . 15
⊢
((fi‘(𝐹 ∪
{𝑥})) ∈
(fBas‘𝑋) →
(fi‘(𝐹 ∪ {𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (fi‘(𝐹 ∪ {𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))) |
55 | 13, 54 | sstrd 3887 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 ∪ {𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))) |
56 | 55 | unssad 4077 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))) |
57 | | fgcl 22629 |
. . . . . . . . . . . . 13
⊢
((fi‘(𝐹 ∪
{𝑥})) ∈
(fBas‘𝑋) →
(𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) ∈ (Fil‘𝑋)) |
58 | | sseq2 3903 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → (𝐹 ⊆ 𝑓 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))))) |
59 | | eqeq2 2750 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → (𝐹 = 𝑓 ↔ 𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))))) |
60 | 58, 59 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → ((𝐹 ⊆ 𝑓 → 𝐹 = 𝑓) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → 𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))))) |
61 | 60 | rspcv 3521 |
. . . . . . . . . . . . 13
⊢ ((𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) ∈ (Fil‘𝑋) → (∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → 𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))))) |
62 | 52, 57, 61 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → 𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))))) |
63 | 56, 62 | mpid 44 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓) → 𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))))) |
64 | | vsnid 4553 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ {𝑥} |
65 | 20, 64 | sselii 3874 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ (𝐹 ∪ {𝑥}) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑥 ∈ (𝐹 ∪ {𝑥})) |
67 | 55, 66 | sseldd 3878 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → 𝑥 ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥})))) |
68 | | eleq2 2821 |
. . . . . . . . . . . 12
⊢ (𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → (𝑥 ∈ 𝐹 ↔ 𝑥 ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))))) |
69 | 67, 68 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (𝐹 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥}))) → 𝑥 ∈ 𝐹)) |
70 | 63, 69 | syld 47 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) → (∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓) → 𝑥 ∈ 𝐹)) |
71 | 70 | impancom 455 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) → (∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
72 | 71 | an32s 652 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ⊆ 𝑋) → (∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
73 | 72 | con3d 155 |
. . . . . . 7
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅)) |
74 | | rexnal 3151 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
𝐹 ¬ (𝑦 ∩ 𝑥) ≠ ∅ ↔ ¬ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅) |
75 | | nne 2938 |
. . . . . . . . . . 11
⊢ (¬
(𝑦 ∩ 𝑥) ≠ ∅ ↔ (𝑦 ∩ 𝑥) = ∅) |
76 | | filelss 22603 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) |
77 | | reldisj 4341 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ 𝑋 → ((𝑦 ∩ 𝑥) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ 𝑥))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → ((𝑦 ∩ 𝑥) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ 𝑥))) |
79 | | difss 4022 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 |
80 | | filss 22604 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ 𝑦 ⊆ (𝑋 ∖ 𝑥))) → (𝑋 ∖ 𝑥) ∈ 𝐹) |
81 | 80 | 3exp2 1355 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → ((𝑋 ∖ 𝑥) ⊆ 𝑋 → (𝑦 ⊆ (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑥) ∈ 𝐹)))) |
82 | 79, 81 | mpii 46 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ⊆ (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑥) ∈ 𝐹))) |
83 | 82 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑦 ⊆ (𝑋 ∖ 𝑥) → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
84 | 78, 83 | sylbid 243 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → ((𝑦 ∩ 𝑥) = ∅ → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
85 | 75, 84 | syl5bi 245 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → (¬ (𝑦 ∩ 𝑥) ≠ ∅ → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
86 | 85 | rexlimdva 3194 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑦 ∈ 𝐹 ¬ (𝑦 ∩ 𝑥) ≠ ∅ → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
87 | 74, 86 | syl5bir 246 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅ → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
88 | 87 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ⊆ 𝑋) → (¬ ∀𝑦 ∈ 𝐹 (𝑦 ∩ 𝑥) ≠ ∅ → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
89 | 73, 88 | syld 47 |
. . . . . 6
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐹)) |
90 | 89 | orrd 862 |
. . . . 5
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
91 | 7, 90 | sylan2b 597 |
. . . 4
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) ∧ 𝑥 ∈ 𝒫 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
92 | 91 | ralrimiva 3096 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) → ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
93 | | isufil 22654 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹))) |
94 | 6, 92, 93 | sylanbrc 586 |
. 2
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)) → 𝐹 ∈ (UFil‘𝑋)) |
95 | 5, 94 | impbii 212 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓))) |