Theorem restdis

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

	Ref	Expression
Assertion	restdis	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐴 ↾t 𝐵 ) = 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		distop	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top )
2		elpw2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3	2	biimpar	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝒫 𝐴 )
4		restopn2	⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝐵 ∈ 𝒫 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
5	1 3 4	syl2an2r	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
6		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
7		sstr	⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 )
8	7	expcom	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐴 ) )
10		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
11	9 10	imbitrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 → 𝑥 ∈ 𝒫 𝐴 ) )
12	11	pm4.71rd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
13	6 12	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝒫 𝐵 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) )
14	5 13	bitr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ↾t 𝐵 ) ↔ 𝑥 ∈ 𝒫 𝐵 ) )
15	14	eqrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐴 ↾t 𝐵 ) = 𝒫 𝐵 )