| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imasf1obl.u |
⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) ) |
| 2 |
|
imasf1obl.v |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) |
| 3 |
|
imasf1obl.f |
⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) |
| 4 |
|
imasf1oxms.r |
⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp ) |
| 5 |
|
eqid |
⊢ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) |
| 6 |
|
eqid |
⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 ) |
| 7 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
| 8 |
|
eqid |
⊢ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) |
| 9 |
7 8
|
xmsxmet |
⊢ ( 𝑅 ∈ ∞MetSp → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) ) |
| 10 |
4 9
|
syl |
⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) ) |
| 11 |
2
|
sqxpeqd |
⊢ ( 𝜑 → ( 𝑉 × 𝑉 ) = ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) |
| 12 |
11
|
reseq2d |
⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) |
| 13 |
2
|
fveq2d |
⊢ ( 𝜑 → ( ∞Met ‘ 𝑉 ) = ( ∞Met ‘ ( Base ‘ 𝑅 ) ) ) |
| 14 |
10 12 13
|
3eltr4d |
⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) ) |
| 15 |
1 2 3 4 5 6 14
|
imasf1oxmet |
⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) ) |
| 16 |
|
f1ofo |
⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –onto→ 𝐵 ) |
| 17 |
3 16
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 ) |
| 18 |
1 2 17 4
|
imasbas |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) ) |
| 19 |
18
|
fveq2d |
⊢ ( 𝜑 → ( ∞Met ‘ 𝐵 ) = ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ) |
| 20 |
15 19
|
eleqtrd |
⊢ ( 𝜑 → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ) |
| 21 |
|
ssid |
⊢ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 ) |
| 22 |
|
xmetres2 |
⊢ ( ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ∧ ( Base ‘ 𝑈 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ) |
| 23 |
20 21 22
|
sylancl |
⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ) |
| 24 |
|
eqid |
⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 ) |
| 25 |
|
eqid |
⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 ) |
| 26 |
1 2 17 4 24 25
|
imastopn |
⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ) |
| 27 |
24 7 8
|
xmstopn |
⊢ ( 𝑅 ∈ ∞MetSp → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ) |
| 28 |
4 27
|
syl |
⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ) |
| 29 |
12
|
fveq2d |
⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ) |
| 30 |
28 29
|
eqtr4d |
⊢ ( 𝜑 → ( TopOpen ‘ 𝑅 ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) |
| 31 |
30
|
oveq1d |
⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) |
| 32 |
|
blbas |
⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ) |
| 33 |
14 32
|
syl |
⊢ ( 𝜑 → ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ) |
| 34 |
|
unirnbl |
⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = 𝑉 ) |
| 35 |
|
f1oeq2 |
⊢ ( ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = 𝑉 → ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) ) |
| 36 |
14 34 35
|
3syl |
⊢ ( 𝜑 → ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ↔ 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) ) |
| 37 |
3 36
|
mpbird |
⊢ ( 𝜑 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ) |
| 38 |
|
eqid |
⊢ ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) |
| 39 |
38
|
tgqtop |
⊢ ( ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ∧ 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 ) → ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) ) |
| 40 |
33 37 39
|
syl2anc |
⊢ ( 𝜑 → ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) ) |
| 41 |
|
eqid |
⊢ ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) |
| 42 |
41
|
mopnval |
⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) |
| 43 |
14 42
|
syl |
⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) = ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) |
| 44 |
43
|
oveq1d |
⊢ ( 𝜑 → ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ( ( topGen ‘ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) qTop 𝐹 ) ) |
| 45 |
|
eqid |
⊢ ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( MetOpen ‘ ( dist ‘ 𝑈 ) ) |
| 46 |
45
|
mopnval |
⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) |
| 47 |
15 46
|
syl |
⊢ ( 𝜑 → ( MetOpen ‘ ( dist ‘ 𝑈 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) |
| 48 |
|
xmetf |
⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) → ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* ) |
| 49 |
20 48
|
syl |
⊢ ( 𝜑 → ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* ) |
| 50 |
|
ffn |
⊢ ( ( dist ‘ 𝑈 ) : ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ⟶ ℝ* → ( dist ‘ 𝑈 ) Fn ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) |
| 51 |
|
fnresdm |
⊢ ( ( dist ‘ 𝑈 ) Fn ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( dist ‘ 𝑈 ) ) |
| 52 |
49 50 51
|
3syl |
⊢ ( 𝜑 → ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( dist ‘ 𝑈 ) ) |
| 53 |
52
|
fveq2d |
⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) = ( MetOpen ‘ ( dist ‘ 𝑈 ) ) ) |
| 54 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) |
| 55 |
|
f1of1 |
⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 : 𝑉 –1-1→ 𝐵 ) |
| 56 |
54 55
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –1-1→ 𝐵 ) |
| 57 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 |
| 58 |
|
f1odm |
⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → dom 𝐹 = 𝑉 ) |
| 59 |
54 58
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → dom 𝐹 = 𝑉 ) |
| 60 |
57 59
|
sseqtrid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑉 ) |
| 61 |
14
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) ) |
| 62 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑦 ∈ 𝑉 ) |
| 63 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑟 ∈ ℝ* ) |
| 64 |
|
blssm |
⊢ ( ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 ) |
| 65 |
61 62 63 64
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 ) |
| 66 |
|
f1imaeq |
⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝐵 ∧ ( ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑉 ∧ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ⊆ 𝑉 ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ) |
| 67 |
56 60 65 66
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ) |
| 68 |
54 16
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝐹 : 𝑉 –onto→ 𝐵 ) |
| 69 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑥 ⊆ 𝐵 ) |
| 70 |
|
foimacnv |
⊢ ( ( 𝐹 : 𝑉 –onto→ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 ) |
| 71 |
68 69 70
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 ) |
| 72 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑈 = ( 𝐹 “s 𝑅 ) ) |
| 73 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑉 = ( Base ‘ 𝑅 ) ) |
| 74 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → 𝑅 ∈ ∞MetSp ) |
| 75 |
72 73 54 74 5 6 61 62 63
|
imasf1obl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ) |
| 76 |
75
|
eqcomd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) |
| 77 |
71 76
|
eqeq12d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 78 |
67 77
|
bitr3d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) ) → ( ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 79 |
78
|
2rexbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 80 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝑉 –1-1-onto→ 𝐵 ) |
| 81 |
|
f1ofn |
⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝐵 → 𝐹 Fn 𝑉 ) |
| 82 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) |
| 83 |
82
|
eqeq2d |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 84 |
83
|
rexbidv |
⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 85 |
84
|
rexrn |
⊢ ( 𝐹 Fn 𝑉 → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 86 |
80 81 85
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* 𝑥 = ( ( 𝐹 ‘ 𝑦 ) ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 87 |
|
forn |
⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 ) |
| 88 |
80 16 87
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ran 𝐹 = 𝐵 ) |
| 89 |
88
|
rexeqdv |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑧 ∈ ran 𝐹 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 90 |
79 86 89
|
3bitr2d |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 91 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) ) |
| 92 |
|
blrn |
⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ∈ ( ∞Met ‘ 𝑉 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ) |
| 93 |
91 92
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ 𝑥 ) = ( 𝑦 ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) 𝑟 ) ) ) |
| 94 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) ) |
| 95 |
|
blrn |
⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 96 |
94 95
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑧 ( ball ‘ ( dist ‘ 𝑈 ) ) 𝑟 ) ) ) |
| 97 |
90 93 96
|
3bitr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ↔ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) |
| 98 |
97
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) ) |
| 99 |
|
f1ofo |
⊢ ( 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –1-1-onto→ 𝐵 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 ) |
| 100 |
37 99
|
syl |
⊢ ( 𝜑 → 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 ) |
| 101 |
38
|
elqtop2 |
⊢ ( ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ∈ TopBases ∧ 𝐹 : ∪ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) –onto→ 𝐵 ) → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) ) |
| 102 |
33 100 101
|
syl2anc |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) ) ) ) |
| 103 |
|
blf |
⊢ ( ( dist ‘ 𝑈 ) ∈ ( ∞Met ‘ 𝐵 ) → ( ball ‘ ( dist ‘ 𝑈 ) ) : ( 𝐵 × ℝ* ) ⟶ 𝒫 𝐵 ) |
| 104 |
|
frn |
⊢ ( ( ball ‘ ( dist ‘ 𝑈 ) ) : ( 𝐵 × ℝ* ) ⟶ 𝒫 𝐵 → ran ( ball ‘ ( dist ‘ 𝑈 ) ) ⊆ 𝒫 𝐵 ) |
| 105 |
15 103 104
|
3syl |
⊢ ( 𝜑 → ran ( ball ‘ ( dist ‘ 𝑈 ) ) ⊆ 𝒫 𝐵 ) |
| 106 |
105
|
sseld |
⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) → 𝑥 ∈ 𝒫 𝐵 ) ) |
| 107 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵 ) |
| 108 |
106 107
|
syl6 |
⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) → 𝑥 ⊆ 𝐵 ) ) |
| 109 |
108
|
pm4.71rd |
⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) ) |
| 110 |
98 102 109
|
3bitr4d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ↔ 𝑥 ∈ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) |
| 111 |
110
|
eqrdv |
⊢ ( 𝜑 → ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) |
| 112 |
111
|
fveq2d |
⊢ ( 𝜑 → ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) = ( topGen ‘ ran ( ball ‘ ( dist ‘ 𝑈 ) ) ) ) |
| 113 |
47 53 112
|
3eqtr4d |
⊢ ( 𝜑 → ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) = ( topGen ‘ ( ran ( ball ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) ) ) |
| 114 |
40 44 113
|
3eqtr4d |
⊢ ( 𝜑 → ( ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) ) qTop 𝐹 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) ) |
| 115 |
26 31 114
|
3eqtrd |
⊢ ( 𝜑 → ( TopOpen ‘ 𝑈 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) ) |
| 116 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
| 117 |
|
eqid |
⊢ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) = ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) |
| 118 |
25 116 117
|
isxms2 |
⊢ ( 𝑈 ∈ ∞MetSp ↔ ( ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑈 ) ) ∧ ( TopOpen ‘ 𝑈 ) = ( MetOpen ‘ ( ( dist ‘ 𝑈 ) ↾ ( ( Base ‘ 𝑈 ) × ( Base ‘ 𝑈 ) ) ) ) ) ) |
| 119 |
23 115 118
|
sylanbrc |
⊢ ( 𝜑 → 𝑈 ∈ ∞MetSp ) |