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 = ( Xt_ ` ( x e. A |-> K ) )
Assertion ptunimpt 
|- ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = U. J )

Proof

Step Hyp Ref Expression
1 ptunimpt.j 
 |-  J = ( Xt_ ` ( x e. A |-> K ) )
2 eqid 
 |-  ( x e. A |-> K ) = ( x e. A |-> K )
3 2 fvmpt2 
 |-  ( ( x e. A /\ K e. Top ) -> ( ( x e. A |-> K ) ` x ) = K )
4 3 eqcomd 
 |-  ( ( x e. A /\ K e. Top ) -> K = ( ( x e. A |-> K ) ` x ) )
5 4 unieqd 
 |-  ( ( x e. A /\ K e. Top ) -> U. K = U. ( ( x e. A |-> K ) ` x ) )
6 5 ralimiaa 
 |-  ( A. x e. A K e. Top -> A. x e. A U. K = U. ( ( x e. A |-> K ) ` x ) )
7 6 adantl 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> A. x e. A U. K = U. ( ( x e. A |-> K ) ` x ) )
8 ixpeq2 
 |-  ( A. x e. A U. K = U. ( ( x e. A |-> K ) ` x ) -> X_ x e. A U. K = X_ x e. A U. ( ( x e. A |-> K ) ` x ) )
9 7 8 syl 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = X_ x e. A U. ( ( x e. A |-> K ) ` x ) )
10 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> K ) ` y )
11 10 nfuni 
 |-  F/_ x U. ( ( x e. A |-> K ) ` y )
12 nfcv 
 |-  F/_ y U. ( ( x e. A |-> K ) ` x )
13 fveq2 
 |-  ( y = x -> ( ( x e. A |-> K ) ` y ) = ( ( x e. A |-> K ) ` x ) )
14 13 unieqd 
 |-  ( y = x -> U. ( ( x e. A |-> K ) ` y ) = U. ( ( x e. A |-> K ) ` x ) )
15 11 12 14 cbvixp 
 |-  X_ y e. A U. ( ( x e. A |-> K ) ` y ) = X_ x e. A U. ( ( x e. A |-> K ) ` x )
16 9 15 eqtr4di 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = X_ y e. A U. ( ( x e. A |-> K ) ` y ) )
17 2 fmpt 
 |-  ( A. x e. A K e. Top <-> ( x e. A |-> K ) : A --> Top )
18 1 ptuni 
 |-  ( ( A e. V /\ ( x e. A |-> K ) : A --> Top ) -> X_ y e. A U. ( ( x e. A |-> K ) ` y ) = U. J )
19 17 18 sylan2b 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> X_ y e. A U. ( ( x e. A |-> K ) ` y ) = U. J )
20 16 19 eqtrd 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = U. J )