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

Metamath Proof Explorer

Theorem isbasisg

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

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( z = B -> ( z i^i ~P ( x i^i y ) ) = ( B i^i ~P ( x i^i y ) ) )
2 1 unieqd 
 |-  ( z = B -> U. ( z i^i ~P ( x i^i y ) ) = U. ( B i^i ~P ( x i^i y ) ) )
3 2 sseq2d 
 |-  ( z = B -> ( ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
4 3 raleqbi1dv 
 |-  ( z = B -> ( A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
5 4 raleqbi1dv 
 |-  ( z = B -> ( A. x e. z A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
6 df-bases 
 |-  TopBases = { z | A. x e. z A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) }
7 5 6 elab2g 
 |-  ( 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 ) ) ) )