![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssfg | Structured version Visualization version GIF version |
Description: A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
Ref | Expression |
---|---|
ssfg | ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fbelss 22145 | . . . . 5 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑡 ∈ 𝐹) → 𝑡 ⊆ 𝑋) | |
2 | 1 | ex 405 | . . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ 𝐹 → 𝑡 ⊆ 𝑋)) |
3 | ssid 3880 | . . . . 5 ⊢ 𝑡 ⊆ 𝑡 | |
4 | sseq1 3883 | . . . . . 6 ⊢ (𝑥 = 𝑡 → (𝑥 ⊆ 𝑡 ↔ 𝑡 ⊆ 𝑡)) | |
5 | 4 | rspcev 3536 | . . . . 5 ⊢ ((𝑡 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑡) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡) |
6 | 3, 5 | mpan2 678 | . . . 4 ⊢ (𝑡 ∈ 𝐹 → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡) |
7 | 2, 6 | jca2 506 | . . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ 𝐹 → (𝑡 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡))) |
8 | elfg 22183 | . . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡))) | |
9 | 7, 8 | sylibrd 251 | . 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ 𝐹 → 𝑡 ∈ (𝑋filGen𝐹))) |
10 | 9 | ssrdv 3865 | 1 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 ∃wrex 3090 ⊆ wss 3830 ‘cfv 6188 (class class class)co 6976 fBascfbas 20235 filGencfg 20236 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fv 6196 df-ov 6979 df-oprab 6980 df-mpo 6981 df-fbas 20244 df-fg 20245 |
This theorem is referenced by: fgss2 22186 fgfil 22187 fgabs 22191 trfg 22203 isufil2 22220 ssufl 22230 ufileu 22231 filufint 22232 elfm2 22260 fmfnfmlem4 22269 fmfnfm 22270 fmco 22273 hausflim 22293 flimclslem 22296 flffbas 22307 fclsbas 22333 fclsfnflim 22339 flimfnfcls 22340 fclscmp 22342 isucn2 22591 cfilufg 22605 metust 22871 psmetutop 22880 fgcfil 23577 cmetss 23622 minveclem4a 23736 minveclem4 23738 fgmin 33236 |
Copyright terms: Public domain | W3C validator |