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

Metamath Proof Explorer

Theorem isbasis2g

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion isbasis2g 
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )

Proof

Step Hyp Ref Expression
1 isbasisg 
 |-  ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
2 dfss3 
 |-  ( ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. z e. ( x i^i y ) z e. U. ( B i^i ~P ( x i^i y ) ) )
3 elin 
 |-  ( w e. ( B i^i ~P ( x i^i y ) ) <-> ( w e. B /\ w e. ~P ( x i^i y ) ) )
4 velpw 
 |-  ( w e. ~P ( x i^i y ) <-> w C_ ( x i^i y ) )
5 4 anbi2i 
 |-  ( ( w e. B /\ w e. ~P ( x i^i y ) ) <-> ( w e. B /\ w C_ ( x i^i y ) ) )
6 3 5 bitri 
 |-  ( w e. ( B i^i ~P ( x i^i y ) ) <-> ( w e. B /\ w C_ ( x i^i y ) ) )
7 6 anbi2i 
 |-  ( ( z e. w /\ w e. ( B i^i ~P ( x i^i y ) ) ) <-> ( z e. w /\ ( w e. B /\ w C_ ( x i^i y ) ) ) )
8 an12 
 |-  ( ( z e. w /\ ( w e. B /\ w C_ ( x i^i y ) ) ) <-> ( w e. B /\ ( z e. w /\ w C_ ( x i^i y ) ) ) )
9 7 8 bitri 
 |-  ( ( z e. w /\ w e. ( B i^i ~P ( x i^i y ) ) ) <-> ( w e. B /\ ( z e. w /\ w C_ ( x i^i y ) ) ) )
10 9 exbii 
 |-  ( E. w ( z e. w /\ w e. ( B i^i ~P ( x i^i y ) ) ) <-> E. w ( w e. B /\ ( z e. w /\ w C_ ( x i^i y ) ) ) )
11 eluni 
 |-  ( z e. U. ( B i^i ~P ( x i^i y ) ) <-> E. w ( z e. w /\ w e. ( B i^i ~P ( x i^i y ) ) ) )
12 df-rex 
 |-  ( E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) <-> E. w ( w e. B /\ ( z e. w /\ w C_ ( x i^i y ) ) ) )
13 10 11 12 3bitr4i 
 |-  ( z e. U. ( B i^i ~P ( x i^i y ) ) <-> E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
14 13 ralbii 
 |-  ( A. z e. ( x i^i y ) z e. U. ( B i^i ~P ( x i^i y ) ) <-> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
15 2 14 bitri 
 |-  ( ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
16 15 2ralbii 
 |-  ( A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
17 1 16 bitrdi 
 |-  ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )