Metamath Proof Explorer


Theorem txval

Description: Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 30-Aug-2015)

Ref Expression
Hypothesis txval.1 B = ran x R , y S x × y
Assertion txval R V S W R × t S = topGen B

Proof

Step Hyp Ref Expression
1 txval.1 B = ran x R , y S x × y
2 elex R V R V
3 elex S W S V
4 mpoeq12 r = R s = S x r , y s x × y = x R , y S x × y
5 4 rneqd r = R s = S ran x r , y s x × y = ran x R , y S x × y
6 5 1 eqtr4di r = R s = S ran x r , y s x × y = B
7 6 fveq2d r = R s = S topGen ran x r , y s x × y = topGen B
8 df-tx × t = r V , s V topGen ran x r , y s x × y
9 fvex topGen B V
10 7 8 9 ovmpoa R V S V R × t S = topGen B
11 2 3 10 syl2an R V S W R × t S = topGen B