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 A F fBas B F 𝒫 B F F x F y F z F z x y

Proof

Step Hyp Ref Expression
1 isfbas B A F fBas B F 𝒫 B F F x F y F F 𝒫 x y
2 elin z F 𝒫 x y z F z 𝒫 x y
3 velpw z 𝒫 x y z x y
4 3 anbi2i z F z 𝒫 x y z F z x y
5 2 4 bitri z F 𝒫 x y z F z x y
6 5 exbii z z F 𝒫 x y z z F z x y
7 n0 F 𝒫 x y z z F 𝒫 x y
8 df-rex z F z x y z z F z x y
9 6 7 8 3bitr4i F 𝒫 x y z F z x y
10 9 2ralbii x F y F F 𝒫 x y x F y F z F z x y
11 10 3anbi3i F F x F y F F 𝒫 x y F F x F y F z F z x y
12 11 anbi2i F 𝒫 B F F x F y F F 𝒫 x y F 𝒫 B F F x F y F z F z x y
13 1 12 bitrdi B A F fBas B F 𝒫 B F F x F y F z F z x y