infil

Description: The intersection of two filters is a filter. Use fiint to extend this property to the intersection of a finite set of filters. Paragraph 3 of BourbakiTop1 p. I.36. (Contributed by FL, 17-Sep-2007) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	infil	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to F \cap G \in Fil (X)$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ F \cap G \subseteq F$
2		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
3	2	adantr	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to F \subseteq 𝒫 X$
4	1 3	sstrid	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to F \cap G \subseteq 𝒫 X$
5		0nelfil	$⊢ F \in Fil (X) \to \neg \emptyset \in F$
6	5	adantr	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to \neg \emptyset \in F$
7		elinel1	$⊢ \emptyset \in (F \cap G) \to \emptyset \in F$
8	6 7	nsyl	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to \neg \emptyset \in (F \cap G)$
9		filtop	$⊢ F \in Fil (X) \to X \in F$
10	9	adantr	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to X \in F$
11		filtop	$⊢ G \in Fil (X) \to X \in G$
12	11	adantl	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to X \in G$
13	10 12	elind	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to X \in (F \cap G)$
14	4 8 13	3jca	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to (F \cap G \subseteq 𝒫 X \land \neg \emptyset \in (F \cap G) \land X \in (F \cap G))$
15		simpll	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to F \in Fil (X)$
16		simpr2	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to y \in (F \cap G)$
17		elinel1	$⊢ y \in (F \cap G) \to y \in F$
18	16 17	syl	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to y \in F$
19		simpr1	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to x \in 𝒫 X$
20	19	elpwid	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to x \subseteq X$
21		simpr3	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to y \subseteq x$
22		filss	$⊢ (F \in Fil (X) \land (y \in F \land x \subseteq X \land y \subseteq x)) \to x \in F$
23	15 18 20 21 22	syl13anc	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to x \in F$
24		simplr	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to G \in Fil (X)$
25		elinel2	$⊢ y \in (F \cap G) \to y \in G$
26	16 25	syl	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to y \in G$
27		filss	$⊢ (G \in Fil (X) \land (y \in G \land x \subseteq X \land y \subseteq x)) \to x \in G$
28	24 26 20 21 27	syl13anc	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to x \in G$
29	23 28	elind	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in 𝒫 X \land y \in (F \cap G) \land y \subseteq x)) \to x \in (F \cap G)$
30	29	3exp2	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to (x \in 𝒫 X \to (y \in (F \cap G) \to (y \subseteq x \to x \in (F \cap G))))$
31	30	imp	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land x \in 𝒫 X) \to (y \in (F \cap G) \to (y \subseteq x \to x \in (F \cap G)))$
32	31	rexlimdv	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land x \in 𝒫 X) \to (\exists y \in (F \cap G) y \subseteq x \to x \in (F \cap G))$
33	32	ralrimiva	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to \forall x \in 𝒫 X (\exists y \in (F \cap G) y \subseteq x \to x \in (F \cap G))$
34		simpl	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to F \in Fil (X)$
35		elinel1	$⊢ x \in (F \cap G) \to x \in F$
36	35 17	anim12i	$⊢ (x \in (F \cap G) \land y \in (F \cap G)) \to (x \in F \land y \in F)$
37		filin	$⊢ (F \in Fil (X) \land x \in F \land y \in F) \to x \cap y \in F$
38	37	3expb	$⊢ (F \in Fil (X) \land (x \in F \land y \in F)) \to x \cap y \in F$
39	34 36 38	syl2an	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in (F \cap G) \land y \in (F \cap G))) \to x \cap y \in F$
40		simpr	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to G \in Fil (X)$
41		elinel2	$⊢ x \in (F \cap G) \to x \in G$
42	41 25	anim12i	$⊢ (x \in (F \cap G) \land y \in (F \cap G)) \to (x \in G \land y \in G)$
43		filin	$⊢ (G \in Fil (X) \land x \in G \land y \in G) \to x \cap y \in G$
44	43	3expb	$⊢ (G \in Fil (X) \land (x \in G \land y \in G)) \to x \cap y \in G$
45	40 42 44	syl2an	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in (F \cap G) \land y \in (F \cap G))) \to x \cap y \in G$
46	39 45	elind	$⊢ ((F \in Fil (X) \land G \in Fil (X)) \land (x \in (F \cap G) \land y \in (F \cap G))) \to x \cap y \in (F \cap G)$
47	46	ralrimivva	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to \forall x \in (F \cap G) \forall y \in (F \cap G) x \cap y \in (F \cap G)$
48		isfil2	$⊢ F \cap G \in Fil (X) \leftrightarrow ((F \cap G \subseteq 𝒫 X \land \neg \emptyset \in (F \cap G) \land X \in (F \cap G)) \land \forall x \in 𝒫 X (\exists y \in (F \cap G) y \subseteq x \to x \in (F \cap G)) \land \forall x \in (F \cap G) \forall y \in (F \cap G) x \cap y \in (F \cap G))$
49	14 33 47 48	syl3anbrc	$⊢ (F \in Fil (X) \land G \in Fil (X)) \to F \cap G \in Fil (X)$

Metamath Proof Explorer

Theorem infil

Proof