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