Metamath Proof Explorer

Theorem rlimcn2

Description: Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses rlimcn2.1a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
rlimcn2.1b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑌 )
rlimcn2.2a ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
rlimcn2.2b ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
rlimcn2.3a ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 )
rlimcn2.3b ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝑆 )
rlimcn2.4 ⊢ ( 𝜑 → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
rlimcn2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
Assertion rlimcn2 ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ ( 𝐵 𝐹 𝐶 ) ) ⇝𝑟 ( 𝑅 𝐹 𝑆 ) )

Proof

Step Hyp Ref Expression
1 rlimcn2.1a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
2 rlimcn2.1b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑌 )
3 rlimcn2.2a ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
4 rlimcn2.2b ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
5 rlimcn2.3a ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 )
6 rlimcn2.3b ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝑆 )
7 rlimcn2.4 ⊢ ( 𝜑 → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
8 rlimcn2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
9 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑋 )
10 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑋 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 )
13 10 11 12 rlimi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ∃ 𝑎 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) )
14 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐶 ∈ 𝑌 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ∀ 𝑧 ∈ 𝐴 𝐶 ∈ 𝑌 )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → 𝑠 ∈ ℝ+ )
17 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝑆 )
18 15 16 17 rlimi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) )
19 reeanv ⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ↔ ( ∃ 𝑎 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) )
20 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ↔ ( ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) )
21 anim12 ⊢ ( ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) )
22 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
23 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑏 ∈ ℝ )
24 eqid ⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐵 )
25 24 1 dmmptd ⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
26 rlimss ⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
27 5 26 syl ⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
28 25 27 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
30 29 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
31 maxle ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 ↔ ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) ) )
32 22 23 30 31 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 ↔ ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) ) )
33 32 imbi1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ↔ ( ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ) )
34 21 33 syl5ibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ) )
35 34 ralimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) ) )
36 ifcl ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ )
37 36 ancoms ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ )
38 37 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ )
39 1 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
40 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑌 )
41 39 40 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ) )
42 fvoveq1 ⊢ ( 𝑢 = 𝐵 → ( abs ‘ ( 𝑢 − 𝑅 ) ) = ( abs ‘ ( 𝐵 − 𝑅 ) ) )
43 42 breq1d ⊢ ( 𝑢 = 𝐵 → ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ↔ ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) )
44 43 anbi1d ⊢ ( 𝑢 = 𝐵 → ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) ↔ ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) ) )
45 oveq1 ⊢ ( 𝑢 = 𝐵 → ( 𝑢 𝐹 𝑣 ) = ( 𝐵 𝐹 𝑣 ) )
46 45 fvoveq1d ⊢ ( 𝑢 = 𝐵 → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) = ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) )
47 46 breq1d ⊢ ( 𝑢 = 𝐵 → ( ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
48 44 47 imbi12d ⊢ ( 𝑢 = 𝐵 → ( ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ↔ ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
49 fvoveq1 ⊢ ( 𝑣 = 𝐶 → ( abs ‘ ( 𝑣 − 𝑆 ) ) = ( abs ‘ ( 𝐶 − 𝑆 ) ) )
50 49 breq1d ⊢ ( 𝑣 = 𝐶 → ( ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ↔ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) )
51 50 anbi2d ⊢ ( 𝑣 = 𝐶 → ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) ↔ ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) )
52 oveq2 ⊢ ( 𝑣 = 𝐶 → ( 𝐵 𝐹 𝑣 ) = ( 𝐵 𝐹 𝐶 ) )
53 52 fvoveq1d ⊢ ( 𝑣 = 𝐶 → ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) = ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) )
54 53 breq1d ⊢ ( 𝑣 = 𝐶 → ( ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
55 51 54 imbi12d ⊢ ( 𝑣 = 𝐶 → ( ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝐵 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ↔ ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
56 48 55 rspc2va ⊢ ( ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
57 41 56 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
58 57 imim2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
59 58 an32s ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
60 59 ralimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
61 60 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
62 breq1 ⊢ ( 𝑐 = if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) → ( 𝑐 ≤ 𝑧 ↔ if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 ) )
63 62 rspceaimv ⊢ ( ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
64 38 61 63 syl6an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
65 64 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ( ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
66 65 com23 ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
67 35 66 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
68 20 67 syl5bir ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ( ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
69 68 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
70 19 69 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( ( ∃ 𝑎 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝑅 ) ) < 𝑟 ) ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐶 − 𝑆 ) ) < 𝑠 ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) ) )
71 13 18 70 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
72 71 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
73 72 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
74 8 73 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
75 74 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
76 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
77 76 1 2 fovrnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐵 𝐹 𝐶 ) ∈ ℂ )
78 77 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ( 𝐵 𝐹 𝐶 ) ∈ ℂ )
79 7 3 4 fovrnd ⊢ ( 𝜑 → ( 𝑅 𝐹 𝑆 ) ∈ ℂ )
80 78 28 79 rlim2 ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐵 𝐹 𝐶 ) ) ⇝𝑟 ( 𝑅 𝐹 𝑆 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑐 ≤ 𝑧 → ( abs ‘ ( ( 𝐵 𝐹 𝐶 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) ) )
81 75 80 mpbird ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ ( 𝐵 𝐹 𝐶 ) ) ⇝𝑟 ( 𝑅 𝐹 𝑆 ) )