| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 2 | 1 | elintrab 4959 | . . . 4
⊢ (𝑥 ∈ ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)) | 
| 3 |  | filsspw 23860 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) | 
| 4 | 3 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝒫 𝑋) | 
| 5 |  | difss 4135 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 | 
| 6 |  | filtop 23864 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) | 
| 7 | 6 | difexd 5330 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ V) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ V) | 
| 9 |  | elpwg 4602 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) | 
| 11 | 5, 10 | mpbiri 258 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) | 
| 12 | 11 | snssd 4808 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋) | 
| 13 | 4, 12 | unssd 4191 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋) | 
| 14 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) | 
| 15 |  | filn0 23871 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) | 
| 16 |  | ssn0 4403 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) | 
| 17 | 14, 15, 16 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) | 
| 18 | 17 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) | 
| 19 |  | elsni 4642 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {(𝑋 ∖ 𝑥)} → 𝑧 = (𝑋 ∖ 𝑥)) | 
| 20 |  | filelss 23861 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) | 
| 21 | 20 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑦 ⊆ 𝑋) | 
| 22 |  | reldisj 4452 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ⊆ 𝑋 → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)))) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)))) | 
| 24 |  | dfss4 4268 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) | 
| 25 | 24 | biimpi 216 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ⊆ 𝑋 → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) | 
| 26 | 25 | sseq2d 4015 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ⊆ 𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥)) | 
| 27 | 26 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥)) | 
| 28 | 23, 27 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ 𝑥)) | 
| 29 |  | filss 23862 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹) | 
| 30 | 29 | 3exp2 1354 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) | 
| 31 | 30 | 3imp 1110 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) | 
| 32 | 28, 31 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ → 𝑥 ∈ 𝐹)) | 
| 33 | 32 | necon3bd 2953 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)) | 
| 34 | 33 | 3exp 1119 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)))) | 
| 35 | 34 | com24 95 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)))) | 
| 36 | 35 | 3imp1 1347 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅) | 
| 37 |  | ineq2 4213 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑋 ∖ 𝑥))) | 
| 38 | 37 | neeq1d 2999 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑋 ∖ 𝑥) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)) | 
| 39 | 36, 38 | syl5ibrcom 247 | . . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) ≠ ∅)) | 
| 40 | 39 | expimpd 453 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 = (𝑋 ∖ 𝑥)) → (𝑦 ∩ 𝑧) ≠ ∅)) | 
| 41 | 19, 40 | sylan2i 606 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {(𝑋 ∖ 𝑥)}) → (𝑦 ∩ 𝑧) ≠ ∅)) | 
| 42 | 41 | ralrimivv 3199 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅) | 
| 43 |  | filfbas 23857 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) | 
| 44 | 43 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑋)) | 
| 45 | 5 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ⊆ 𝑋) | 
| 46 | 25 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) | 
| 47 |  | difeq2 4119 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = (𝑋 ∖ ∅)) | 
| 48 |  | dif0 4377 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 ∖ ∅) = 𝑋 | 
| 49 | 47, 48 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋) | 
| 50 | 49 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋) | 
| 51 | 46, 50 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 = 𝑋) | 
| 52 | 6 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑋 ∈ 𝐹) | 
| 53 | 51, 52 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 ∈ 𝐹) | 
| 54 | 53 | 3expia 1121 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) = ∅ → 𝑥 ∈ 𝐹)) | 
| 55 | 54 | necon3bd 2953 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅)) | 
| 56 | 55 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))) | 
| 57 | 56 | com23 86 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑋 ∖ 𝑥) ≠ ∅))) | 
| 58 | 57 | 3imp 1110 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅) | 
| 59 | 6 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑋 ∈ 𝐹) | 
| 60 |  | snfbas 23875 | . . . . . . . . . . . . . . 15
⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) | 
| 61 | 45, 58, 59, 60 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) | 
| 62 |  | fbunfip 23878 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)) | 
| 63 | 44, 61, 62 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)) | 
| 64 | 42, 63 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 65 |  | fsubbas 23876 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) | 
| 66 | 6, 65 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) | 
| 67 | 66 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) | 
| 68 | 13, 18, 64, 67 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋)) | 
| 69 |  | fgcl 23887 | . . . . . . . . . . 11
⊢
((fi‘(𝐹 ∪
{(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋)) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋)) | 
| 71 |  | filssufil 23921 | . . . . . . . . . . 11
⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) | 
| 72 |  | snex 5435 | . . . . . . . . . . . . . . . . . . . . 21
⊢ {(𝑋 ∖ 𝑥)} ∈ V | 
| 73 |  | unexg 7764 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V) | 
| 74 | 72, 73 | mpan2 691 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V) | 
| 75 |  | ssfii 9460 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 76 | 74, 75 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 77 | 76 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 78 | 77 | unssad 4192 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 79 |  | ssfg 23881 | . . . . . . . . . . . . . . . . . 18
⊢
((fi‘(𝐹 ∪
{(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 80 | 68, 79 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 81 | 78, 80 | sstrd 3993 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 82 | 81 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 83 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) | 
| 84 | 82, 83 | sstrd 3993 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ 𝑓) | 
| 85 |  | ufilfil 23913 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋)) | 
| 86 |  | 0nelfil 23858 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝑓) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈
𝑓) | 
| 88 | 87 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓) | 
| 89 |  | disjdif 4471 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∩ (𝑋 ∖ 𝑥)) = ∅ | 
| 90 | 85 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑓 ∈ (Fil‘𝑋)) | 
| 91 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑥 ∈ 𝑓) | 
| 92 | 76 | unssbd 4193 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹 ∈ (Fil‘𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 93 | 92 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) | 
| 95 | 68 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋)) | 
| 96 | 95, 79 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 97 | 94, 96 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 98 | 97 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) | 
| 99 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) | 
| 100 | 98, 99 | sstrd 3993 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ 𝑓) | 
| 101 |  | snidg 4659 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) | 
| 102 | 7, 101 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) | 
| 103 | 102 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) | 
| 104 | 103 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) | 
| 105 | 100, 104 | sseldd 3983 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ 𝑓) | 
| 106 |  | filin 23863 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓 ∧ (𝑋 ∖ 𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓) | 
| 107 | 90, 91, 105, 106 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓) | 
| 108 | 89, 107 | eqeltrrid 2845 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → ∅ ∈ 𝑓) | 
| 109 | 108 | expr 456 | . . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑥 ∈ 𝑓 → ∅ ∈ 𝑓)) | 
| 110 | 88, 109 | mtod 198 | . . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ 𝑥 ∈ 𝑓) | 
| 111 | 84, 110 | jca 511 | . . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) | 
| 112 | 111 | exp31 419 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))) | 
| 113 | 112 | reximdvai 3164 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 114 | 71, 113 | syl5 34 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 115 | 70, 114 | mpd 15 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) | 
| 116 | 115 | 3expia 1121 | . . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 117 |  | filssufil 23921 | . . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | 
| 118 |  | filelss 23861 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) | 
| 119 | 118 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋)) | 
| 120 | 85, 119 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋)) | 
| 121 | 120 | con3d 152 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ¬ 𝑥 ∈ 𝑓)) | 
| 122 | 121 | impcom 407 | . . . . . . . . . . . . 13
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥 ∈ 𝑓) | 
| 123 | 122 | a1d 25 | . . . . . . . . . . . 12
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → ¬ 𝑥 ∈ 𝑓)) | 
| 124 | 123 | ancld 550 | . . . . . . . . . . 11
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 125 | 124 | reximdva 3167 | . . . . . . . . . 10
⊢ (¬
𝑥 ⊆ 𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 126 | 117, 125 | syl5com 31 | . . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 127 | 126 | adantr 480 | . . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 128 | 116, 127 | pm2.61d 179 | . . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) | 
| 129 | 128 | ex 412 | . . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) | 
| 130 |  | rexanali 3101 | . . . . . 6
⊢
(∃𝑓 ∈
(UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)) | 
| 131 | 129, 130 | imbitrdi 251 | . . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))) | 
| 132 | 131 | con4d 115 | . . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓) → 𝑥 ∈ 𝐹)) | 
| 133 | 2, 132 | biimtrid 242 | . . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} → 𝑥 ∈ 𝐹)) | 
| 134 | 133 | ssrdv 3988 | . 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} ⊆ 𝐹) | 
| 135 |  | ssintub 4965 | . . 3
⊢ 𝐹 ⊆ ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} | 
| 136 | 135 | a1i 11 | . 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓}) | 
| 137 | 134, 136 | eqssd 4000 | 1
⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} = 𝐹) |