Metamath Proof Explorer


Theorem dishaus

Description: A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007) (Proof shortened by Mario Carneiro, 8-Apr-2015)

Ref Expression
Assertion dishaus
|- ( A e. V -> ~P A e. Haus )

Proof

Step Hyp Ref Expression
1 distop
 |-  ( A e. V -> ~P A e. Top )
2 simplrl
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> x e. A )
3 2 snssd
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> { x } C_ A )
4 snex
 |-  { x } e. _V
5 4 elpw
 |-  ( { x } e. ~P A <-> { x } C_ A )
6 3 5 sylibr
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> { x } e. ~P A )
7 simplrr
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> y e. A )
8 7 snssd
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> { y } C_ A )
9 snex
 |-  { y } e. _V
10 9 elpw
 |-  ( { y } e. ~P A <-> { y } C_ A )
11 8 10 sylibr
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> { y } e. ~P A )
12 vsnid
 |-  x e. { x }
13 12 a1i
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> x e. { x } )
14 vsnid
 |-  y e. { y }
15 14 a1i
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> y e. { y } )
16 disjsn2
 |-  ( x =/= y -> ( { x } i^i { y } ) = (/) )
17 16 adantl
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> ( { x } i^i { y } ) = (/) )
18 eleq2
 |-  ( u = { x } -> ( x e. u <-> x e. { x } ) )
19 ineq1
 |-  ( u = { x } -> ( u i^i v ) = ( { x } i^i v ) )
20 19 eqeq1d
 |-  ( u = { x } -> ( ( u i^i v ) = (/) <-> ( { x } i^i v ) = (/) ) )
21 18 20 3anbi13d
 |-  ( u = { x } -> ( ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) <-> ( x e. { x } /\ y e. v /\ ( { x } i^i v ) = (/) ) ) )
22 eleq2
 |-  ( v = { y } -> ( y e. v <-> y e. { y } ) )
23 ineq2
 |-  ( v = { y } -> ( { x } i^i v ) = ( { x } i^i { y } ) )
24 23 eqeq1d
 |-  ( v = { y } -> ( ( { x } i^i v ) = (/) <-> ( { x } i^i { y } ) = (/) ) )
25 22 24 3anbi23d
 |-  ( v = { y } -> ( ( x e. { x } /\ y e. v /\ ( { x } i^i v ) = (/) ) <-> ( x e. { x } /\ y e. { y } /\ ( { x } i^i { y } ) = (/) ) ) )
26 21 25 rspc2ev
 |-  ( ( { x } e. ~P A /\ { y } e. ~P A /\ ( x e. { x } /\ y e. { y } /\ ( { x } i^i { y } ) = (/) ) ) -> E. u e. ~P A E. v e. ~P A ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
27 6 11 13 15 17 26 syl113anc
 |-  ( ( ( A e. V /\ ( x e. A /\ y e. A ) ) /\ x =/= y ) -> E. u e. ~P A E. v e. ~P A ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) )
28 27 ex
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) ) -> ( x =/= y -> E. u e. ~P A E. v e. ~P A ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
29 28 ralrimivva
 |-  ( A e. V -> A. x e. A A. y e. A ( x =/= y -> E. u e. ~P A E. v e. ~P A ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) )
30 unipw
 |-  U. ~P A = A
31 30 eqcomi
 |-  A = U. ~P A
32 31 ishaus
 |-  ( ~P A e. Haus <-> ( ~P A e. Top /\ A. x e. A A. y e. A ( x =/= y -> E. u e. ~P A E. v e. ~P A ( x e. u /\ y e. v /\ ( u i^i v ) = (/) ) ) ) )
33 1 29 32 sylanbrc
 |-  ( A e. V -> ~P A e. Haus )