Metamath Proof Explorer

Theorem metcnpi

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

Ref Expression
Hypotheses metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
Assertion metcnpi ( ( ( 𝐢 ∈ ( ∞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 metcnp ⊒ ( ( 𝐢 ∈ ( ∞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 𝐾 ) β€˜ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) β†’ βˆƒ π‘₯ ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑋 ( ( 𝑃 𝐢 𝑦 ) < π‘₯ β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑦 ) ) < 𝐴 ) )