Metamath Proof Explorer


Theorem ptunimpt

Description: Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypothesis ptunimpt.j J=𝑡xAK
Assertion ptunimpt AVxAKTopxAK=J

Proof

Step Hyp Ref Expression
1 ptunimpt.j J=𝑡xAK
2 eqid xAK=xAK
3 2 fvmpt2 xAKTopxAKx=K
4 3 eqcomd xAKTopK=xAKx
5 4 unieqd xAKTopK=xAKx
6 5 ralimiaa xAKTopxAK=xAKx
7 6 adantl AVxAKTopxAK=xAKx
8 ixpeq2 xAK=xAKxxAK=xAxAKx
9 7 8 syl AVxAKTopxAK=xAxAKx
10 nffvmpt1 _xxAKy
11 10 nfuni _xxAKy
12 nfcv _yxAKx
13 fveq2 y=xxAKy=xAKx
14 13 unieqd y=xxAKy=xAKx
15 11 12 14 cbvixp yAxAKy=xAxAKx
16 9 15 eqtr4di AVxAKTopxAK=yAxAKy
17 2 fmpt xAKTopxAK:ATop
18 1 ptuni AVxAK:ATopyAxAKy=J
19 17 18 sylan2b AVxAKTopyAxAKy=J
20 16 19 eqtrd AVxAKTopxAK=J