This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metcnpi2

Description: Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 . (Contributed by NM, 16-Dec-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metcnpi2 ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 simpr ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
4 simpll ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
5 simplr ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 6 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
8 7 adantl ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑃 ∈ ∪ 𝐽 )
9 1 mopnuni ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
10 9 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑋 = ∪ 𝐽 )
11 8 10 eleqtrrd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑃 ∈ 𝑋 )
12 1 2 metcnp2 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) ) ) )
13 4 5 11 12 syl3anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) ) ) )
14 3 13 mpbid ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) ) )
15 breq2 ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ↔ ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) )
16 15 imbi2d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) ↔ ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) )
17 16 rexralbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) )
18 17 rspccv ⊢ ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑧 ) → ( 𝐴 ∈ ℝ+ → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) )
19 14 18 simpl2im ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → ( 𝐴 ∈ ℝ+ → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) )
20 19 impr ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) )