This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fbasweak

Description: A filter base on any set is also a filter base on any larger set. (Contributed by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fbasweak	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to F \in fBas (Y)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to F \subseteq 𝒫 Y$
2		simp1	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to F \in fBas (X)$
3		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
4	3	3ad2ant1	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to X \in dom fBas$
5		isfbas	$⊢ X \in dom fBas \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 F \cap 𝒫 (x \cap y) \neq \emptyset)))$
6	4 5	syl	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \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 F \cap 𝒫 (x \cap y) \neq \emptyset)))$
7	2 6	mpbid	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset))$
8	7	simprd	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)$
9		isfbas	$⊢ Y \in V \to (F \in fBas (Y) \leftrightarrow (F \subseteq 𝒫 Y \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
10	9	3ad2ant3	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to (F \in fBas (Y) \leftrightarrow (F \subseteq 𝒫 Y \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
11	1 8 10	mpbir2and	$⊢ (F \in fBas (X) \land F \subseteq 𝒫 Y \land Y \in V) \to F \in fBas (Y)$