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

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 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 =/= (/) )