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 ) )