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

Metamath Proof Explorer

Definition df-bases

Description: Define the class of topological bases. Equivalent to definition of basis in Munkres p. 78 (see isbasis2g ). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion df-bases 
|- TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctb 
 |-  TopBases
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 vz 
 |-  z
5 2 cv 
 |-  y
6 4 cv 
 |-  z
7 5 6 cin 
 |-  ( y i^i z )
8 7 cpw 
 |-  ~P ( y i^i z )
9 3 8 cin 
 |-  ( x i^i ~P ( y i^i z ) )
10 9 cuni 
 |-  U. ( x i^i ~P ( y i^i z ) )
11 7 10 wss 
 |-  ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
12 11 4 3 wral 
 |-  A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
13 12 2 3 wral 
 |-  A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
14 13 1 cab 
 |-  { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }
15 0 14 wceq 
 |-  TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }