Theorem ssfg 22184

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.)

Assertion

Ref	Expression
ssfg	⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))

Proof of Theorem ssfg

Dummy variables 𝑥 𝑡 are mutually distinct and distinct from all other variables.

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𝐹))

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