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 \in R, y \in S ⟼ x \times y)$
	Assertion	txval	$⊢ (R \in V \land S \in W) \to R \times_{t} S = topGen (B)$

Step	Hyp	Ref	Expression
1		txval.1	$⊢ B = ran (x \in R, y \in S ⟼ x \times y)$
2		elex	$⊢ R \in V \to R \in V$
3		elex	$⊢ S \in W \to S \in V$
4		mpoeq12	$⊢ (r = R \land s = S) \to (x \in r, y \in s ⟼ x \times y) = (x \in R, y \in S ⟼ x \times y)$
5	4	rneqd	$⊢ (r = R \land s = S) \to ran (x \in r, y \in s ⟼ x \times y) = ran (x \in R, y \in S ⟼ x \times y)$
6	5 1	syl6eqr	$⊢ (r = R \land s = S) \to ran (x \in r, y \in s ⟼ x \times y) = B$
7	6	fveq2d	$⊢ (r = R \land s = S) \to topGen (ran (x \in r, y \in s ⟼ x \times y)) = topGen (B)$
8		df-tx	$⊢ \times_{t} = (r \in V, s \in V ⟼ topGen (ran (x \in r, y \in s ⟼ x \times y)))$
9		fvex	$⊢ topGen (B) \in V$
10	7 8 9	ovmpoa	$⊢ (R \in V \land S \in V) \to R \times_{t} S = topGen (B)$
11	2 3 10	syl2an	$⊢ (R \in V \land S \in W) \to R \times_{t} S = topGen (B)$

Metamath Proof Explorer