Theorem fgcl 23821

Description: A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)

Assertion

Ref	Expression
fgcl	⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))

Proof of Theorem fgcl

Dummy variables 𝑣 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfg 23814	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧 ⊆ 𝑋 ∧ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)))
2		elfvex 6919	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V)
3		fbasne0 23773	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
4		n0 4333	. . . . . 6 ⊢ (𝐹 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐹)
5	3, 4	sylib 218	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦 ∈ 𝐹)
6		fbelss 23776	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
7	6	ex 412	. . . . . . 7 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋))
8	7	ancld 550	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
9	8	eximdv 1917	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦 ∈ 𝐹 → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
10	5, 9	mpd 15	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
11		df-rex 3062	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
12	10, 11	sylibr 234	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)
13		elfvdm 6918	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas)
14		sseq2 3990	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋))
15	14	rexbidv 3165	. . . . 5 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
16	15	sbcieg 3810	. . . 4 ⊢ (𝑋 ∈ dom fBas → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
17	13, 16	syl 17	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
18	12, 17	mpbird 257	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
19		0nelfb 23774	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐹)
20		0ex 5282	. . . . 5 ⊢ ∅ ∈ V
21		sseq2 3990	. . . . . 6 ⊢ (𝑧 = ∅ → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅))
22	21	rexbidv 3165	. . . . 5 ⊢ (𝑧 = ∅ → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅))
23	20, 22	sbcie 3812	. . . 4 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅)
24		ss0 4382	. . . . . . 7 ⊢ (𝑦 ⊆ ∅ → 𝑦 = ∅)
25	24	eleq1d 2820	. . . . . 6 ⊢ (𝑦 ⊆ ∅ → (𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹))
26	25	biimpac 478	. . . . 5 ⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅) → ∅ ∈ 𝐹)
27	26	rexlimiva 3134	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹)
28	23, 27	sylbi 217	. . 3 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹)
29	19, 28	nsyl 140	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
30		sstr 3972	. . . . . 6 ⊢ ((𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢) → 𝑦 ⊆ 𝑢)
31	30	expcom 413	. . . . 5 ⊢ (𝑣 ⊆ 𝑢 → (𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢))
32	31	reximdv 3156	. . . 4 ⊢ (𝑣 ⊆ 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
33	32	3ad2ant3 1135	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
34		vex 3468	. . . 4 ⊢ 𝑣 ∈ V
35		sseq2 3990	. . . . 5 ⊢ (𝑧 = 𝑣 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣))
36	35	rexbidv 3165	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣))
37	34, 36	sbcie 3812	. . 3 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣)
38		vex 3468	. . . 4 ⊢ 𝑢 ∈ V
39		sseq2 3990	. . . . 5 ⊢ (𝑧 = 𝑢 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢))
40	39	rexbidv 3165	. . . 4 ⊢ (𝑧 = 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
41	38, 40	sbcie 3812	. . 3 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)
42	33, 37, 41	3imtr4g 296	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
43		fbasssin 23779	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤))
44	43	3expib 1122	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤)))
45		sstr2 3970	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
46	45	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑦 ⊆ (𝑧 ∩ 𝑤) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
47	46	reximdv 3156	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
48		ss2in 4225	. . . . . . . . . . . 12 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
49	47, 48	syl11 33	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
50	44, 49	syl6 35	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
51	50	exp5c 444	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ 𝐹 → (𝑤 ∈ 𝐹 → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))))
52	51	imp31 417	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑤 ∈ 𝐹) → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
53	52	impancom 451	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (𝑤 ∈ 𝐹 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
54	53	rexlimdv 3140	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
55	54	rexlimdva2 3144	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
56	55	impd 410	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
57	56	3ad2ant1 1133	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
58		sseq1 3989	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢))
59	58	cbvrexvw 3225	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
60	41, 59	bitri 275	. . . 4 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
61		sseq1 3989	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣))
62	61	cbvrexvw 3225	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
63	37, 62	bitri 275	. . . 4 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
64	60, 63	anbi12i 628	. . 3 ⊢ (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) ↔ (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
65	38	inex1 5292	. . . 4 ⊢ (𝑢 ∩ 𝑣) ∈ V
66		sseq2 3990	. . . . 5 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑢 ∩ 𝑣)))
67	66	rexbidv 3165	. . . 4 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
68	65, 67	sbcie 3812	. . 3 ⊢ ([(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))
69	57, 64, 68	3imtr4g 296	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) → [(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
70	1, 2, 18, 29, 42, 69	isfild 23801	1 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2933  ∃wrex 3061  Vcvv 3464  [wsbc 3770   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  dom cdm 5659  ‘cfv 6536  (class class class)co 7410  fBascfbas 21308  filGencfg 21309  Filcfil 23788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-fbas 21317  df-fg 21318  df-fil 23789

This theorem is referenced by:  fgabs  23822  trfg  23834  isufil2  23851  ssufl  23861  ufileu  23862  filufint  23863  fixufil  23865  uffixfr  23866  fmfil  23887  fmfg  23892  elfm3  23893  rnelfm  23896  fmfnfmlem2  23898  fmfnfm  23901  fbflim  23919  hausflim  23924  flimclslem  23927  flffbas  23938  fclsbas  23964  fclsfnflim  23970  flimfnfcls  23971  fclscmp  23973  haustsms  24079  tsmscls  24081  tsmsmhm  24089  tsmsadd  24090  cfilufg  24236  metust  24502  fgcfil  25228  cmetcaulem  25245  cmetss  25273  minveclem4a  25387  minveclem4  25389