![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > filtop | Structured version Visualization version GIF version |
Description: The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
Ref | Expression |
---|---|
filtop | ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | filfbas 23751 | . . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) | |
2 | fbasne0 23733 | . . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
4 | n0 4347 | . . 3 ⊢ (𝐹 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐹) | |
5 | filelss 23755 | . . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → 𝑥 ⊆ 𝑋) | |
6 | ssid 4002 | . . . . . . 7 ⊢ 𝑋 ⊆ 𝑋 | |
7 | filss 23756 | . . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ∈ 𝐹 ∧ 𝑋 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋)) → 𝑋 ∈ 𝐹) | |
8 | 7 | 3exp2 1352 | . . . . . . . 8 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐹 → (𝑋 ⊆ 𝑋 → (𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹)))) |
9 | 8 | imp 406 | . . . . . . 7 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → (𝑋 ⊆ 𝑋 → (𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹))) |
10 | 6, 9 | mpi 20 | . . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → (𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹)) |
11 | 5, 10 | mpd 15 | . . . . 5 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → 𝑋 ∈ 𝐹) |
12 | 11 | ex 412 | . . . 4 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐹 → 𝑋 ∈ 𝐹)) |
13 | 12 | exlimdv 1929 | . . 3 ⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑥 𝑥 ∈ 𝐹 → 𝑋 ∈ 𝐹)) |
14 | 4, 13 | biimtrid 241 | . 2 ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ≠ ∅ → 𝑋 ∈ 𝐹)) |
15 | 3, 14 | mpd 15 | 1 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1774 ∈ wcel 2099 ≠ wne 2937 ⊆ wss 3947 ∅c0 4323 ‘cfv 6548 fBascfbas 21266 Filcfil 23748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6500 df-fun 6550 df-fv 6556 df-fbas 21275 df-fil 23749 |
This theorem is referenced by: isfil2 23759 filn0 23765 infil 23766 filunibas 23784 filuni 23788 trfil1 23789 trfil2 23790 fgtr 23793 trfg 23794 isufil2 23811 filssufil 23815 ssufl 23821 ufileu 23822 filufint 23823 uffixfr 23826 cfinufil 23831 rnelfmlem 23855 rnelfm 23856 fmfnfmlem1 23857 fmfnfmlem2 23858 fmfnfmlem4 23860 fmfnfm 23861 flfval 23893 fclsfnflim 23930 flimfnfcls 23931 fcfval 23936 alexsublem 23947 metust 24466 cmetss 25243 minveclem4a 25357 filnetlem3 35864 filnetlem4 35865 |
Copyright terms: Public domain | W3C validator |