Theorem restdis

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

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

Proof

Step	Hyp	Ref	Expression
1		distop	|- ( A e. V -> ~P A e. Top )
2		elpw2g	|- ( A e. V -> ( B e. ~P A <-> B C_ A ) )
3	2	biimpar	|- ( ( A e. V /\ B C_ A ) -> B e. ~P A )
4		restopn2	|- ( ( ~P A e. Top /\ B e. ~P A ) -> ( x e. ( ~P A |`t B ) <-> ( x e. ~P A /\ x C_ B ) ) )
5	1 3 4	syl2an2r	|- ( ( A e. V /\ B C_ A ) -> ( x e. ( ~P A |`t B ) <-> ( x e. ~P A /\ x C_ B ) ) )
6		velpw	|- ( x e. ~P B <-> x C_ B )
7		sstr	|- ( ( x C_ B /\ B C_ A ) -> x C_ A )
8	7	expcom	|- ( B C_ A -> ( x C_ B -> x C_ A ) )
9	8	adantl	|- ( ( A e. V /\ B C_ A ) -> ( x C_ B -> x C_ A ) )
10		velpw	|- ( x e. ~P A <-> x C_ A )
11	9 10	imbitrrdi	|- ( ( A e. V /\ B C_ A ) -> ( x C_ B -> x e. ~P A ) )
12	11	pm4.71rd	|- ( ( A e. V /\ B C_ A ) -> ( x C_ B <-> ( x e. ~P A /\ x C_ B ) ) )
13	6 12	bitrid	|- ( ( A e. V /\ B C_ A ) -> ( x e. ~P B <-> ( x e. ~P A /\ x C_ B ) ) )
14	5 13	bitr4d	|- ( ( A e. V /\ B C_ A ) -> ( x e. ( ~P A |`t B ) <-> x e. ~P B ) )
15	14	eqrdv	|- ( ( A e. V /\ B C_ A ) -> ( ~P A |`t B ) = ~P B )