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

Metamath Proof Explorer

Theorem restid2

Description: The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion restid2 
|- ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = J )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 1 adantr 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ~P A e. _V )
3 simpr 
 |-  ( ( A e. V /\ J C_ ~P A ) -> J C_ ~P A )
4 2 3 ssexd 
 |-  ( ( A e. V /\ J C_ ~P A ) -> J e. _V )
5 simpl 
 |-  ( ( A e. V /\ J C_ ~P A ) -> A e. V )
6 restval 
 |-  ( ( J e. _V /\ A e. V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
7 4 5 6 syl2anc 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
8 3 sselda 
 |-  ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> x e. ~P A )
9 8 elpwid 
 |-  ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> x C_ A )
10 dfss2 
 |-  ( x C_ A <-> ( x i^i A ) = x )
11 9 10 sylib 
 |-  ( ( ( A e. V /\ J C_ ~P A ) /\ x e. J ) -> ( x i^i A ) = x )
12 11 mpteq2dva 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ( x e. J |-> ( x i^i A ) ) = ( x e. J |-> x ) )
13 mptresid 
 |-  ( _I |` J ) = ( x e. J |-> x )
14 12 13 eqtr4di 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ( x e. J |-> ( x i^i A ) ) = ( _I |` J ) )
15 14 rneqd 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ran ( x e. J |-> ( x i^i A ) ) = ran ( _I |` J ) )
16 rnresi 
 |-  ran ( _I |` J ) = J
17 15 16 eqtrdi 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ran ( x e. J |-> ( x i^i A ) ) = J )
18 7 17 eqtrd 
 |-  ( ( A e. V /\ J C_ ~P A ) -> ( J |`t A ) = J )