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 e. ( Fil ` X ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> |^| A =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		elfir	|- ( ( F e. ( Fil ` X ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. ( fi ` F ) )
2		filfi	|- ( F e. ( Fil ` X ) -> ( fi ` F ) = F )
3	2	adantr	|- ( ( F e. ( Fil ` X ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> ( fi ` F ) = F )
4	1 3	eleqtrd	|- ( ( F e. ( Fil ` X ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. F )
5		fileln0	|- ( ( F e. ( Fil ` X ) /\ |^| A e. F ) -> |^| A =/= (/) )
6	4 5	syldan	|- ( ( F e. ( Fil ` X ) /\ ( A C_ F /\ A =/= (/) /\ A e. Fin ) ) -> |^| A =/= (/) )