| Step |
Hyp |
Ref |
Expression |
| 1 |
|
metcn.2 |
⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) |
| 2 |
|
metcn.4 |
⊢ 𝐾 = ( MetOpen ‘ 𝐷 ) |
| 3 |
1
|
mopntopon |
⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
| 4 |
3
|
3ad2ant1 |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
| 5 |
2
|
mopnval |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
| 6 |
5
|
3ad2ant2 |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
| 7 |
2
|
mopntopon |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
| 8 |
7
|
3ad2ant2 |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
| 9 |
|
simp3 |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 ) |
| 10 |
4 6 8 9
|
tgcnp |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) ) |
| 11 |
|
simpll2 |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) |
| 12 |
|
simplr |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
| 13 |
|
simpll3 |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑃 ∈ 𝑋 ) |
| 14 |
12 13
|
ffvelcdmd |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ) |
| 15 |
|
simpr |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ ) |
| 16 |
|
blcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) |
| 17 |
11 14 15 16
|
syl3anc |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) |
| 18 |
|
rpxr |
⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* ) |
| 19 |
18
|
adantl |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ* ) |
| 20 |
|
blelrn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) ) |
| 21 |
11 14 19 20
|
syl3anc |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) ) |
| 22 |
|
eleq2 |
⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 23 |
|
sseq2 |
⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 24 |
23
|
anbi2d |
⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |
| 25 |
24
|
rexbidv |
⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |
| 26 |
22 25
|
imbi12d |
⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) ) |
| 27 |
26
|
rspcv |
⊢ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) ) |
| 28 |
21 27
|
syl |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) ) |
| 29 |
17 28
|
mpid |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |
| 30 |
|
simpl1 |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 31 |
30
|
ad2antrr |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 32 |
|
simplrr |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝑣 ∈ 𝐽 ) |
| 33 |
|
simpr |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝑃 ∈ 𝑣 ) |
| 34 |
1
|
mopni2 |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ∧ 𝑃 ∈ 𝑣 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 ) |
| 35 |
31 32 33 34
|
syl3anc |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 ) |
| 36 |
|
sstr2 |
⊢ ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( 𝐹 “ 𝑣 ) → ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 37 |
|
imass2 |
⊢ ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( 𝐹 “ 𝑣 ) ) |
| 38 |
36 37
|
syl11 |
⊢ ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 39 |
38
|
reximdv |
⊢ ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 40 |
35 39
|
syl5com |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 41 |
40
|
expimpd |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 42 |
41
|
expr |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑣 ∈ 𝐽 → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |
| 43 |
42
|
rexlimdv |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 44 |
29 43
|
syld |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 45 |
44
|
ralrimdva |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 46 |
|
simpl2 |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) |
| 47 |
|
blss |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) |
| 48 |
47
|
3expib |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ) |
| 49 |
46 48
|
syl |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ) |
| 50 |
|
r19.29r |
⊢ ( ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑦 ∈ ℝ+ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 51 |
30
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 52 |
13
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑃 ∈ 𝑋 ) |
| 53 |
|
rpxr |
⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ* ) |
| 54 |
53
|
ad2antrl |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑧 ∈ ℝ* ) |
| 55 |
1
|
blopn |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 ) |
| 56 |
51 52 54 55
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 ) |
| 57 |
|
simprl |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑧 ∈ ℝ+ ) |
| 58 |
|
blcntr |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) |
| 59 |
51 52 57 58
|
syl3anc |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) |
| 60 |
|
sstr |
⊢ ( ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) |
| 61 |
60
|
ad2ant2l |
⊢ ( ( ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ∧ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) |
| 62 |
61
|
ancoms |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) |
| 63 |
|
eleq2 |
⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝑃 ∈ 𝑣 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ) |
| 64 |
|
imaeq2 |
⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝐹 “ 𝑣 ) = ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ) |
| 65 |
64
|
sseq1d |
⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) ) |
| 66 |
63 65
|
anbi12d |
⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) ) ) |
| 67 |
66
|
rspcev |
⊢ ( ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) |
| 68 |
56 59 62 67
|
syl12anc |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) |
| 69 |
68
|
expr |
⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) |
| 70 |
69
|
rexlimdva |
⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) → ( ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) |
| 71 |
70
|
expimpd |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) |
| 72 |
71
|
rexlimdva |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑦 ∈ ℝ+ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) |
| 73 |
50 72
|
syl5 |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) |
| 74 |
73
|
expd |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) |
| 75 |
49 74
|
syld |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) |
| 76 |
75
|
com23 |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) |
| 77 |
76
|
exp4a |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) ) |
| 78 |
77
|
ralrimdv |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) |
| 79 |
45 78
|
impbid |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) |
| 80 |
79
|
pm5.32da |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |
| 81 |
10 80
|
bitrd |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) |