Step | Hyp | Ref
| Expression |
1 | | vex 3401 |
. . . . 5
⊢ 𝑥 ∈ V |
2 | 1 | elintrab 4722 |
. . . 4
⊢ (𝑥 ∈ ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)) |
3 | | filsspw 22063 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
4 | 3 | 3ad2ant1 1124 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
5 | | difss 3960 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∖ 𝑥) ⊆ 𝑋 |
6 | | filtop 22067 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
7 | | difexg 5045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ V) |
9 | 8 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ V) |
10 | | elpwg 4387 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∖ 𝑥) ∈ V → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑋)) |
12 | 5, 11 | mpbiri 250 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ 𝒫 𝑋) |
13 | 12 | snssd 4571 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ 𝒫 𝑋) |
14 | 4, 13 | unssd 4012 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋) |
15 | | ssun1 3999 |
. . . . . . . . . . . . . 14
⊢ 𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) |
16 | | filn0 22074 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
17 | | ssn0 4202 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ⊆ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) |
18 | 15, 16, 17 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) |
19 | 18 | 3ad2ant1 1124 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅) |
20 | | elsni 4415 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {(𝑋 ∖ 𝑥)} → 𝑧 = (𝑋 ∖ 𝑥)) |
21 | | filelss 22064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) |
22 | 21 | 3adant3 1123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑦 ⊆ 𝑋) |
23 | | reldisj 4245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ⊆ 𝑋 → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)))) |
25 | | dfss4 4085 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
26 | 25 | biimpi 208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ⊆ 𝑋 → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
27 | 26 | sseq2d 3852 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ⊆ 𝑋 → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥)) |
28 | 27 | 3ad2ant3 1126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ (𝑋 ∖ (𝑋 ∖ 𝑥)) ↔ 𝑦 ⊆ 𝑥)) |
29 | 24, 28 | bitrd 271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ ↔ 𝑦 ⊆ 𝑥)) |
30 | | filss 22065 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹) |
31 | 30 | 3exp2 1416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
32 | 31 | 3imp 1098 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
33 | 29, 32 | sylbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∩ (𝑋 ∖ 𝑥)) = ∅ → 𝑥 ∈ 𝐹)) |
34 | 33 | necon3bd 2983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)) |
35 | 34 | 3exp 1109 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)))) |
36 | 35 | com24 95 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)))) |
37 | 36 | 3imp1 1409 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅) |
38 | | ineq2 4031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) = (𝑦 ∩ (𝑋 ∖ 𝑥))) |
39 | 38 | neeq1d 3028 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑋 ∖ 𝑥) → ((𝑦 ∩ 𝑧) ≠ ∅ ↔ (𝑦 ∩ (𝑋 ∖ 𝑥)) ≠ ∅)) |
40 | 37, 39 | syl5ibrcom 239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ∈ 𝐹) → (𝑧 = (𝑋 ∖ 𝑥) → (𝑦 ∩ 𝑧) ≠ ∅)) |
41 | 40 | expimpd 447 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 = (𝑋 ∖ 𝑥)) → (𝑦 ∩ 𝑧) ≠ ∅)) |
42 | 20, 41 | sylan2i 599 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ∈ 𝐹 ∧ 𝑧 ∈ {(𝑋 ∖ 𝑥)}) → (𝑦 ∩ 𝑧) ≠ ∅)) |
43 | 42 | ralrimivv 3152 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅) |
44 | | filfbas 22060 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
45 | 44 | 3ad2ant1 1124 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
46 | 5 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ⊆ 𝑋) |
47 | 26 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑥) |
48 | | difeq2 3945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = (𝑋 ∖ ∅)) |
49 | | dif0 4181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 ∖ ∅) = 𝑋 |
50 | 48, 49 | syl6eq 2830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∖ 𝑥) = ∅ → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋) |
51 | 50 | 3ad2ant3 1126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → (𝑋 ∖ (𝑋 ∖ 𝑥)) = 𝑋) |
52 | 47, 51 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 = 𝑋) |
53 | 6 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑋 ∈ 𝐹) |
54 | 52, 53 | eqeltrd 2859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) = ∅) → 𝑥 ∈ 𝐹) |
55 | 54 | 3expia 1111 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) = ∅ → 𝑥 ∈ 𝐹)) |
56 | 55 | necon3bd 2983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅)) |
57 | 56 | ex 403 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (¬ 𝑥 ∈ 𝐹 → (𝑋 ∖ 𝑥) ≠ ∅))) |
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑋 ∖ 𝑥) ≠ ∅))) |
59 | 58 | 3imp 1098 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅) |
60 | 6 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝑋 ∈ 𝐹) |
61 | | snfbas 22078 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅ ∧ 𝑋 ∈ 𝐹) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) |
62 | 46, 59, 60, 61 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) |
63 | | fbunfip 22081 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ (fBas‘𝑋)) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)) |
64 | 45, 62, 63 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ↔ ∀𝑦 ∈ 𝐹 ∀𝑧 ∈ {(𝑋 ∖ 𝑥)} (𝑦 ∩ 𝑧) ≠ ∅)) |
65 | 43, 64 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
66 | | fsubbas 22079 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) |
67 | 6, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) |
68 | 67 | 3ad2ant1 1124 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))))) |
69 | 14, 19, 65, 68 | mpbir3and 1399 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋)) |
70 | | fgcl 22090 |
. . . . . . . . . . 11
⊢
((fi‘(𝐹 ∪
{(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋)) |
72 | | filssufil 22124 |
. . . . . . . . . . 11
⊢ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) |
73 | | snex 5140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {(𝑋 ∖ 𝑥)} ∈ V |
74 | | unexg 7236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ {(𝑋 ∖ 𝑥)} ∈ V) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V) |
75 | 73, 74 | mpan2 681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V) |
76 | | ssfii 8613 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∪ {(𝑋 ∖ 𝑥)}) ∈ V → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
78 | 77 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝐹 ∪ {(𝑋 ∖ 𝑥)}) ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
79 | 78 | unssad 4013 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
80 | | ssfg 22084 |
. . . . . . . . . . . . . . . . . 18
⊢
((fi‘(𝐹 ∪
{(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
81 | 69, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
82 | 79, 81 | sstrd 3831 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
83 | 82 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
84 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) |
85 | 83, 84 | sstrd 3831 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → 𝐹 ⊆ 𝑓) |
86 | | ufilfil 22116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (UFil‘𝑋) → 𝑓 ∈ (Fil‘𝑋)) |
87 | | 0nelfil 22061 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝑓) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (UFil‘𝑋) → ¬ ∅ ∈
𝑓) |
89 | 88 | ad2antlr 717 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ ∅ ∈ 𝑓) |
90 | | disjdif 4264 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∩ (𝑋 ∖ 𝑥)) = ∅ |
91 | 86 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑓 ∈ (Fil‘𝑋)) |
92 | | simprr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → 𝑥 ∈ 𝑓) |
93 | 77 | unssbd 4014 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹 ∈ (Fil‘𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
94 | 93 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
95 | 94 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) |
96 | 69 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ∈ (fBas‘𝑋)) |
97 | 96, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → (fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
98 | 95, 97 | sstrd 3831 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
99 | 98 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)})))) |
100 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) |
101 | 99, 100 | sstrd 3831 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → {(𝑋 ∖ 𝑥)} ⊆ 𝑓) |
102 | | snidg 4428 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑋 ∖ 𝑥) ∈ V → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) |
103 | 8, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) |
104 | 103 | 3ad2ant1 1124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) |
105 | 104 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ {(𝑋 ∖ 𝑥)}) |
106 | 101, 105 | sseldd 3822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑋 ∖ 𝑥) ∈ 𝑓) |
107 | | filin 22066 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓 ∧ (𝑋 ∖ 𝑥) ∈ 𝑓) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓) |
108 | 91, 92, 106, 107 | syl3anc 1439 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → (𝑥 ∩ (𝑋 ∖ 𝑥)) ∈ 𝑓) |
109 | 90, 108 | syl5eqelr 2864 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 ∧ 𝑥 ∈ 𝑓)) → ∅ ∈ 𝑓) |
110 | 109 | expr 450 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝑥 ∈ 𝑓 → ∅ ∈ 𝑓)) |
111 | 89, 110 | mtod 190 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → ¬ 𝑥 ∈ 𝑓) |
112 | 85, 111 | jca 507 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) ∧ 𝑓 ∈ (UFil‘𝑋)) ∧ (𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓) → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) |
113 | 112 | exp31 412 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (𝑓 ∈ (UFil‘𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)))) |
114 | 113 | reximdvai 3196 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → (∃𝑓 ∈ (UFil‘𝑋)(𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
115 | 72, 114 | syl5 34 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ((𝑋filGen(fi‘(𝐹 ∪ {(𝑋 ∖ 𝑥)}))) ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
116 | 71, 115 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) |
117 | 116 | 3expia 1111 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
118 | | filssufil 22124 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) |
119 | | filelss 22064 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝑓) → 𝑥 ⊆ 𝑋) |
120 | 119 | ex 403 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋)) |
121 | 86, 120 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝑓 → 𝑥 ⊆ 𝑋)) |
122 | 121 | con3d 150 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (UFil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ¬ 𝑥 ∈ 𝑓)) |
123 | 122 | impcom 398 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → ¬ 𝑥 ∈ 𝑓) |
124 | 123 | a1d 25 |
. . . . . . . . . . . 12
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → ¬ 𝑥 ∈ 𝑓)) |
125 | 124 | ancld 546 |
. . . . . . . . . . 11
⊢ ((¬
𝑥 ⊆ 𝑋 ∧ 𝑓 ∈ (UFil‘𝑋)) → (𝐹 ⊆ 𝑓 → (𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
126 | 125 | reximdva 3198 |
. . . . . . . . . 10
⊢ (¬
𝑥 ⊆ 𝑋 → (∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
127 | 118, 126 | syl5com 31 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
128 | 127 | adantr 474 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → (¬ 𝑥 ⊆ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
129 | 117, 128 | pm2.61d 172 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ¬ 𝑥 ∈ 𝐹) → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓)) |
130 | 129 | ex 403 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ∃𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓))) |
131 | | rexanali 3179 |
. . . . . 6
⊢
(∃𝑓 ∈
(UFil‘𝑋)(𝐹 ⊆ 𝑓 ∧ ¬ 𝑥 ∈ 𝑓) ↔ ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓)) |
132 | 130, 131 | syl6ib 243 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (¬ 𝑥 ∈ 𝐹 → ¬ ∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓))) |
133 | 132 | con4d 115 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (∀𝑓 ∈ (UFil‘𝑋)(𝐹 ⊆ 𝑓 → 𝑥 ∈ 𝑓) → 𝑥 ∈ 𝐹)) |
134 | 2, 133 | syl5bi 234 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} → 𝑥 ∈ 𝐹)) |
135 | 134 | ssrdv 3827 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} ⊆ 𝐹) |
136 | | ssintub 4728 |
. . 3
⊢ 𝐹 ⊆ ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} |
137 | 136 | a1i 11 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓}) |
138 | 135, 137 | eqssd 3838 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓
∈ (UFil‘𝑋)
∣ 𝐹 ⊆ 𝑓} = 𝐹) |