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 ⊢ × t = r ∈ V , s ∈ V ⟼ topGen ⁡ ran ⁡ x ∈ r , y ∈ s ⟼ x × y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctx class × t
1 vr setvar r
2 cvv class V
3 vs setvar s
4 ctg class topGen
5 vx setvar x
6 1 cv setvar r
7 vy setvar y
8 3 cv setvar s
9 5 cv setvar x
10 7 cv setvar y
11 9 10 cxp class x × y
12 5 7 6 8 11 cmpo class x ∈ r , y ∈ s ⟼ x × y
13 12 crn class ran ⁡ x ∈ r , y ∈ s ⟼ x × y
14 13 4 cfv class topGen ⁡ ran ⁡ x ∈ r , y ∈ s ⟼ x × y
15 1 3 2 2 14 cmpo class r ∈ V , s ∈ V ⟼ topGen ⁡ ran ⁡ x ∈ r , y ∈ s ⟼ x × y
16 0 15 wceq wff × t = r ∈ V , s ∈ V ⟼ topGen ⁡ ran ⁡ x ∈ r , y ∈ s ⟼ x × y