This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pttopon

Description: The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis ptunimpt.j 
|- J = ( Xt_ ` ( x e. A |-> K ) )
Assertion pttopon 
|- ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> J e. ( TopOn ` X_ x e. A B ) )

Proof

Step Hyp Ref Expression
1 ptunimpt.j 
 |-  J = ( Xt_ ` ( x e. A |-> K ) )
2 topontop 
 |-  ( K e. ( TopOn ` B ) -> K e. Top )
3 2 ralimi 
 |-  ( A. x e. A K e. ( TopOn ` B ) -> A. x e. A K e. Top )
4 eqid 
 |-  ( x e. A |-> K ) = ( x e. A |-> K )
5 4 fmpt 
 |-  ( A. x e. A K e. Top <-> ( x e. A |-> K ) : A --> Top )
6 3 5 sylib 
 |-  ( A. x e. A K e. ( TopOn ` B ) -> ( x e. A |-> K ) : A --> Top )
7 pttop 
 |-  ( ( A e. V /\ ( x e. A |-> K ) : A --> Top ) -> ( Xt_ ` ( x e. A |-> K ) ) e. Top )
8 1 7 eqeltrid 
 |-  ( ( A e. V /\ ( x e. A |-> K ) : A --> Top ) -> J e. Top )
9 6 8 sylan2 
 |-  ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> J e. Top )
10 toponuni 
 |-  ( K e. ( TopOn ` B ) -> B = U. K )
11 10 ralimi 
 |-  ( A. x e. A K e. ( TopOn ` B ) -> A. x e. A B = U. K )
12 ixpeq2 
 |-  ( A. x e. A B = U. K -> X_ x e. A B = X_ x e. A U. K )
13 11 12 syl 
 |-  ( A. x e. A K e. ( TopOn ` B ) -> X_ x e. A B = X_ x e. A U. K )
14 13 adantl 
 |-  ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> X_ x e. A B = X_ x e. A U. K )
15 1 ptunimpt 
 |-  ( ( A e. V /\ A. x e. A K e. Top ) -> X_ x e. A U. K = U. J )
16 3 15 sylan2 
 |-  ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> X_ x e. A U. K = U. J )
17 14 16 eqtrd 
 |-  ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> X_ x e. A B = U. J )
18 istopon 
 |-  ( J e. ( TopOn ` X_ x e. A B ) <-> ( J e. Top /\ X_ x e. A B = U. J ) )
19 9 17 18 sylanbrc 
 |-  ( ( A e. V /\ A. x e. A K e. ( TopOn ` B ) ) -> J e. ( TopOn ` X_ x e. A B ) )