Theorem fgcl 23389

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 23382	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧 ⊆ 𝑋 ∧ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)))
2		elfvex 6929	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V)
3		fbasne0 23341	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅)
4		n0 4346	. . . . . 6 ⊢ (𝐹 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐹)
5	3, 4	sylib 217	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦 ∈ 𝐹)
6		fbelss 23344	. . . . . . . 8 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋)
7	6	ex 413	. . . . . . 7 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋))
8	7	ancld 551	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
9	8	eximdv 1920	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦 ∈ 𝐹 → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)))
10	5, 9	mpd 15	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
11		df-rex 3071	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))
12	10, 11	sylibr 233	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)
13		elfvdm 6928	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas)
14		sseq2 4008	. . . . . 6 ⊢ (𝑧 = 𝑋 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋))
15	14	rexbidv 3178	. . . . 5 ⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
16	15	sbcieg 3817	. . . 4 ⊢ (𝑋 ∈ dom fBas → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
17	13, 16	syl 17	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋))
18	12, 17	mpbird 256	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
19		0nelfb 23342	. . 3 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ 𝐹)
20		0ex 5307	. . . . 5 ⊢ ∅ ∈ V
21		sseq2 4008	. . . . . 6 ⊢ (𝑧 = ∅ → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅))
22	21	rexbidv 3178	. . . . 5 ⊢ (𝑧 = ∅ → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅))
23	20, 22	sbcie 3820	. . . 4 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅)
24		ss0 4398	. . . . . . 7 ⊢ (𝑦 ⊆ ∅ → 𝑦 = ∅)
25	24	eleq1d 2818	. . . . . 6 ⊢ (𝑦 ⊆ ∅ → (𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹))
26	25	biimpac 479	. . . . 5 ⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅) → ∅ ∈ 𝐹)
27	26	rexlimiva 3147	. . . 4 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹)
28	23, 27	sylbi 216	. . 3 ⊢ ([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹)
29	19, 28	nsyl 140	. 2 ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)
30		sstr 3990	. . . . . 6 ⊢ ((𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢) → 𝑦 ⊆ 𝑢)
31	30	expcom 414	. . . . 5 ⊢ (𝑣 ⊆ 𝑢 → (𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢))
32	31	reximdv 3170	. . . 4 ⊢ (𝑣 ⊆ 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
33	32	3ad2ant3 1135	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
34		vex 3478	. . . 4 ⊢ 𝑣 ∈ V
35		sseq2 4008	. . . . 5 ⊢ (𝑧 = 𝑣 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣))
36	35	rexbidv 3178	. . . 4 ⊢ (𝑧 = 𝑣 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣))
37	34, 36	sbcie 3820	. . 3 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣)
38		vex 3478	. . . 4 ⊢ 𝑢 ∈ V
39		sseq2 4008	. . . . 5 ⊢ (𝑧 = 𝑢 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢))
40	39	rexbidv 3178	. . . 4 ⊢ (𝑧 = 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢))
41	38, 40	sbcie 3820	. . 3 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)
42	33, 37, 41	3imtr4g 295	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
43		fbasssin 23347	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤))
44	43	3expib 1122	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤)))
45		sstr2 3989	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
46	45	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑦 ⊆ (𝑧 ∩ 𝑤) → 𝑦 ⊆ (𝑢 ∩ 𝑣)))
47	46	reximdv 3170	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
48		ss2in 4236	. . . . . . . . . . . 12 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
49	47, 48	syl11 33	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
50	44, 49	syl6 35	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
51	50	exp5c 445	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ 𝐹 → (𝑤 ∈ 𝐹 → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))))
52	51	imp31 418	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑤 ∈ 𝐹) → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
53	52	impancom 452	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (𝑤 ∈ 𝐹 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
54	53	rexlimdv 3153	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
55	54	rexlimdva2 3157	. . . . 5 ⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))))
56	55	impd 411	. . . 4 ⊢ (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
57	56	3ad2ant1 1133	. . 3 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
58		sseq1 4007	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢))
59	58	cbvrexvw 3235	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
60	41, 59	bitri 274	. . . 4 ⊢ ([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢)
61		sseq1 4007	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣))
62	61	cbvrexvw 3235	. . . . 5 ⊢ (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
63	37, 62	bitri 274	. . . 4 ⊢ ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)
64	60, 63	anbi12i 627	. . 3 ⊢ (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) ↔ (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣))
65	38	inex1 5317	. . . 4 ⊢ (𝑢 ∩ 𝑣) ∈ V
66		sseq2 4008	. . . . 5 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑢 ∩ 𝑣)))
67	66	rexbidv 3178	. . . 4 ⊢ (𝑧 = (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))
68	65, 67	sbcie 3820	. . 3 ⊢ ([(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))
69	57, 64, 68	3imtr4g 295	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) → [(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))
70	1, 2, 18, 29, 42, 69	isfild 23369	1 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2940  ∃wrex 3070  Vcvv 3474  [wsbc 3777   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  dom cdm 5676  ‘cfv 6543  (class class class)co 7411  fBascfbas 20938  filGencfg 20939  Filcfil 23356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-fbas 20947  df-fg 20948  df-fil 23357

This theorem is referenced by:  fgabs  23390  trfg  23402  isufil2  23419  ssufl  23429  ufileu  23430  filufint  23431  fixufil  23433  uffixfr  23434  fmfil  23455  fmfg  23460  elfm3  23461  rnelfm  23464  fmfnfmlem2  23466  fmfnfm  23469  fbflim  23487  hausflim  23492  flimclslem  23495  flffbas  23506  fclsbas  23532  fclsfnflim  23538  flimfnfcls  23539  fclscmp  23541  haustsms  23647  tsmscls  23649  tsmsmhm  23657  tsmsadd  23658  cfilufg  23805  metust  24074  fgcfil  24795  cmetcaulem  24812  cmetss  24840  minveclem4a  24954  minveclem4  24956