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 V J 𝒫 A J 𝑡 A = J

Proof

Step Hyp Ref Expression
1 pwexg A V 𝒫 A V
2 1 adantr A V J 𝒫 A 𝒫 A V
3 simpr A V J 𝒫 A J 𝒫 A
4 2 3 ssexd A V J 𝒫 A J V
5 simpl A V J 𝒫 A A V
6 restval J V A V J 𝑡 A = ran x J x A
7 4 5 6 syl2anc A V J 𝒫 A J 𝑡 A = ran x J x A
8 3 sselda A V J 𝒫 A x J x 𝒫 A
9 8 elpwid A V J 𝒫 A x J x A
10 df-ss x A x A = x
11 9 10 sylib A V J 𝒫 A x J x A = x
12 11 mpteq2dva A V J 𝒫 A x J x A = x J x
13 mptresid I J = x J x
14 12 13 eqtr4di A V J 𝒫 A x J x A = I J
15 14 rneqd A V J 𝒫 A ran x J x A = ran I J
16 rnresi ran I J = J
17 15 16 eqtrdi A V J 𝒫 A ran x J x A = J
18 7 17 eqtrd A V J 𝒫 A J 𝑡 A = J