Metamath Proof Explorer

Theorem filintn0

Description: A filter has the finite intersection property. Remark below Definition 1 of BourbakiTop1 p. I.36. (Contributed by FL, 20-Sep-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filintn0	$⊢ (F \in Fil (X) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elfir	$⊢ (F \in Fil (X) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \in fi (F)$
2		filfi	$⊢ F \in Fil (X) \to fi (F) = F$
3	2	adantr	$⊢ (F \in Fil (X) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to fi (F) = F$
4	1 3	eleqtrd	$⊢ (F \in Fil (X) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \in F$
5		fileln0	$⊢ (F \in Fil (X) \land ⋂ A \in F) \to ⋂ A \neq \emptyset$
6	4 5	syldan	$⊢ (F \in Fil (X) \land (A \subseteq F \land A \neq \emptyset \land A \in Fin)) \to ⋂ A \neq \emptyset$