Metamath Proof Explorer

Theorem metcnp2

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . The distance arguments are swapped compared to metcnp (and Munkres' metcn ) for compatibility with df-lm . Definition 1.3-3 of Kreyszig p. 20. (Contributed by NM, 4-Jun-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metcnp2 ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 2 metcnp ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
4 simpl1 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
5 4 ad2antrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
6 simpl3 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝑃 ∈ 𝑋 )
7 6 ad2antrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
8 simpr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
9 xmetsym ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑤 ) = ( 𝑤 𝐶 𝑃 ) )
10 5 7 8 9 syl3anc ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑤 ) = ( 𝑤 𝐶 𝑃 ) )
11 10 breq1d ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 ↔ ( 𝑤 𝐶 𝑃 ) < 𝑧 ) )
12 simpl2 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
13 12 ad2antrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
14 simpllr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
15 14 7 ffvelrnd ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
16 14 8 ffvelrnd ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑌 )
17 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) )
18 13 15 16 17 syl3anc ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) )
19 18 breq1d ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) )
20 11 19 imbi12d ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ↔ ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) )
21 20 ralbidva ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) )
22 21 anassrs ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) )
23 22 rexbidva ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) )
24 23 ralbidva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) )
25 24 pm5.32da ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) ) )
26 3 25 bitrd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑤 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝑦 ) ) ) )