Step |
Hyp |
Ref |
Expression |
1 |
|
stdbdmet.1 |
β’ π· = ( π₯ β π , π¦ β π β¦ if ( ( π₯ πΆ π¦ ) β€ π
, ( π₯ πΆ π¦ ) , π
) ) |
2 |
|
simpll2 |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β π
β β* ) |
3 |
|
simpr1 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β π β π ) |
4 |
3
|
adantr |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β π β π ) |
5 |
|
simpr |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β π§ β π ) |
6 |
1
|
stdbdmetval |
β’ ( ( π
β β* β§ π β π β§ π§ β π ) β ( π π· π§ ) = if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) |
7 |
2 4 5 6
|
syl3anc |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( π π· π§ ) = if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) |
8 |
7
|
breq1d |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( ( π π· π§ ) < π β if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) < π ) ) |
9 |
|
simplr3 |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β π β€ π
) |
10 |
9
|
biantrud |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( π β€ ( π πΆ π§ ) β ( π β€ ( π πΆ π§ ) β§ π β€ π
) ) ) |
11 |
|
simpr2 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β π β β* ) |
12 |
11
|
adantr |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β π β β* ) |
13 |
|
simpl1 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β πΆ β ( βMet β π ) ) |
14 |
13
|
adantr |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β πΆ β ( βMet β π ) ) |
15 |
|
xmetcl |
β’ ( ( πΆ β ( βMet β π ) β§ π β π β§ π§ β π ) β ( π πΆ π§ ) β β* ) |
16 |
14 4 5 15
|
syl3anc |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( π πΆ π§ ) β β* ) |
17 |
|
xrlemin |
β’ ( ( π β β* β§ ( π πΆ π§ ) β β* β§ π
β β* ) β ( π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) β ( π β€ ( π πΆ π§ ) β§ π β€ π
) ) ) |
18 |
12 16 2 17
|
syl3anc |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) β ( π β€ ( π πΆ π§ ) β§ π β€ π
) ) ) |
19 |
10 18
|
bitr4d |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( π β€ ( π πΆ π§ ) β π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) ) |
20 |
19
|
notbid |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( Β¬ π β€ ( π πΆ π§ ) β Β¬ π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) ) |
21 |
|
xrltnle |
β’ ( ( ( π πΆ π§ ) β β* β§ π β β* ) β ( ( π πΆ π§ ) < π β Β¬ π β€ ( π πΆ π§ ) ) ) |
22 |
16 12 21
|
syl2anc |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( ( π πΆ π§ ) < π β Β¬ π β€ ( π πΆ π§ ) ) ) |
23 |
16 2
|
ifcld |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) β β* ) |
24 |
|
xrltnle |
β’ ( ( if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) β β* β§ π β β* ) β ( if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) < π β Β¬ π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) ) |
25 |
23 12 24
|
syl2anc |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) < π β Β¬ π β€ if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) ) ) |
26 |
20 22 25
|
3bitr4d |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( ( π πΆ π§ ) < π β if ( ( π πΆ π§ ) β€ π
, ( π πΆ π§ ) , π
) < π ) ) |
27 |
8 26
|
bitr4d |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β§ π§ β π ) β ( ( π π· π§ ) < π β ( π πΆ π§ ) < π ) ) |
28 |
27
|
rabbidva |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β { π§ β π β£ ( π π· π§ ) < π } = { π§ β π β£ ( π πΆ π§ ) < π } ) |
29 |
1
|
stdbdxmet |
β’ ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β π· β ( βMet β π ) ) |
30 |
29
|
adantr |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β π· β ( βMet β π ) ) |
31 |
|
blval |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π β β* ) β ( π ( ball β π· ) π ) = { π§ β π β£ ( π π· π§ ) < π } ) |
32 |
30 3 11 31
|
syl3anc |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β ( π ( ball β π· ) π ) = { π§ β π β£ ( π π· π§ ) < π } ) |
33 |
|
blval |
β’ ( ( πΆ β ( βMet β π ) β§ π β π β§ π β β* ) β ( π ( ball β πΆ ) π ) = { π§ β π β£ ( π πΆ π§ ) < π } ) |
34 |
13 3 11 33
|
syl3anc |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β ( π ( ball β πΆ ) π ) = { π§ β π β£ ( π πΆ π§ ) < π } ) |
35 |
28 32 34
|
3eqtr4d |
β’ ( ( ( πΆ β ( βMet β π ) β§ π
β β* β§ 0 < π
) β§ ( π β π β§ π β β* β§ π β€ π
) ) β ( π ( ball β π· ) π ) = ( π ( ball β πΆ ) π ) ) |