fgcl

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

		Ref	Expression
	Assertion	fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$

Proof

Step	Hyp	Ref	Expression
1		elfg	$⊢ F \in fBas (X) \to (z \in (X filGen F) \leftrightarrow (z \subseteq X \land \exists y \in F y \subseteq z))$
2		elfvex	$⊢ F \in fBas (X) \to X \in V$
3		fbasne0	$⊢ F \in fBas (X) \to F \neq \emptyset$
4		n0	$⊢ F \neq \emptyset \leftrightarrow \exists y y \in F$
5	3 4	sylib	$⊢ F \in fBas (X) \to \exists y y \in F$
6		fbelss	$⊢ (F \in fBas (X) \land y \in F) \to y \subseteq X$
7	6	ex	$⊢ F \in fBas (X) \to (y \in F \to y \subseteq X)$
8	7	ancld	$⊢ F \in fBas (X) \to (y \in F \to (y \in F \land y \subseteq X))$
9	8	eximdv	$⊢ F \in fBas (X) \to (\exists y y \in F \to \exists y (y \in F \land y \subseteq X))$
10	5 9	mpd	$⊢ F \in fBas (X) \to \exists y (y \in F \land y \subseteq X)$
11		df-rex	$⊢ \exists y \in F y \subseteq X \leftrightarrow \exists y (y \in F \land y \subseteq X)$
12	10 11	sylibr	$⊢ F \in fBas (X) \to \exists y \in F y \subseteq X$
13		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
14		sseq2	$⊢ z = X \to (y \subseteq z \leftrightarrow y \subseteq X)$
15	14	rexbidv	$⊢ z = X \to (\exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq X)$
16	15	sbcieg	$⊢ X \in dom fBas \to (\underset{˙}{[} X / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq X)$
17	13 16	syl	$⊢ F \in fBas (X) \to (\underset{˙}{[} X / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq X)$
18	12 17	mpbird	$⊢ F \in fBas (X) \to \underset{˙}{[} X / z \underset{˙}{]} \exists y \in F y \subseteq z$
19		0nelfb	$⊢ F \in fBas (X) \to \neg \emptyset \in F$
20		0ex	$⊢ \emptyset \in V$
21		sseq2	$⊢ z = \emptyset \to (y \subseteq z \leftrightarrow y \subseteq \emptyset)$
22	21	rexbidv	$⊢ z = \emptyset \to (\exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq \emptyset)$
23	20 22	sbcie	$⊢ \underset{˙}{[} \emptyset / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq \emptyset$
24		ss0	$⊢ y \subseteq \emptyset \to y = \emptyset$
25	24	eleq1d	$⊢ y \subseteq \emptyset \to (y \in F \leftrightarrow \emptyset \in F)$
26	25	biimpac	$⊢ (y \in F \land y \subseteq \emptyset) \to \emptyset \in F$
27	26	rexlimiva	$⊢ \exists y \in F y \subseteq \emptyset \to \emptyset \in F$
28	23 27	sylbi	$⊢ \underset{˙}{[} \emptyset / z \underset{˙}{]} \exists y \in F y \subseteq z \to \emptyset \in F$
29	19 28	nsyl	$⊢ F \in fBas (X) \to \neg \underset{˙}{[} \emptyset / z \underset{˙}{]} \exists y \in F y \subseteq z$
30		sstr	$⊢ (y \subseteq v \land v \subseteq u) \to y \subseteq u$
31	30	expcom	$⊢ v \subseteq u \to (y \subseteq v \to y \subseteq u)$
32	31	reximdv	$⊢ v \subseteq u \to (\exists y \in F y \subseteq v \to \exists y \in F y \subseteq u)$
33	32	3ad2ant3	$⊢ (F \in fBas (X) \land u \subseteq X \land v \subseteq u) \to (\exists y \in F y \subseteq v \to \exists y \in F y \subseteq u)$
34		vex	$⊢ v \in V$
35		sseq2	$⊢ z = v \to (y \subseteq z \leftrightarrow y \subseteq v)$
36	35	rexbidv	$⊢ z = v \to (\exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq v)$
37	34 36	sbcie	$⊢ \underset{˙}{[} v / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq v$
38		vex	$⊢ u \in V$
39		sseq2	$⊢ z = u \to (y \subseteq z \leftrightarrow y \subseteq u)$
40	39	rexbidv	$⊢ z = u \to (\exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq u)$
41	38 40	sbcie	$⊢ \underset{˙}{[} u / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq u$
42	33 37 41	3imtr4g	$⊢ (F \in fBas (X) \land u \subseteq X \land v \subseteq u) \to (\underset{˙}{[} v / z \underset{˙}{]} \exists y \in F y \subseteq z \to \underset{˙}{[} u / z \underset{˙}{]} \exists y \in F y \subseteq z)$
43		fbasssin	$⊢ (F \in fBas (X) \land z \in F \land w \in F) \to \exists y \in F y \subseteq z \cap w$
44	43	3expib	$⊢ F \in fBas (X) \to ((z \in F \land w \in F) \to \exists y \in F y \subseteq z \cap w)$
45		sstr2	$⊢ y \subseteq z \cap w \to (z \cap w \subseteq u \cap v \to y \subseteq u \cap v)$
46	45	com12	$⊢ z \cap w \subseteq u \cap v \to (y \subseteq z \cap w \to y \subseteq u \cap v)$
47	46	reximdv	$⊢ z \cap w \subseteq u \cap v \to (\exists y \in F y \subseteq z \cap w \to \exists y \in F y \subseteq u \cap v)$
48		ss2in	$⊢ (z \subseteq u \land w \subseteq v) \to z \cap w \subseteq u \cap v$
49	47 48	syl11	$⊢ \exists y \in F y \subseteq z \cap w \to ((z \subseteq u \land w \subseteq v) \to \exists y \in F y \subseteq u \cap v)$
50	44 49	syl6	$⊢ F \in fBas (X) \to ((z \in F \land w \in F) \to ((z \subseteq u \land w \subseteq v) \to \exists y \in F y \subseteq u \cap v))$
51	50	exp5c	$⊢ F \in fBas (X) \to (z \in F \to (w \in F \to (z \subseteq u \to (w \subseteq v \to \exists y \in F y \subseteq u \cap v))))$
52	51	imp31	$⊢ ((F \in fBas (X) \land z \in F) \land w \in F) \to (z \subseteq u \to (w \subseteq v \to \exists y \in F y \subseteq u \cap v))$
53	52	impancom	$⊢ ((F \in fBas (X) \land z \in F) \land z \subseteq u) \to (w \in F \to (w \subseteq v \to \exists y \in F y \subseteq u \cap v))$
54	53	rexlimdv	$⊢ ((F \in fBas (X) \land z \in F) \land z \subseteq u) \to (\exists w \in F w \subseteq v \to \exists y \in F y \subseteq u \cap v)$
55	54	rexlimdva2	$⊢ F \in fBas (X) \to (\exists z \in F z \subseteq u \to (\exists w \in F w \subseteq v \to \exists y \in F y \subseteq u \cap v))$
56	55	impd	$⊢ F \in fBas (X) \to ((\exists z \in F z \subseteq u \land \exists w \in F w \subseteq v) \to \exists y \in F y \subseteq u \cap v)$
57	56	3ad2ant1	$⊢ (F \in fBas (X) \land u \subseteq X \land v \subseteq X) \to ((\exists z \in F z \subseteq u \land \exists w \in F w \subseteq v) \to \exists y \in F y \subseteq u \cap v)$
58		sseq1	$⊢ y = z \to (y \subseteq u \leftrightarrow z \subseteq u)$
59	58	cbvrexvw	$⊢ \exists y \in F y \subseteq u \leftrightarrow \exists z \in F z \subseteq u$
60	41 59	bitri	$⊢ \underset{˙}{[} u / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists z \in F z \subseteq u$
61		sseq1	$⊢ y = w \to (y \subseteq v \leftrightarrow w \subseteq v)$
62	61	cbvrexvw	$⊢ \exists y \in F y \subseteq v \leftrightarrow \exists w \in F w \subseteq v$
63	37 62	bitri	$⊢ \underset{˙}{[} v / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists w \in F w \subseteq v$
64	60 63	anbi12i	$⊢ (\underset{˙}{[} u / z \underset{˙}{]} \exists y \in F y \subseteq z \land \underset{˙}{[} v / z \underset{˙}{]} \exists y \in F y \subseteq z) \leftrightarrow (\exists z \in F z \subseteq u \land \exists w \in F w \subseteq v)$
65	38	inex1	$⊢ u \cap v \in V$
66		sseq2	$⊢ z = u \cap v \to (y \subseteq z \leftrightarrow y \subseteq u \cap v)$
67	66	rexbidv	$⊢ z = u \cap v \to (\exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq u \cap v)$
68	65 67	sbcie	$⊢ \underset{˙}{[} (u \cap v) / z \underset{˙}{]} \exists y \in F y \subseteq z \leftrightarrow \exists y \in F y \subseteq u \cap v$
69	57 64 68	3imtr4g	$⊢ (F \in fBas (X) \land u \subseteq X \land v \subseteq X) \to ((\underset{˙}{[} u / z \underset{˙}{]} \exists y \in F y \subseteq z \land \underset{˙}{[} v / z \underset{˙}{]} \exists y \in F y \subseteq z) \to \underset{˙}{[} (u \cap v) / z \underset{˙}{]} \exists y \in F y \subseteq z)$
70	1 2 18 29 42 69	isfild	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$

Metamath Proof Explorer

Theorem fgcl

Proof