Step |
Hyp |
Ref |
Expression |
1 |
|
metcn.2 |
⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) |
2 |
|
metcn.4 |
⊢ 𝐾 = ( MetOpen ‘ 𝐷 ) |
3 |
1
|
mopntopon |
⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
4 |
2
|
mopntopon |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
5 |
|
cncnp |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) ) |
7 |
|
simplr |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
8 |
1 2
|
metcnp |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) ) |
9 |
8
|
ad4ant124 |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) ) |
10 |
7 9
|
mpbirand |
⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) |
11 |
10
|
ralbidva |
⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) |
12 |
11
|
pm5.32da |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) ) |
13 |
6 12
|
bitrd |
⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) ) |