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 ) )