Metamath Proof Explorer

Theorem cncfmet

Description: Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007) (Revised by Mario Carneiro, 7-Sep-2015)

Ref Expression
Hypotheses cncfmet.1 ⊒ 𝐢 = ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) )
cncfmet.2 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) )
cncfmet.3 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
cncfmet.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
Assertion cncfmet ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( 𝐴 –cnβ†’ 𝐡 ) = ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cncfmet.1 ⊒ 𝐢 = ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) )
2 cncfmet.2 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) )
3 cncfmet.3 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
4 cncfmet.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
5 simplll ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ 𝐴 βŠ† β„‚ )
6 simprl ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ π‘₯ ∈ 𝐴 )
7 simprr ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ 𝑀 ∈ 𝐴 )
8 1 oveqi ⊒ ( π‘₯ 𝐢 𝑀 ) = ( π‘₯ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) 𝑀 )
9 ovres ⊒ ( ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) β†’ ( π‘₯ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) 𝑀 ) = ( π‘₯ ( abs ∘ βˆ’ ) 𝑀 ) )
10 8 9 eqtrid ⊒ ( ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) β†’ ( π‘₯ 𝐢 𝑀 ) = ( π‘₯ ( abs ∘ βˆ’ ) 𝑀 ) )
11 10 ad2ant2l ⊒ ( ( ( 𝐴 βŠ† β„‚ ∧ π‘₯ ∈ 𝐴 ) ∧ ( 𝐴 βŠ† β„‚ ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( π‘₯ 𝐢 𝑀 ) = ( π‘₯ ( abs ∘ βˆ’ ) 𝑀 ) )
12 ssel2 ⊒ ( ( 𝐴 βŠ† β„‚ ∧ π‘₯ ∈ 𝐴 ) β†’ π‘₯ ∈ β„‚ )
13 ssel2 ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝑀 ∈ 𝐴 ) β†’ 𝑀 ∈ β„‚ )
14 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
15 14 cnmetdval ⊒ ( ( π‘₯ ∈ β„‚ ∧ 𝑀 ∈ β„‚ ) β†’ ( π‘₯ ( abs ∘ βˆ’ ) 𝑀 ) = ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) )
16 12 13 15 syl2an ⊒ ( ( ( 𝐴 βŠ† β„‚ ∧ π‘₯ ∈ 𝐴 ) ∧ ( 𝐴 βŠ† β„‚ ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( π‘₯ ( abs ∘ βˆ’ ) 𝑀 ) = ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) )
17 11 16 eqtrd ⊒ ( ( ( 𝐴 βŠ† β„‚ ∧ π‘₯ ∈ 𝐴 ) ∧ ( 𝐴 βŠ† β„‚ ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( π‘₯ 𝐢 𝑀 ) = ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) )
18 5 6 5 7 17 syl22anc ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( π‘₯ 𝐢 𝑀 ) = ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) )
19 18 breq1d ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 ↔ ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 ) )
20 ffvelcdm ⊒ ( ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ π‘₯ ∈ 𝐴 ) β†’ ( 𝑓 β€˜ π‘₯ ) ∈ 𝐡 )
21 20 ad2ant2lr ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( 𝑓 β€˜ π‘₯ ) ∈ 𝐡 )
22 ffvelcdm ⊒ ( ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ 𝑀 ∈ 𝐴 ) β†’ ( 𝑓 β€˜ 𝑀 ) ∈ 𝐡 )
23 22 ad2ant2l ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( 𝑓 β€˜ 𝑀 ) ∈ 𝐡 )
24 2 oveqi ⊒ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) = ( ( 𝑓 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) ) ( 𝑓 β€˜ 𝑀 ) )
25 ovres ⊒ ( ( ( 𝑓 β€˜ π‘₯ ) ∈ 𝐡 ∧ ( 𝑓 β€˜ 𝑀 ) ∈ 𝐡 ) β†’ ( ( 𝑓 β€˜ π‘₯ ) ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) ) ( 𝑓 β€˜ 𝑀 ) ) = ( ( 𝑓 β€˜ π‘₯ ) ( abs ∘ βˆ’ ) ( 𝑓 β€˜ 𝑀 ) ) )
26 24 25 eqtrid ⊒ ( ( ( 𝑓 β€˜ π‘₯ ) ∈ 𝐡 ∧ ( 𝑓 β€˜ 𝑀 ) ∈ 𝐡 ) β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) = ( ( 𝑓 β€˜ π‘₯ ) ( abs ∘ βˆ’ ) ( 𝑓 β€˜ 𝑀 ) ) )
27 21 23 26 syl2anc ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) = ( ( 𝑓 β€˜ π‘₯ ) ( abs ∘ βˆ’ ) ( 𝑓 β€˜ 𝑀 ) ) )
28 simpllr ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ 𝐡 βŠ† β„‚ )
29 28 21 sseldd ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( 𝑓 β€˜ π‘₯ ) ∈ β„‚ )
30 28 23 sseldd ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( 𝑓 β€˜ 𝑀 ) ∈ β„‚ )
31 14 cnmetdval ⊒ ( ( ( 𝑓 β€˜ π‘₯ ) ∈ β„‚ ∧ ( 𝑓 β€˜ 𝑀 ) ∈ β„‚ ) β†’ ( ( 𝑓 β€˜ π‘₯ ) ( abs ∘ βˆ’ ) ( 𝑓 β€˜ 𝑀 ) ) = ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) )
32 29 30 31 syl2anc ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( 𝑓 β€˜ π‘₯ ) ( abs ∘ βˆ’ ) ( 𝑓 β€˜ 𝑀 ) ) = ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) )
33 27 32 eqtrd ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) = ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) )
34 33 breq1d ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ↔ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) )
35 19 34 imbi12d ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ ( π‘₯ ∈ 𝐴 ∧ 𝑀 ∈ 𝐴 ) ) β†’ ( ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
36 35 anassrs ⊒ ( ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ π‘₯ ∈ 𝐴 ) ∧ 𝑀 ∈ 𝐴 ) β†’ ( ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
37 36 ralbidva ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
38 37 rexbidv ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
39 38 ralbidv ⊒ ( ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) ∧ π‘₯ ∈ 𝐴 ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
40 39 ralbidva ⊒ ( ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ∧ 𝑓 : 𝐴 ⟢ 𝐡 ) β†’ ( βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ↔ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) )
41 40 pm5.32da ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ) ↔ ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) ) )
42 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
43 xmetres2 ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 𝐴 βŠ† β„‚ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( ∞Met β€˜ 𝐴 ) )
44 42 43 mpan ⊒ ( 𝐴 βŠ† β„‚ β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐴 Γ— 𝐴 ) ) ∈ ( ∞Met β€˜ 𝐴 ) )
45 1 44 eqeltrid ⊒ ( 𝐴 βŠ† β„‚ β†’ 𝐢 ∈ ( ∞Met β€˜ 𝐴 ) )
46 xmetres2 ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 𝐡 βŠ† β„‚ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) ) ∈ ( ∞Met β€˜ 𝐡 ) )
47 42 46 mpan ⊒ ( 𝐡 βŠ† β„‚ β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( 𝐡 Γ— 𝐡 ) ) ∈ ( ∞Met β€˜ 𝐡 ) )
48 2 47 eqeltrid ⊒ ( 𝐡 βŠ† β„‚ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) )
49 3 4 metcn ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝐴 ) ∧ 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) ) β†’ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
50 45 48 49 syl2an ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝑓 β€˜ π‘₯ ) 𝐷 ( 𝑓 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
51 elcncf ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( 𝑓 ∈ ( 𝐴 –cnβ†’ 𝐡 ) ↔ ( 𝑓 : 𝐴 ⟢ 𝐡 ∧ βˆ€ π‘₯ ∈ 𝐴 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝐴 ( ( abs β€˜ ( π‘₯ βˆ’ 𝑀 ) ) < 𝑧 β†’ ( abs β€˜ ( ( 𝑓 β€˜ π‘₯ ) βˆ’ ( 𝑓 β€˜ 𝑀 ) ) ) < 𝑦 ) ) ) )
52 41 50 51 3bitr4rd ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( 𝑓 ∈ ( 𝐴 –cnβ†’ 𝐡 ) ↔ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) )
53 52 eqrdv ⊒ ( ( 𝐴 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) β†’ ( 𝐴 –cnβ†’ 𝐡 ) = ( 𝐽 Cn 𝐾 ) )