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

Metamath Proof Explorer

Theorem fbasfip

Description: A filter base has the finite intersection property. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbasfip 
|- ( F e. ( fBas ` X ) -> -. (/) e. ( fi ` F ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( y e. ( ~P F i^i Fin ) <-> ( y e. ~P F /\ y e. Fin ) )
2 elpwi 
 |-  ( y e. ~P F -> y C_ F )
3 2 anim1i 
 |-  ( ( y e. ~P F /\ y e. Fin ) -> ( y C_ F /\ y e. Fin ) )
4 1 3 sylbi 
 |-  ( y e. ( ~P F i^i Fin ) -> ( y C_ F /\ y e. Fin ) )
5 fbssint 
 |-  ( ( F e. ( fBas ` X ) /\ y C_ F /\ y e. Fin ) -> E. z e. F z C_ |^| y )
6 5 3expb 
 |-  ( ( F e. ( fBas ` X ) /\ ( y C_ F /\ y e. Fin ) ) -> E. z e. F z C_ |^| y )
7 4 6 sylan2 
 |-  ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) -> E. z e. F z C_ |^| y )
8 0nelfb 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. F )
9 8 ad2antrr 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. (/) e. F )
10 eleq1 
 |-  ( z = (/) -> ( z e. F <-> (/) e. F ) )
11 10 biimpcd 
 |-  ( z e. F -> ( z = (/) -> (/) e. F ) )
12 11 adantl 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> ( z = (/) -> (/) e. F ) )
13 9 12 mtod 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. z = (/) )
14 ss0 
 |-  ( z C_ (/) -> z = (/) )
15 13 14 nsyl 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. z C_ (/) )
16 15 adantrr 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> -. z C_ (/) )
17 sseq2 
 |-  ( (/) = |^| y -> ( z C_ (/) <-> z C_ |^| y ) )
18 17 biimprcd 
 |-  ( z C_ |^| y -> ( (/) = |^| y -> z C_ (/) ) )
19 18 ad2antll 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> ( (/) = |^| y -> z C_ (/) ) )
20 16 19 mtod 
 |-  ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> -. (/) = |^| y )
21 7 20 rexlimddv 
 |-  ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) -> -. (/) = |^| y )
22 21 nrexdv 
 |-  ( F e. ( fBas ` X ) -> -. E. y e. ( ~P F i^i Fin ) (/) = |^| y )
23 0ex 
 |-  (/) e. _V
24 elfi 
 |-  ( ( (/) e. _V /\ F e. ( fBas ` X ) ) -> ( (/) e. ( fi ` F ) <-> E. y e. ( ~P F i^i Fin ) (/) = |^| y ) )
25 23 24 mpan 
 |-  ( F e. ( fBas ` X ) -> ( (/) e. ( fi ` F ) <-> E. y e. ( ~P F i^i Fin ) (/) = |^| y ) )
26 22 25 mtbird 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. ( fi ` F ) )