Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uptx.1 | |
|
uptx.2 | |
||
uptx.3 | |
||
uptx.4 | |
||
uptx.5 | |
||
uptx.6 | |
||
Assertion | uptx | |