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 vsnex 
 |-  { 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 vsnex 
 |-  { 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 )