Metamath Proof Explorer

Theorem o1of2

Description: Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Hypotheses o1of2.1 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → 𝑀 ∈ ℝ )
o1of2.2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 𝑅 𝑦 ) ∈ ℂ )
o1of2.3 ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) )
Assertion o1of2 ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1of2.1 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → 𝑀 ∈ ℝ )
2 o1of2.2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 𝑅 𝑦 ) ∈ ℂ )
3 o1of2.3 ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) )
4 o1f ⊢ ( 𝐹 ∈ 𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℂ )
5 o1bdd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) )
6 4 5 mpdan ⊢ ( 𝐹 ∈ 𝑂(1) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) )
7 6 adantr ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) )
8 o1f ⊢ ( 𝐺 ∈ 𝑂(1) → 𝐺 : dom 𝐺 ⟶ ℂ )
9 o1bdd ⊢ ( ( 𝐺 ∈ 𝑂(1) ∧ 𝐺 : dom 𝐺 ⟶ ℂ ) → ∃ 𝑏 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) )
10 8 9 mpdan ⊢ ( 𝐺 ∈ 𝑂(1) → ∃ 𝑏 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) )
11 10 adantl ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ∃ 𝑏 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) )
12 reeanv ⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ↔ ( ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑏 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
13 reeanv ⊢ ( ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
14 inss1 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹
15 ssralv ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹 → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ) )
16 14 15 ax-mp ⊢ ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) )
17 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
18 ssralv ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 → ( ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
19 17 18 ax-mp ⊢ ( ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) )
20 16 19 anim12i ⊢ ( ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
21 r19.26 ⊢ ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ↔ ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
22 20 21 sylibr ⊢ ( ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
23 anim12 ⊢ ( ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
24 simplrl ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝑎 ∈ ℝ )
25 24 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 𝑎 ∈ ℝ )
26 simplrr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝑏 ∈ ℝ )
27 26 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 𝑏 ∈ ℝ )
28 o1dm ⊢ ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ )
29 28 ad3antrrr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → dom 𝐹 ⊆ ℝ )
30 14 29 sstrid ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ⊆ ℝ )
31 30 sselda ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 𝑧 ∈ ℝ )
32 maxle ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 ↔ ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) ) )
33 25 27 31 32 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 ↔ ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) ) )
34 33 biimpd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) ) )
35 4 ad3antrrr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
36 14 sseli ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐹 )
37 ffvelcdm ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
38 35 36 37 syl2an ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
39 8 ad3antlr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝐺 : dom 𝐺 ⟶ ℂ )
40 17 sseli ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐺 )
41 ffvelcdm ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
42 39 40 41 syl2an ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
43 3 ralrimivva ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) )
44 43 ad2antlr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) )
45 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
46 45 breq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ 𝑥 ) ≤ 𝑚 ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) )
47 46 anbi1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ) )
48 fvoveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) )
49 48 breq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) ≤ 𝑀 ) )
50 47 49 imbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) ↔ ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) ≤ 𝑀 ) ) )
51 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ 𝑦 ) = ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
52 51 breq1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ 𝑦 ) ≤ 𝑛 ↔ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) )
53 52 anbi2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
54 oveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) )
55 54 fveq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) )
56 55 breq1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) ≤ 𝑀 ) )
57 53 56 imbi12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 𝑦 ) ) ≤ 𝑀 ) ↔ ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) ≤ 𝑀 ) ) )
58 50 57 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( abs ‘ 𝑥 ) ≤ 𝑚 ∧ ( abs ‘ 𝑦 ) ≤ 𝑛 ) → ( abs ‘ ( 𝑥 𝑅 𝑦 ) ) ≤ 𝑀 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) ≤ 𝑀 ) )
59 38 42 44 58 syl21anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) ≤ 𝑀 ) )
60 35 ffnd ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝐹 Fn dom 𝐹 )
61 39 ffnd ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝐺 Fn dom 𝐺 )
62 reex ⊢ ℝ ∈ V
63 ssexg ⊢ ( ( dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V ) → dom 𝐹 ∈ V )
64 29 62 63 sylancl ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → dom 𝐹 ∈ V )
65 dmexg ⊢ ( 𝐺 ∈ 𝑂(1) → dom 𝐺 ∈ V )
66 65 ad3antlr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → dom 𝐺 ∈ V )
67 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
68 eqidd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
69 eqidd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
70 60 61 64 66 67 68 69 ofval ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) )
71 70 fveq2d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) )
72 71 breq1d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) 𝑅 ( 𝐺 ‘ 𝑧 ) ) ) ≤ 𝑀 ) )
73 59 72 sylibrd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) )
74 34 73 imim12d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ( 𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) ) )
75 23 74 syl5 ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) ) )
76 75 ralimdva ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) ) )
77 2 adantl ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 𝑅 𝑦 ) ∈ ℂ )
78 77 35 39 64 66 67 off ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ )
79 26 24 ifcld ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ )
80 1 adantl ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → 𝑀 ∈ ℝ )
81 elo12r ⊢ ( ( ( ( 𝐹 ∘f 𝑅 𝐺 ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ ∧ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ ℝ ) ∧ ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) )
82 81 3expia ⊢ ( ( ( ( 𝐹 ∘f 𝑅 𝐺 ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ ∧ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ ℝ ) ∧ ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
83 78 30 79 80 82 syl22anc ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑧 ) ) ≤ 𝑀 ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
84 76 83 syld ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
85 22 84 syl5 ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ) → ( ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
86 85 rexlimdvva ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
87 13 86 biimtrrid ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( ( ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
88 87 rexlimdvva ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
89 12 88 biimtrrid ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( ( ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑎 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑚 ) ∧ ∃ 𝑏 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ dom 𝐺 ( 𝑏 ≤ 𝑧 → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) ) )
90 7 11 89 mp2and ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ∈ 𝑂(1) ) → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ 𝑂(1) )