snfbas

Description: Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	snfbas	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to \{A\} \in fBas (B)$

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
2	1	3adant2	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to A \in V$
3		simp2	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to A \neq \emptyset$
4		snfil	$⊢ (A \in V \land A \neq \emptyset) \to \{A\} \in Fil (A)$
5	2 3 4	syl2anc	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to \{A\} \in Fil (A)$
6		filfbas	$⊢ \{A\} \in Fil (A) \to \{A\} \in fBas (A)$
7	5 6	syl	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to \{A\} \in fBas (A)$
8		simp1	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to A \subseteq B$
9		elpw2g	$⊢ B \in V \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
10	9	3ad2ant3	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
11	8 10	mpbird	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to A \in 𝒫 B$
12	11	snssd	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to \{A\} \subseteq 𝒫 B$
13		simp3	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to B \in V$
14		fbasweak	$⊢ (\{A\} \in fBas (A) \land \{A\} \subseteq 𝒫 B \land B \in V) \to \{A\} \in fBas (B)$
15	7 12 13 14	syl3anc	$⊢ (A \subseteq B \land A \neq \emptyset \land B \in V) \to \{A\} \in fBas (B)$

Metamath Proof Explorer