Theorem fgcl 22937

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 22930	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧 ⊆ 𝑋 ∧ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)))
2		elfvex 6789	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V)
3		fbasne0 22889	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
4		n0 4277	. . . . . 6 ⊢ (𝐹 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐹)
5	3, 4	sylib 217	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦 ∈ 𝐹)
6		fbelss 22892	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
7	6	ex 412	. . . . . . 7 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋))
8	7	ancld 550	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
9	8	eximdv 1921	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦 ∈ 𝐹 → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
10	5, 9	mpd 15	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
11		df-rex 3069	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
12	10, 11	sylibr 233	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)
13		elfvdm 6788	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas)
14		sseq2 3943	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋))
15	14	rexbidv 3225	. . . . 5 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
16	15	sbcieg 3751	. . . 4 ⊢ (𝑋 ∈ dom fBas → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
17	13, 16	syl 17	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
18	12, 17	mpbird 256	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
19		0nelfb 22890	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐹)
20		0ex 5226	. . . . 5 ⊢ ∅ ∈ V
21		sseq2 3943	. . . . . 6 ⊢ (𝑧 = ∅ → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅))
22	21	rexbidv 3225	. . . . 5 ⊢ (𝑧 = ∅ → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅))
23	20, 22	sbcie 3754	. . . 4 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅)
24		ss0 4329	. . . . . . 7 ⊢ (𝑦 ⊆ ∅ → 𝑦 = ∅)
25	24	eleq1d 2823	. . . . . 6 ⊢ (𝑦 ⊆ ∅ → (𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹))
26	25	biimpac 478	. . . . 5 ⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅) → ∅ ∈ 𝐹)
27	26	rexlimiva 3209	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹)
28	23, 27	sylbi 216	. . 3 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹)
29	19, 28	nsyl 140	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
30		sstr 3925	. . . . . 6 ⊢ ((𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢) → 𝑦 ⊆ 𝑢)
31	30	expcom 413	. . . . 5 ⊢ (𝑣 ⊆ 𝑢 → (𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢))
32	31	reximdv 3201	. . . 4 ⊢ (𝑣 ⊆ 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
33	32	3ad2ant3 1133	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
34		vex 3426	. . . 4 ⊢ 𝑣 ∈ V
35		sseq2 3943	. . . . 5 ⊢ (𝑧 = 𝑣 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣))
36	35	rexbidv 3225	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣))
37	34, 36	sbcie 3754	. . 3 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣)
38		vex 3426	. . . 4 ⊢ 𝑢 ∈ V
39		sseq2 3943	. . . . 5 ⊢ (𝑧 = 𝑢 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢))
40	39	rexbidv 3225	. . . 4 ⊢ (𝑧 = 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
41	38, 40	sbcie 3754	. . 3 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)
42	33, 37, 41	3imtr4g 295	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
43		fbasssin 22895	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤))
44	43	3expib 1120	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤)))
45		sstr2 3924	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
46	45	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑦 ⊆ (𝑧 ∩ 𝑤) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
47	46	reximdv 3201	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
48		ss2in 4167	. . . . . . . . . . . 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 3211	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
55	54	rexlimdva2 3215	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
56	55	impd 410	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
57	56	3ad2ant1 1131	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
58		sseq1 3942	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢))
59	58	cbvrexvw 3373	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
60	41, 59	bitri 274	. . . 4 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
61		sseq1 3942	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣))
62	61	cbvrexvw 3373	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
63	37, 62	bitri 274	. . . 4 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
64	60, 63	anbi12i 626	. . 3 ⊢ (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) ↔ (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
65	38	inex1 5236	. . . 4 ⊢ (𝑢 ∩ 𝑣) ∈ V
66		sseq2 3943	. . . . 5 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑢 ∩ 𝑣)))
67	66	rexbidv 3225	. . . 4 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
68	65, 67	sbcie 3754	. . 3 ⊢ ([(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))
69	57, 64, 68	3imtr4g 295	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) → [(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
70	1, 2, 18, 29, 42, 69	isfild 22917	1 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  Vcvv 3422  [wsbc 3711   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  dom cdm 5580  ‘cfv 6418  (class class class)co 7255  fBascfbas 20498  filGencfg 20499  Filcfil 22904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-fbas 20507  df-fg 20508  df-fil 22905

This theorem is referenced by:  fgabs  22938  trfg  22950  isufil2  22967  ssufl  22977  ufileu  22978  filufint  22979  fixufil  22981  uffixfr  22982  fmfil  23003  fmfg  23008  elfm3  23009  rnelfm  23012  fmfnfmlem2  23014  fmfnfm  23017  fbflim  23035  hausflim  23040  flimclslem  23043  flffbas  23054  fclsbas  23080  fclsfnflim  23086  flimfnfcls  23087  fclscmp  23089  haustsms  23195  tsmscls  23197  tsmsmhm  23205  tsmsadd  23206  cfilufg  23353  metust  23620  fgcfil  24340  cmetcaulem  24357  cmetss  24385  minveclem4a  24499  minveclem4  24501