Theorem elbigo2 44605

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

Assertion

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

Distinct variable groups:   𝑥,𝐺,𝑚,𝑦   𝑚,𝐹,𝑥,𝑦   𝐴,𝑚,𝑥,𝑦   𝐵,𝑚,𝑥,𝑦

Proof of Theorem elbigo2

Step	Hyp	Ref	Expression
1		elbigo 44604	. . . 4 ⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
2		df-3an 1085	. . . 4 ⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
3	1, 2	bitri 277	. . 3 ⊢ (𝐹 ∈ (Ο‘𝐺) ↔ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
4		reex 10622	. . . . . . 7 ⊢ ℝ ∈ V
5	4, 4	pm3.2i 473	. . . . . 6 ⊢ (ℝ ∈ V ∧ ℝ ∈ V)
6	5	a1i 11	. . . . 5 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (ℝ ∈ V ∧ ℝ ∈ V))
7		simpl 485	. . . . . 6 ⊢ ((𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) → 𝐹:𝐵⟶ℝ)
8	7	adantl 484	. . . . 5 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → 𝐹:𝐵⟶ℝ)
9		sstr2 3974	. . . . . . . 8 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ ℝ → 𝐵 ⊆ ℝ))
10	9	adantld 493	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐴 → ((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐵 ⊆ ℝ))
11	10	adantl 484	. . . . . 6 ⊢ ((𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) → ((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → 𝐵 ⊆ ℝ))
12	11	impcom 410	. . . . 5 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ⊆ ℝ)
13		elpm2r 8418	. . . . 5 ⊢ (((ℝ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ ℝ)) → 𝐹 ∈ (ℝ ↑pm ℝ))
14	6, 8, 12, 13	syl12anc 834	. . . 4 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → 𝐹 ∈ (ℝ ↑pm ℝ))
15		simpl 485	. . . . 5 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ))
16		elpm2r 8418	. . . . 5 ⊢ (((ℝ ∈ V ∧ ℝ ∈ V) ∧ (𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ)) → 𝐺 ∈ (ℝ ↑pm ℝ))
17	6, 15, 16	syl2anc 586	. . . 4 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → 𝐺 ∈ (ℝ ↑pm ℝ))
18		ibar 531	. . . . 5 ⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
19	18	bicomd 225	. . . 4 ⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) → (((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
20	14, 17, 19	syl2anc 586	. . 3 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ)) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
21	3, 20	syl5bb 285	. 2 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
22		elin 4169	. . . . . . . 8 ⊢ (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)))
23		fdm 6517	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵⟶ℝ → dom 𝐹 = 𝐵)
24	23	ad2antrl 726	. . . . . . . . . . . 12 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → dom 𝐹 = 𝐵)
25	24	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → dom 𝐹 = 𝐵)
26	25	eleq2d 2898	. . . . . . . . . 10 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐵))
27	26	anbi1d 631	. . . . . . . . 9 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ (𝑥[,)+∞))))
28		elicopnf 12827	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦)))
29	28	ad3antlr 729	. . . . . . . . . . 11 ⊢ ((((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦)))
30	12	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → 𝐵 ⊆ ℝ)
31	30	sselda 3967	. . . . . . . . . . . 12 ⊢ ((((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ)
32	31	biantrurd 535	. . . . . . . . . . 11 ⊢ ((((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑦 ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦)))
33	29, 32	bitr4d 284	. . . . . . . . . 10 ⊢ ((((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ (𝑥[,)+∞) ↔ 𝑥 ≤ 𝑦))
34	33	pm5.32da 581	. . . . . . . . 9 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦)))
35	27, 34	bitrd 281	. . . . . . . 8 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦)))
36	22, 35	syl5bb 285	. . . . . . 7 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦)))
37	36	imbi1d 344	. . . . . 6 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
38		impexp 453	. . . . . 6 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ (𝑦 ∈ 𝐵 → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
39	37, 38	syl6bb 289	. . . . 5 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ (𝑦 ∈ 𝐵 → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))))
40	39	ralbidv2 3195	. . . 4 ⊢ (((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
41	40	rexbidva 3296	. . 3 ⊢ ((((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) ∧ 𝑥 ∈ ℝ) → (∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
42	41	rexbidva 3296	. 2 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
43	21, 42	bitrd 281	1 ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139  Vcvv 3495   ∩ cin 3935   ⊆ wss 3936   class class class wbr 5059  dom cdm 5550  ⟶wf 6346  ‘cfv 6350  (class class class)co 7150   ↑_pm cpm 8401  ℝcr 10530   · cmul 10536  +∞cpnf 10666   ≤ cle 10670  [,)cico 12734  Οcbigo 44600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605  ax-pre-lttrn 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-po 5469  df-so 5470  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8283  df-pm 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-ico 12738  df-bigo 44601

This theorem is referenced by:  elbigo2r  44606  elbigoimp  44609  elbigolo1  44610