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

Metamath Proof Explorer

Definition df-tx

Description: Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion df-tx 
|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctx 
 |-  tX
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vs 
 |-  s
4 ctg 
 |-  topGen
5 vx 
 |-  x
6 1 cv 
 |-  r
7 vy 
 |-  y
8 3 cv 
 |-  s
9 5 cv 
 |-  x
10 7 cv 
 |-  y
11 9 10 cxp 
 |-  ( x X. y )
12 5 7 6 8 11 cmpo 
 |-  ( x e. r , y e. s |-> ( x X. y ) )
13 12 crn 
 |-  ran ( x e. r , y e. s |-> ( x X. y ) )
14 13 4 cfv 
 |-  ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) )
15 1 3 2 2 14 cmpo 
 |-  ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
16 0 15 wceq 
 |-  tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )