Metamath Proof Explorer

Theorem elbigo2

Description: Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020)

Ref Expression
Assertion elbigo2 ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elbigo ⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
2 df-3an ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
3 1 2 bitri ⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
4 reex ⊢ ℝ ∈ V
5 4 4 pm3.2i ⊢ ( ℝ ∈ V ∧ ℝ ∈ V )
6 5 a1i ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( ℝ ∈ V ∧ ℝ ∈ V ) )
7 simpl ⊢ ( ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) → 𝐹 : 𝐵 ⟶ ℝ )
8 7 adantl ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐹 : 𝐵 ⟶ ℝ )
9 sstr2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ⊆ ℝ → 𝐵 ⊆ ℝ ) )
10 9 adantld ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → 𝐵 ⊆ ℝ ) )
11 10 adantl ⊢ ( ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → 𝐵 ⊆ ℝ ) )
12 11 impcom ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ⊆ ℝ )
13 elpm2r ⊢ ( ( ( ℝ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ ℝ ) ) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
14 6 8 12 13 syl12anc ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
15 simpl ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) )
16 elpm2r ⊢ ( ( ( ℝ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )
17 6 15 16 syl2anc ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )
18 ibar ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
19 18 bicomd ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) → ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
20 14 17 19 syl2anc ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
21 3 20 syl5bb ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
22 elin ⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) )
23 fdm ⊢ ( 𝐹 : 𝐵 ⟶ ℝ → dom 𝐹 = 𝐵 )
24 23 ad2antrl ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → dom 𝐹 = 𝐵 )
25 24 ad2antrr ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → dom 𝐹 = 𝐵 )
26 25 eleq2d ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐵 ) )
27 26 anbi1d ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ) )
28 elicopnf ⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) ) )
29 28 ad3antlr ⊢ ( ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) ) )
30 12 ad2antrr ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝐵 ⊆ ℝ )
31 30 sselda ⊢ ( ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ )
32 31 biantrurd ⊢ ( ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) ) )
33 29 32 bitr4d ⊢ ( ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ 𝑥 ≤ 𝑦 ) )
34 33 pm5.32da ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) ) )
35 27 34 bitrd ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) ) )
36 22 35 syl5bb ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) ) )
37 36 imbi1d ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
38 impexp ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
39 37 38 bitrdi ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) ) )
40 39 ralbidv2 ⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
41 40 rexbidva ⊢ ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
42 41 rexbidva ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
43 21 42 bitrd ⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )