This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | txtopi.1 | ||
| txtopi.2 | |||
| Assertion | txtopi |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | txtopi.1 | ||
| 2 | txtopi.2 | ||
| 3 | txtop | ||
| 4 | 1 2 3 | mp2an |