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 ) ) ) )