Metamath Proof Explorer


Theorem methaus

Description: The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis methaus.1
|- J = ( MetOpen ` D )
Assertion methaus
|- ( D e. ( *Met ` X ) -> J e. Haus )

Proof

Step Hyp Ref Expression
1 methaus.1
 |-  J = ( MetOpen ` D )
2 1 mopnex
 |-  ( D e. ( *Met ` X ) -> E. d e. ( Met ` X ) J = ( MetOpen ` d ) )
3 metxmet
 |-  ( d e. ( Met ` X ) -> d e. ( *Met ` X ) )
4 3 ad2antrr
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> d e. ( *Met ` X ) )
5 simplrl
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> x e. X )
6 metcl
 |-  ( ( d e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x d y ) e. RR )
7 6 3expb
 |-  ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x d y ) e. RR )
8 7 adantr
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( x d y ) e. RR )
9 metgt0
 |-  ( ( d e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x =/= y <-> 0 < ( x d y ) ) )
10 9 3expb
 |-  ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x =/= y <-> 0 < ( x d y ) ) )
11 10 biimpa
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> 0 < ( x d y ) )
12 8 11 elrpd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( x d y ) e. RR+ )
13 12 rphalfcld
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( x d y ) / 2 ) e. RR+ )
14 13 rpxrd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( x d y ) / 2 ) e. RR* )
15 eqid
 |-  ( MetOpen ` d ) = ( MetOpen ` d )
16 15 blopn
 |-  ( ( d e. ( *Met ` X ) /\ x e. X /\ ( ( x d y ) / 2 ) e. RR* ) -> ( x ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) )
17 4 5 14 16 syl3anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( x ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) )
18 simplrr
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> y e. X )
19 15 blopn
 |-  ( ( d e. ( *Met ` X ) /\ y e. X /\ ( ( x d y ) / 2 ) e. RR* ) -> ( y ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) )
20 4 18 14 19 syl3anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( y ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) )
21 blcntr
 |-  ( ( d e. ( *Met ` X ) /\ x e. X /\ ( ( x d y ) / 2 ) e. RR+ ) -> x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) )
22 4 5 13 21 syl3anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) )
23 blcntr
 |-  ( ( d e. ( *Met ` X ) /\ y e. X /\ ( ( x d y ) / 2 ) e. RR+ ) -> y e. ( y ( ball ` d ) ( ( x d y ) / 2 ) ) )
24 4 18 13 23 syl3anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> y e. ( y ( ball ` d ) ( ( x d y ) / 2 ) ) )
25 13 rpred
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( x d y ) / 2 ) e. RR )
26 25 25 rexaddd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( ( x d y ) / 2 ) +e ( ( x d y ) / 2 ) ) = ( ( ( x d y ) / 2 ) + ( ( x d y ) / 2 ) ) )
27 8 recnd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( x d y ) e. CC )
28 27 2halvesd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( ( x d y ) / 2 ) + ( ( x d y ) / 2 ) ) = ( x d y ) )
29 26 28 eqtrd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( ( x d y ) / 2 ) +e ( ( x d y ) / 2 ) ) = ( x d y ) )
30 8 leidd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( x d y ) <_ ( x d y ) )
31 29 30 eqbrtrd
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( ( x d y ) / 2 ) +e ( ( x d y ) / 2 ) ) <_ ( x d y ) )
32 bldisj
 |-  ( ( ( d e. ( *Met ` X ) /\ x e. X /\ y e. X ) /\ ( ( ( x d y ) / 2 ) e. RR* /\ ( ( x d y ) / 2 ) e. RR* /\ ( ( ( x d y ) / 2 ) +e ( ( x d y ) / 2 ) ) <_ ( x d y ) ) ) -> ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) = (/) )
33 4 5 18 14 14 31 32 syl33anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) = (/) )
34 eleq2
 |-  ( m = ( x ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( x e. m <-> x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) ) )
35 ineq1
 |-  ( m = ( x ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( m i^i n ) = ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) )
36 35 eqeq1d
 |-  ( m = ( x ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( ( m i^i n ) = (/) <-> ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) = (/) ) )
37 34 36 3anbi13d
 |-  ( m = ( x ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) <-> ( x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) /\ y e. n /\ ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) = (/) ) ) )
38 eleq2
 |-  ( n = ( y ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( y e. n <-> y e. ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) )
39 ineq2
 |-  ( n = ( y ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) = ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) )
40 39 eqeq1d
 |-  ( n = ( y ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) = (/) <-> ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) = (/) ) )
41 38 40 3anbi23d
 |-  ( n = ( y ( ball ` d ) ( ( x d y ) / 2 ) ) -> ( ( x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) /\ y e. n /\ ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i n ) = (/) ) <-> ( x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) /\ y e. ( y ( ball ` d ) ( ( x d y ) / 2 ) ) /\ ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) = (/) ) ) )
42 37 41 rspc2ev
 |-  ( ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) /\ ( y ( ball ` d ) ( ( x d y ) / 2 ) ) e. ( MetOpen ` d ) /\ ( x e. ( x ( ball ` d ) ( ( x d y ) / 2 ) ) /\ y e. ( y ( ball ` d ) ( ( x d y ) / 2 ) ) /\ ( ( x ( ball ` d ) ( ( x d y ) / 2 ) ) i^i ( y ( ball ` d ) ( ( x d y ) / 2 ) ) ) = (/) ) ) -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
43 17 20 22 24 33 42 syl113anc
 |-  ( ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) /\ x =/= y ) -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
44 43 ex
 |-  ( ( d e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x =/= y -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
45 44 ralrimivva
 |-  ( d e. ( Met ` X ) -> A. x e. X A. y e. X ( x =/= y -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
46 15 mopntopon
 |-  ( d e. ( *Met ` X ) -> ( MetOpen ` d ) e. ( TopOn ` X ) )
47 ishaus2
 |-  ( ( MetOpen ` d ) e. ( TopOn ` X ) -> ( ( MetOpen ` d ) e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
48 3 46 47 3syl
 |-  ( d e. ( Met ` X ) -> ( ( MetOpen ` d ) e. Haus <-> A. x e. X A. y e. X ( x =/= y -> E. m e. ( MetOpen ` d ) E. n e. ( MetOpen ` d ) ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
49 45 48 mpbird
 |-  ( d e. ( Met ` X ) -> ( MetOpen ` d ) e. Haus )
50 eleq1
 |-  ( J = ( MetOpen ` d ) -> ( J e. Haus <-> ( MetOpen ` d ) e. Haus ) )
51 49 50 syl5ibrcom
 |-  ( d e. ( Met ` X ) -> ( J = ( MetOpen ` d ) -> J e. Haus ) )
52 51 rexlimiv
 |-  ( E. d e. ( Met ` X ) J = ( MetOpen ` d ) -> J e. Haus )
53 2 52 syl
 |-  ( D e. ( *Met ` X ) -> J e. Haus )