MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfbas Structured version   Unicode version

Theorem isfbas 19371
Description: The predicate " F is a filter base." Note that some authors require filter bases to be closed under pairwise intersections, but that is not necessary under our definition. One advantage of this definition is that tails in a directed set form a filter base under our meaning. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.)
Assertion
Ref Expression
isfbas  |-  ( B  e.  A  ->  ( F  e.  ( fBas `  B )  <->  ( F  C_ 
~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) )
Distinct variable groups:    x, y, F    x, B, y
Allowed substitution hints:    A( x, y)

Proof of Theorem isfbas
Dummy variables  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwexg 4469 . . . . 5  |-  ( B  e.  A  ->  ~P B  e.  _V )
2 elpw2g 4448 . . . . 5  |-  ( ~P B  e.  _V  ->  ( F  e.  ~P ~P B 
<->  F  C_  ~P B
) )
31, 2syl 16 . . . 4  |-  ( B  e.  A  ->  ( F  e.  ~P ~P B 
<->  F  C_  ~P B
) )
43anbi1d 704 . . 3  |-  ( B  e.  A  ->  (
( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) )  <-> 
( F  C_  ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) ) ) )
5 elex 2975 . . . 4  |-  ( B  e.  A  ->  B  e.  _V )
65biantrurd 508 . . 3  |-  ( B  e.  A  ->  (
( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) )  <-> 
( B  e.  _V  /\  ( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) ) )
74, 6bitr3d 255 . 2  |-  ( B  e.  A  ->  (
( F  C_  ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) )  <->  ( B  e.  _V  /\  ( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) ) )
8 df-fbas 17783 . . . 4  |-  fBas  =  ( z  e.  _V  |->  { w  e.  ~P ~P z  |  (
w  =/=  (/)  /\  (/)  e/  w  /\  A. x  e.  w  A. y  e.  w  ( w  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) } )
9 neeq1 2610 . . . . . 6  |-  ( w  =  F  ->  (
w  =/=  (/)  <->  F  =/=  (/) ) )
10 neleq2 2704 . . . . . 6  |-  ( w  =  F  ->  ( (/) 
e/  w  <->  (/)  e/  F
) )
11 ineq1 3538 . . . . . . . . 9  |-  ( w  =  F  ->  (
w  i^i  ~P (
x  i^i  y )
)  =  ( F  i^i  ~P ( x  i^i  y ) ) )
1211neeq1d 2615 . . . . . . . 8  |-  ( w  =  F  ->  (
( w  i^i  ~P ( x  i^i  y
) )  =/=  (/)  <->  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) )
1312raleqbi1dv 2919 . . . . . . 7  |-  ( w  =  F  ->  ( A. y  e.  w  ( w  i^i  ~P (
x  i^i  y )
)  =/=  (/)  <->  A. y  e.  F  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) )
1413raleqbi1dv 2919 . . . . . 6  |-  ( w  =  F  ->  ( A. x  e.  w  A. y  e.  w  ( w  i^i  ~P (
x  i^i  y )
)  =/=  (/)  <->  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) )
159, 10, 143anbi123d 1289 . . . . 5  |-  ( w  =  F  ->  (
( w  =/=  (/)  /\  (/)  e/  w  /\  A. x  e.  w  A. y  e.  w  ( w  i^i  ~P (
x  i^i  y )
)  =/=  (/) )  <->  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) )
1615adantl 466 . . . 4  |-  ( ( z  =  B  /\  w  =  F )  ->  ( ( w  =/=  (/)  /\  (/)  e/  w  /\  A. x  e.  w  A. y  e.  w  (
w  i^i  ~P (
x  i^i  y )
)  =/=  (/) )  <->  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) )
17 pweq 3856 . . . . 5  |-  ( z  =  B  ->  ~P z  =  ~P B
)
1817pweqd 3858 . . . 4  |-  ( z  =  B  ->  ~P ~P z  =  ~P ~P B )
19 vex 2969 . . . . . . 7  |-  z  e. 
_V
2019pwex 4468 . . . . . 6  |-  ~P z  e.  _V
2120pwex 4468 . . . . 5  |-  ~P ~P z  e.  _V
2221a1i 11 . . . 4  |-  ( z  e.  _V  ->  ~P ~P z  e.  _V )
238, 16, 18, 22elmptrab 19369 . . 3  |-  ( F  e.  ( fBas `  B
)  <->  ( B  e. 
_V  /\  F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) )
24 3anass 969 . . 3  |-  ( ( B  e.  _V  /\  F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P ( x  i^i  y ) )  =/=  (/) ) )  <->  ( B  e.  _V  /\  ( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) )
2523, 24bitri 249 . 2  |-  ( F  e.  ( fBas `  B
)  <->  ( B  e. 
_V  /\  ( F  e.  ~P ~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) )
267, 25syl6rbbr 264 1  |-  ( B  e.  A  ->  ( F  e.  ( fBas `  B )  <->  ( F  C_ 
~P B  /\  ( F  =/=  (/)  /\  (/)  e/  F  /\  A. x  e.  F  A. y  e.  F  ( F  i^i  ~P (
x  i^i  y )
)  =/=  (/) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2600    e/ wnel 2601   A.wral 2709   _Vcvv 2966    i^i cin 3320    C_ wss 3321   (/)c0 3630   ~Pcpw 3853   ` cfv 5411   fBascfbas 17773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fv 5419  df-fbas 17783
This theorem is referenced by:  fbasne0  19372  0nelfb  19373  fbsspw  19374  isfbas2  19377  trfbas2  19385  fbasweak  19407  zfbas  19438  tsmsfbas  19667  ustfilxp  19756  minveclem3b  20884
  Copyright terms: Public domain W3C validator