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

Metamath Proof Explorer

Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion isfbas2 
|- ( B e. A -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) =/= (/) ) ) ) )
2 elin 
 |-  ( z e. ( F i^i ~P ( x i^i y ) ) <-> ( z e. F /\ z e. ~P ( x i^i y ) ) )
3 velpw 
 |-  ( z e. ~P ( x i^i y ) <-> z C_ ( x i^i y ) )
4 3 anbi2i 
 |-  ( ( z e. F /\ z e. ~P ( x i^i y ) ) <-> ( z e. F /\ z C_ ( x i^i y ) ) )
5 2 4 bitri 
 |-  ( z e. ( F i^i ~P ( x i^i y ) ) <-> ( z e. F /\ z C_ ( x i^i y ) ) )
6 5 exbii 
 |-  ( E. z z e. ( F i^i ~P ( x i^i y ) ) <-> E. z ( z e. F /\ z C_ ( x i^i y ) ) )
7 n0 
 |-  ( ( F i^i ~P ( x i^i y ) ) =/= (/) <-> E. z z e. ( F i^i ~P ( x i^i y ) ) )
8 df-rex 
 |-  ( E. z e. F z C_ ( x i^i y ) <-> E. z ( z e. F /\ z C_ ( x i^i y ) ) )
9 6 7 8 3bitr4i 
 |-  ( ( F i^i ~P ( x i^i y ) ) =/= (/) <-> E. z e. F z C_ ( x i^i y ) )
10 9 2ralbii 
 |-  ( A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) <-> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) )
11 10 3anbi3i 
 |-  ( ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) <-> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) )
12 11 anbi2i 
 |-  ( ( F C_ ~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 E. z e. F z C_ ( x i^i y ) ) ) )
13 1 12 bitrdi 
 |-  ( B e. A -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )