# Metamath Proof Explorer

## Theorem resttopon

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
2 id ${⊢}{A}\subseteq {X}\to {A}\subseteq {X}$
3 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
4 ssexg ${⊢}\left({A}\subseteq {X}\wedge {X}\in {J}\right)\to {A}\in \mathrm{V}$
5 2 3 4 syl2anr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {A}\in \mathrm{V}$
6 resttop ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{Top}$
7 1 5 6 syl2an2r ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{Top}$
8 simpr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {A}\subseteq {X}$
9 sseqin2 ${⊢}{A}\subseteq {X}↔{X}\cap {A}={A}$
10 8 9 sylib ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {X}\cap {A}={A}$
11 simpl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
12 3 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {X}\in {J}$
13 elrestr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\in \mathrm{V}\wedge {X}\in {J}\right)\to {X}\cap {A}\in \left({J}{↾}_{𝑡}{A}\right)$
14 11 5 12 13 syl3anc ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {X}\cap {A}\in \left({J}{↾}_{𝑡}{A}\right)$
15 10 14 eqeltrrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {A}\in \left({J}{↾}_{𝑡}{A}\right)$
16 elssuni ${⊢}{A}\in \left({J}{↾}_{𝑡}{A}\right)\to {A}\subseteq \bigcup \left({J}{↾}_{𝑡}{A}\right)$
17 15 16 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {A}\subseteq \bigcup \left({J}{↾}_{𝑡}{A}\right)$
18 restval ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{A}=\mathrm{ran}\left({x}\in {J}⟼{x}\cap {A}\right)$
19 5 18 syldan ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}{↾}_{𝑡}{A}=\mathrm{ran}\left({x}\in {J}⟼{x}\cap {A}\right)$
20 inss2 ${⊢}{x}\cap {A}\subseteq {A}$
21 vex ${⊢}{x}\in \mathrm{V}$
22 21 inex1 ${⊢}{x}\cap {A}\in \mathrm{V}$
23 22 elpw ${⊢}{x}\cap {A}\in 𝒫{A}↔{x}\cap {A}\subseteq {A}$
24 20 23 mpbir ${⊢}{x}\cap {A}\in 𝒫{A}$
25 24 a1i ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\wedge {x}\in {J}\right)\to {x}\cap {A}\in 𝒫{A}$
26 25 fmpttd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to \left({x}\in {J}⟼{x}\cap {A}\right):{J}⟶𝒫{A}$
27 26 frnd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to \mathrm{ran}\left({x}\in {J}⟼{x}\cap {A}\right)\subseteq 𝒫{A}$
28 19 27 eqsstrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}{↾}_{𝑡}{A}\subseteq 𝒫{A}$
29 sspwuni ${⊢}{J}{↾}_{𝑡}{A}\subseteq 𝒫{A}↔\bigcup \left({J}{↾}_{𝑡}{A}\right)\subseteq {A}$
30 28 29 sylib ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to \bigcup \left({J}{↾}_{𝑡}{A}\right)\subseteq {A}$
31 17 30 eqssd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
32 istopon ${⊢}{J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)↔\left({J}{↾}_{𝑡}{A}\in \mathrm{Top}\wedge {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)\right)$
33 7 31 32 sylanbrc ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)$