filss

Description: A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filss	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to B \in F$

Proof

Step	Hyp	Ref	Expression
1		isfil	$⊢ F \in Fil (X) \leftrightarrow (F \in fBas (X) \land \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F))$
2	1	simprbi	$⊢ F \in Fil (X) \to \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F)$
3	2	adantr	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F)$
4		elfvdm	$⊢ F \in Fil (X) \to X \in dom Fil$
5		simp2	$⊢ (A \in F \land B \subseteq X \land A \subseteq B) \to B \subseteq X$
6		elpw2g	$⊢ X \in dom Fil \to (B \in 𝒫 X \leftrightarrow B \subseteq X)$
7	6	biimpar	$⊢ (X \in dom Fil \land B \subseteq X) \to B \in 𝒫 X$
8	4 5 7	syl2an	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to B \in 𝒫 X$
9		simpr1	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to A \in F$
10		simpr3	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to A \subseteq B$
11	9 10	elpwd	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to A \in 𝒫 B$
12		inelcm	$⊢ (A \in F \land A \in 𝒫 B) \to F \cap 𝒫 B \neq \emptyset$
13	9 11 12	syl2anc	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to F \cap 𝒫 B \neq \emptyset$
14		pweq	$⊢ x = B \to 𝒫 x = 𝒫 B$
15	14	ineq2d	$⊢ x = B \to F \cap 𝒫 x = F \cap 𝒫 B$
16	15	neeq1d	$⊢ x = B \to (F \cap 𝒫 x \neq \emptyset \leftrightarrow F \cap 𝒫 B \neq \emptyset)$
17		eleq1	$⊢ x = B \to (x \in F \leftrightarrow B \in F)$
18	16 17	imbi12d	$⊢ x = B \to ((F \cap 𝒫 x \neq \emptyset \to x \in F) \leftrightarrow (F \cap 𝒫 B \neq \emptyset \to B \in F))$
19	18	rspccv	$⊢ \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F) \to (B \in 𝒫 X \to (F \cap 𝒫 B \neq \emptyset \to B \in F))$
20	3 8 13 19	syl3c	$⊢ (F \in Fil (X) \land (A \in F \land B \subseteq X \land A \subseteq B)) \to B \in F$

Metamath Proof Explorer

Theorem filss

Proof