This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )