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 )