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

Metamath Proof Explorer

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 )