Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℝ+ → 𝐹:𝐴⟶ℝ+) |
2 | | rpssre 11719 |
. . . . . . . . . . . . 13
⊢
ℝ+ ⊆ ℝ |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℝ+ →
ℝ+ ⊆ ℝ) |
4 | 1, 3 | fssd 5970 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℝ+ → 𝐹:𝐴⟶ℝ) |
5 | 4 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐹:𝐴⟶ℝ) |
6 | 5 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐹:𝐴⟶ℝ) |
7 | 6 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ℝ) |
8 | | simplrr 797 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → 𝑚 ∈ ℝ) |
9 | | simpl2 1058 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐺:𝐴⟶ℝ+) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐺‘𝑦) ∈
ℝ+) |
11 | 10 | rpregt0d 11754 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) |
12 | 7, 8, 11 | 3jca 1235 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦)))) |
13 | | ledivmul2 10781 |
. . . . . . . 8
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) → (((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) |
14 | 13 | bicomd 212 |
. . . . . . 7
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ((𝐺‘𝑦) ∈ ℝ ∧ 0 < (𝐺‘𝑦))) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
15 | 12, 14 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶ℝ+ → 𝐺:𝐴⟶ℝ+) |
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶ℝ+ →
ℝ+ ⊆ ℝ) |
18 | 16, 17 | fssd 5970 |
. . . . . . . . . . . 12
⊢ (𝐺:𝐴⟶ℝ+ → 𝐺:𝐴⟶ℝ) |
19 | 18 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐺:𝐴⟶ℝ) |
20 | | reex 9906 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
21 | 20 | ssex 4730 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ → 𝐴 ∈ V) |
22 | 21 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ∈ V) |
23 | 5, 19, 22 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V)) |
26 | | ffun 5961 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶ℝ+ → Fun 𝐺) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → Fun
𝐺) |
28 | 21 | anim1i 590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐴 ∈ V ∧ 𝐺:𝐴⟶ℝ+)) |
29 | 28 | ancomd 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺:𝐴⟶ℝ+ ∧ 𝐴 ∈ V)) |
30 | | fex 6394 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:𝐴⟶ℝ+ ∧ 𝐴 ∈ V) → 𝐺 ∈ V) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐺 ∈ V) |
32 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0 ∈
ℝ) |
33 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:𝐴⟶ℝ+ → ran 𝐺 ⊆
ℝ+) |
34 | | 0nrp 11741 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 0
∈ ℝ+ |
35 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ran
𝐺 ⊆
ℝ+ → ran 𝐺 ⊆
ℝ+) |
36 | 35 | ssneld 3570 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
𝐺 ⊆
ℝ+ → (¬ 0 ∈ ℝ+ → ¬ 0
∈ ran 𝐺)) |
37 | 34, 36 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran
𝐺 ⊆
ℝ+ → ¬ 0 ∈ ran 𝐺) |
38 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ (0
∉ ran 𝐺 ↔ ¬
0 ∈ ran 𝐺) |
39 | 37, 38 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
𝐺 ⊆
ℝ+ → 0 ∉ ran 𝐺) |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐴⟶ℝ+ → 0 ∉
ran 𝐺) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 0
∉ ran 𝐺) |
42 | | suppdm 42094 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
𝐺 ∧ 𝐺 ∈ V ∧ 0 ∈ ℝ) ∧ 0
∉ ran 𝐺) →
(𝐺 supp 0) = dom 𝐺) |
43 | 27, 31, 32, 41, 42 | syl31anc 1321 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = dom 𝐺) |
44 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝐴⟶ℝ+ → dom 𝐺 = 𝐴) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → dom
𝐺 = 𝐴) |
46 | 43, 45 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴) |
47 | 46 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐺 supp 0) = 𝐴) |
48 | 47 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 = (𝐺 supp 0)) |
49 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝐴 = (𝐺 supp 0)) |
50 | 49 | eleq2d 2673 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ (𝐺 supp 0))) |
51 | 50 | biimpa 500 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ (𝐺 supp 0)) |
52 | | refdivmptfv 42138 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
53 | 25, 51, 52 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹 /f 𝐺)‘𝑦) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
54 | 53 | breq1d 4593 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → (((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚 ↔ ((𝐹‘𝑦) / (𝐺‘𝑦)) ≤ 𝑚)) |
55 | 15, 54 | bitr4d 270 |
. . . . 5
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)) ↔ ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚)) |
56 | 55 | imbi2d 329 |
. . . 4
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑦 ∈ 𝐴) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
57 | 56 | ralbidva 2968 |
. . 3
⊢ (((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) ∧ (𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ)) →
(∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
58 | 57 | 2rexbidva 3038 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) →
(∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
59 | | simp1 1054 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ⊆
ℝ) |
60 | | ssid 3587 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
61 | 60 | a1i 11 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 ⊆ 𝐴) |
62 | | elbigo2 42144 |
. . 3
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) |
63 | 19, 59, 5, 61, 62 | syl22anc 1319 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) |
64 | | refdivmptf 42134 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ V) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) |
65 | 23, 64 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) |
66 | 44 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐺:𝐴⟶ℝ+ → 𝐴 = dom 𝐺) |
67 | 66 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 = dom 𝐺) |
68 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐺:𝐴⟶ℝ+) |
69 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐴 ∈ V) |
70 | 68, 69, 30 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → 𝐺 ∈ V) |
71 | 27, 70, 32, 41, 42 | syl31anc 1321 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+) → (𝐺 supp 0) = dom 𝐺) |
72 | 71 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐺 supp 0) = dom 𝐺) |
73 | 67, 72 | eqtr4d 2647 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → 𝐴 = (𝐺 supp 0)) |
74 | 73 | feq2d 5944 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺):𝐴⟶ℝ ↔ (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)) |
75 | 65, 74 | mpbird 246 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 /f 𝐺):𝐴⟶ℝ) |
76 | | ello12 14095 |
. . 3
⊢ (((𝐹 /f 𝐺):𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
77 | 75, 59, 76 | syl2anc 691 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → ((𝐹 /f 𝐺) ∈ ≤𝑂(1) ↔
∃𝑥 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → ((𝐹 /f 𝐺)‘𝑦) ≤ 𝑚))) |
78 | 58, 63, 77 | 3bitr4d 299 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1))) |