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	bitrid	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( 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	bitrid	⊢ ( ( ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ ( 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	⊢ ( ( ( 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐹 : 𝐵 ⟶ ℝ ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )