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 G : A A F : B B A F O G x m y B x y F y m G y

Proof

Step Hyp Ref Expression
1 elbigo F O G F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y
2 df-3an F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y
3 1 2 bitri F O G F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y
4 reex V
5 4 4 pm3.2i V V
6 5 a1i G : A A F : B B A V V
7 simpl F : B B A F : B
8 7 adantl G : A A F : B B A F : B
9 sstr2 B A A B
10 9 adantld B A G : A A B
11 10 adantl F : B B A G : A A B
12 11 impcom G : A A F : B B A B
13 elpm2r V V F : B B F 𝑝𝑚
14 6 8 12 13 syl12anc G : A A F : B B A F 𝑝𝑚
15 simpl G : A A F : B B A G : A A
16 elpm2r V V G : A A G 𝑝𝑚
17 6 15 16 syl2anc G : A A F : B B A G 𝑝𝑚
18 ibar F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y
19 18 bicomd F 𝑝𝑚 G 𝑝𝑚 F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y x m y dom F x +∞ F y m G y
20 14 17 19 syl2anc G : A A F : B B A F 𝑝𝑚 G 𝑝𝑚 x m y dom F x +∞ F y m G y x m y dom F x +∞ F y m G y
21 3 20 syl5bb G : A A F : B B A F O G x m y dom F x +∞ F y m G y
22 elin y dom F x +∞ y dom F y x +∞
23 fdm F : B dom F = B
24 23 ad2antrl G : A A F : B B A dom F = B
25 24 ad2antrr G : A A F : B B A x m dom F = B
26 25 eleq2d G : A A F : B B A x m y dom F y B
27 26 anbi1d G : A A F : B B A x m y dom F y x +∞ y B y x +∞
28 elicopnf x y x +∞ y x y
29 28 ad3antlr G : A A F : B B A x m y B y x +∞ y x y
30 12 ad2antrr G : A A F : B B A x m B
31 30 sselda G : A A F : B B A x m y B y
32 31 biantrurd G : A A F : B B A x m y B x y y x y
33 29 32 bitr4d G : A A F : B B A x m y B y x +∞ x y
34 33 pm5.32da G : A A F : B B A x m y B y x +∞ y B x y
35 27 34 bitrd G : A A F : B B A x m y dom F y x +∞ y B x y
36 22 35 syl5bb G : A A F : B B A x m y dom F x +∞ y B x y
37 36 imbi1d G : A A F : B B A x m y dom F x +∞ F y m G y y B x y F y m G y
38 impexp y B x y F y m G y y B x y F y m G y
39 37 38 bitrdi G : A A F : B B A x m y dom F x +∞ F y m G y y B x y F y m G y
40 39 ralbidv2 G : A A F : B B A x m y dom F x +∞ F y m G y y B x y F y m G y
41 40 rexbidva G : A A F : B B A x m y dom F x +∞ F y m G y m y B x y F y m G y
42 41 rexbidva G : A A F : B B A x m y dom F x +∞ F y m G y x m y B x y F y m G y
43 21 42 bitrd G : A A F : B B A F O G x m y B x y F y m G y