Theorem restdis

Description: A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Assertion	restdis	$$⊢\left(A\in V\wedge B\subseteq A\right)\to 𝒫A{\upharpoonright }_{𝑡}B=𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		distop	$$⊢A\in V\to 𝒫A\in \mathrm{Top}$$
2		elpw2g	$$⊢A\in V\to \left(B\in 𝒫A\leftrightarrow B\subseteq A\right)$$
3	2	biimpar	$$⊢\left(A\in V\wedge B\subseteq A\right)\to B\in 𝒫A$$
4		restopn2	$$⊢\left(𝒫A\in \mathrm{Top}\wedge B\in 𝒫A\right)\to \left(x\in \left(𝒫A{\upharpoonright }_{𝑡}B\right)\leftrightarrow \left(x\in 𝒫A\wedge x\subseteq B\right)\right)$$
5	1 3 4	syl2an2r	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\in \left(𝒫A{\upharpoonright }_{𝑡}B\right)\leftrightarrow \left(x\in 𝒫A\wedge x\subseteq B\right)\right)$$
6		velpw	$$⊢x\in 𝒫B\leftrightarrow x\subseteq B$$
7		sstr	$$⊢\left(x\subseteq B\wedge B\subseteq A\right)\to x\subseteq A$$
8	7	expcom	$$⊢B\subseteq A\to \left(x\subseteq B\to x\subseteq A\right)$$
9	8	adantl	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\subseteq B\to x\subseteq A\right)$$
10		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
11	9 10	imbitrrdi	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\subseteq B\to x\in 𝒫A\right)$$
12	11	pm4.71rd	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\subseteq B\leftrightarrow \left(x\in 𝒫A\wedge x\subseteq B\right)\right)$$
13	6 12	bitrid	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\in 𝒫B\leftrightarrow \left(x\in 𝒫A\wedge x\subseteq B\right)\right)$$
14	5 13	bitr4d	$$⊢\left(A\in V\wedge B\subseteq A\right)\to \left(x\in \left(𝒫A{\upharpoonright }_{𝑡}B\right)\leftrightarrow x\in 𝒫B\right)$$
15	14	eqrdv	$$⊢\left(A\in V\wedge B\subseteq A\right)\to 𝒫A{\upharpoonright }_{𝑡}B=𝒫B$$