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

Metamath Proof Explorer

Theorem isbasis3g

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

Ref Expression
Assertion isbasis3g 
|- ( B e. C -> ( B e. TopBases <-> ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 elssuni 
 |-  ( x e. B -> x C_ U. B )
3 2 rgen 
 |-  A. x e. B x C_ U. B
4 eluni2 
 |-  ( x e. U. B <-> E. y e. B x e. y )
5 4 biimpi 
 |-  ( x e. U. B -> E. y e. B x e. y )
6 5 rgen 
 |-  A. x e. U. B E. y e. B x e. y
7 3 6 pm3.2i 
 |-  ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. y )
8 7 biantrur 
 |-  ( 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 ) ) <-> ( ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) )
9 df-3an 
 |-  ( ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) <-> ( ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) )
10 8 9 bitr4i 
 |-  ( 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 ) ) <-> ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) )
11 1 10 bitrdi 
 |-  ( B e. C -> ( B e. TopBases <-> ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. 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 ) ) ) ) )