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

Metamath Proof Explorer

Theorem restopnssd

Description: A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses restopnssd.1 
|- ( ph -> J e. Top )
restopnssd.2 
|- ( ph -> A e. J )
Assertion restopnssd 
|- ( ph -> ( J |`t A ) C_ J )

Proof

Step Hyp Ref Expression
1 restopnssd.1 
 |-  ( ph -> J e. Top )
2 restopnssd.2 
 |-  ( ph -> A e. J )
3 simpr 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> x e. ( J |`t A ) )
4 1 adantr 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> J e. Top )
5 2 adantr 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> A e. J )
6 restopn2 
 |-  ( ( J e. Top /\ A e. J ) -> ( x e. ( J |`t A ) <-> ( x e. J /\ x C_ A ) ) )
7 4 5 6 syl2anc 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> ( x e. ( J |`t A ) <-> ( x e. J /\ x C_ A ) ) )
8 3 7 mpbid 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> ( x e. J /\ x C_ A ) )
9 8 simpld 
 |-  ( ( ph /\ x e. ( J |`t A ) ) -> x e. J )
10 9 ssd 
 |-  ( ph -> ( J |`t A ) C_ J )