fbssint

Description: A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	fbssint	$⊢ (F \in fBas (B) \land A \subseteq F \land A \in Fin) \to \exists x \in F x \subseteq ⋂ A$

Proof

Step	Hyp	Ref	Expression
1		fbasne0	$⊢ F \in fBas (B) \to F \neq \emptyset$
2		n0	$⊢ F \neq \emptyset \leftrightarrow \exists x x \in F$
3	1 2	sylib	$⊢ F \in fBas (B) \to \exists x x \in F$
4		ssv	$⊢ x \subseteq V$
5	4	jctr	$⊢ x \in F \to (x \in F \land x \subseteq V)$
6	5	eximi	$⊢ \exists x x \in F \to \exists x (x \in F \land x \subseteq V)$
7		df-rex	$⊢ \exists x \in F x \subseteq V \leftrightarrow \exists x (x \in F \land x \subseteq V)$
8	6 7	sylibr	$⊢ \exists x x \in F \to \exists x \in F x \subseteq V$
9	3 8	syl	$⊢ F \in fBas (B) \to \exists x \in F x \subseteq V$
10		inteq	$⊢ A = \emptyset \to ⋂ A = ⋂ \emptyset$
11		int0	$⊢ ⋂ \emptyset = V$
12	10 11	syl6eq	$⊢ A = \emptyset \to ⋂ A = V$
13	12	sseq2d	$⊢ A = \emptyset \to (x \subseteq ⋂ A \leftrightarrow x \subseteq V)$
14	13	rexbidv	$⊢ A = \emptyset \to (\exists x \in F x \subseteq ⋂ A \leftrightarrow \exists x \in F x \subseteq V)$
15	9 14	syl5ibrcom	$⊢ F \in fBas (B) \to (A = \emptyset \to \exists x \in F x \subseteq ⋂ A)$
16	15	3ad2ant1	$⊢ (F \in fBas (B) \land A \subseteq F \land A \in Fin) \to (A = \emptyset \to \exists x \in F x \subseteq ⋂ A)$
17		simpl1	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to F \in fBas (B)$
18		simpl2	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to A \subseteq F$
19		simpr	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to A \neq \emptyset$
20		simpl3	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to A \in Fin$
21		elfir	$⊢ (F \in fBas (B) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \in fi (F)$
22	17 18 19 20 21	syl13anc	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to ⋂ A \in fi (F)$
23		fbssfi	$⊢ (F \in fBas (B) \land ⋂ A \in fi (F)) \to \exists x \in F x \subseteq ⋂ A$
24	17 22 23	syl2anc	$⊢ ((F \in fBas (B) \land A \subseteq F \land A \in Fin) \land A \neq \emptyset) \to \exists x \in F x \subseteq ⋂ A$
25	24	ex	$⊢ (F \in fBas (B) \land A \subseteq F \land A \in Fin) \to (A \neq \emptyset \to \exists x \in F x \subseteq ⋂ A)$
26	16 25	pm2.61dne	$⊢ (F \in fBas (B) \land A \subseteq F \land A \in Fin) \to \exists x \in F x \subseteq ⋂ A$

Metamath Proof Explorer

Theorem fbssint

Proof