Theorem stoig

Description: The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009) (Proof shortened by Mario Carneiro, 1-May-2015)

	Ref	Expression
Hypothesis	restuni.1	|- X = U. J
Assertion	stoig	|- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ( J |`t A ) >. } e. TopSp )

Proof

Step	Hyp	Ref	Expression
1		restuni.1	|- X = U. J
2	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
3		resttopon	|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
4	2 3	sylanb	|- ( ( J e. Top /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
5		eqid	|- { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ( J |`t A ) >. } = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ( J |`t A ) >. }
6	5	eltpsg	|- ( ( J |`t A ) e. ( TopOn ` A ) -> { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ( J |`t A ) >. } e. TopSp )
7	4 6	syl	|- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , ( J |`t A ) >. } e. TopSp )