isfil2

Description: Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	isfil2	$⊢ F \in Fil (X) \leftrightarrow ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F)$

Proof

Step	Hyp	Ref	Expression
1		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
2		0nelfil	$⊢ F \in Fil (X) \to \neg \emptyset \in F$
3		filtop	$⊢ F \in Fil (X) \to X \in F$
4	1 2 3	3jca	$⊢ F \in Fil (X) \to (F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F)$
5		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
6		filss	$⊢ (F \in Fil (X) \land (y \in F \land x \subseteq X \land y \subseteq x)) \to x \in F$
7	6	3exp2	$⊢ F \in Fil (X) \to (y \in F \to (x \subseteq X \to (y \subseteq x \to x \in F)))$
8	7	com23	$⊢ F \in Fil (X) \to (x \subseteq X \to (y \in F \to (y \subseteq x \to x \in F)))$
9	8	imp	$⊢ (F \in Fil (X) \land x \subseteq X) \to (y \in F \to (y \subseteq x \to x \in F))$
10	9	rexlimdv	$⊢ (F \in Fil (X) \land x \subseteq X) \to (\exists y \in F y \subseteq x \to x \in F)$
11	5 10	sylan2	$⊢ (F \in Fil (X) \land x \in 𝒫 X) \to (\exists y \in F y \subseteq x \to x \in F)$
12	11	ralrimiva	$⊢ F \in Fil (X) \to \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F)$
13		filin	$⊢ (F \in Fil (X) \land x \in F \land y \in F) \to x \cap y \in F$
14	13	3expb	$⊢ (F \in Fil (X) \land (x \in F \land y \in F)) \to x \cap y \in F$
15	14	ralrimivva	$⊢ F \in Fil (X) \to \forall x \in F \forall y \in F x \cap y \in F$
16	4 12 15	3jca	$⊢ F \in Fil (X) \to ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F)$
17		simp11	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to F \subseteq 𝒫 X$
18		simp13	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to X \in F$
19	18	ne0d	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to F \neq \emptyset$
20		simp12	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to \neg \emptyset \in F$
21		df-nel	$⊢ \emptyset \notin F \leftrightarrow \neg \emptyset \in F$
22	20 21	sylibr	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to \emptyset \notin F$
23		ssid	$⊢ x \cap y \subseteq x \cap y$
24		sseq1	$⊢ z = x \cap y \to (z \subseteq x \cap y \leftrightarrow x \cap y \subseteq x \cap y)$
25	24	rspcev	$⊢ (x \cap y \in F \land x \cap y \subseteq x \cap y) \to \exists z \in F z \subseteq x \cap y$
26	23 25	mpan2	$⊢ x \cap y \in F \to \exists z \in F z \subseteq x \cap y$
27	26	ralimi	$⊢ \forall y \in F x \cap y \in F \to \forall y \in F \exists z \in F z \subseteq x \cap y$
28	27	ralimi	$⊢ \forall x \in F \forall y \in F x \cap y \in F \to \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y$
29	28	3ad2ant3	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y$
30	19 22 29	3jca	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)$
31		isfbas2	$⊢ X \in F \to (F \in fBas (X) \leftrightarrow (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)))$
32	18 31	syl	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to (F \in fBas (X) \leftrightarrow (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)))$
33	17 30 32	mpbir2and	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to F \in fBas (X)$
34		n0	$⊢ F \cap 𝒫 x \neq \emptyset \leftrightarrow \exists y y \in (F \cap 𝒫 x)$
35		elin	$⊢ y \in (F \cap 𝒫 x) \leftrightarrow (y \in F \land y \in 𝒫 x)$
36		elpwi	$⊢ y \in 𝒫 x \to y \subseteq x$
37	36	anim2i	$⊢ (y \in F \land y \in 𝒫 x) \to (y \in F \land y \subseteq x)$
38	35 37	sylbi	$⊢ y \in (F \cap 𝒫 x) \to (y \in F \land y \subseteq x)$
39	38	eximi	$⊢ \exists y y \in (F \cap 𝒫 x) \to \exists y (y \in F \land y \subseteq x)$
40	34 39	sylbi	$⊢ F \cap 𝒫 x \neq \emptyset \to \exists y (y \in F \land y \subseteq x)$
41		df-rex	$⊢ \exists y \in F y \subseteq x \leftrightarrow \exists y (y \in F \land y \subseteq x)$
42	40 41	sylibr	$⊢ F \cap 𝒫 x \neq \emptyset \to \exists y \in F y \subseteq x$
43	42	imim1i	$⊢ (\exists y \in F y \subseteq x \to x \in F) \to (F \cap 𝒫 x \neq \emptyset \to x \in F)$
44	43	ralimi	$⊢ \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \to \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F)$
45	44	3ad2ant2	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F)$
46		isfil	$⊢ F \in Fil (X) \leftrightarrow (F \in fBas (X) \land \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F))$
47	33 45 46	sylanbrc	$⊢ ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F) \to F \in Fil (X)$
48	16 47	impbii	$⊢ F \in Fil (X) \leftrightarrow ((F \subseteq 𝒫 X \land \neg \emptyset \in F \land X \in F) \land \forall x \in 𝒫 X (\exists y \in F y \subseteq x \to x \in F) \land \forall x \in F \forall y \in F x \cap y \in F)$

Metamath Proof Explorer

Theorem isfil2

Proof