Metamath Proof Explorer


Theorem lo1resb

Description: The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1resb.1 φ F : A
lo1resb.2 φ A
lo1resb.3 φ B
Assertion lo1resb φ F 𝑂1 F B +∞ 𝑂1

Proof

Step Hyp Ref Expression
1 lo1resb.1 φ F : A
2 lo1resb.2 φ A
3 lo1resb.3 φ B
4 lo1res F 𝑂1 F B +∞ 𝑂1
5 1 feqmptd φ F = x A F x
6 5 reseq1d φ F B +∞ = x A F x B +∞
7 resmpt3 x A F x B +∞ = x A B +∞ F x
8 6 7 syl6eq φ F B +∞ = x A B +∞ F x
9 8 eleq1d φ F B +∞ 𝑂1 x A B +∞ F x 𝑂1
10 inss1 A B +∞ A
11 10 2 sstrid φ A B +∞
12 elinel1 x A B +∞ x A
13 ffvelrn F : A x A F x
14 1 12 13 syl2an φ x A B +∞ F x
15 11 14 ello1mpt φ x A B +∞ F x 𝑂1 y z x A B +∞ y x F x z
16 elin x A B +∞ x A x B +∞
17 16 imbi1i x A B +∞ y x F x z x A x B +∞ y x F x z
18 impexp x A x B +∞ y x F x z x A x B +∞ y x F x z
19 17 18 bitri x A B +∞ y x F x z x A x B +∞ y x F x z
20 impexp x B +∞ y x F x z x B +∞ y x F x z
21 3 ad2antrr φ y z x A B
22 2 adantr φ y z A
23 22 sselda φ y z x A x
24 elicopnf B x B +∞ x B x
25 24 baibd B x x B +∞ B x
26 21 23 25 syl2anc φ y z x A x B +∞ B x
27 26 anbi1d φ y z x A x B +∞ y x B x y x
28 simplrl φ y z x A y
29 maxle B y x if B y y B x B x y x
30 21 28 23 29 syl3anc φ y z x A if B y y B x B x y x
31 27 30 bitr4d φ y z x A x B +∞ y x if B y y B x
32 31 imbi1d φ y z x A x B +∞ y x F x z if B y y B x F x z
33 20 32 syl5bbr φ y z x A x B +∞ y x F x z if B y y B x F x z
34 33 pm5.74da φ y z x A x B +∞ y x F x z x A if B y y B x F x z
35 19 34 syl5bb φ y z x A B +∞ y x F x z x A if B y y B x F x z
36 35 ralbidv2 φ y z x A B +∞ y x F x z x A if B y y B x F x z
37 1 adantr φ y z F : A
38 simprl φ y z y
39 3 adantr φ y z B
40 38 39 ifcld φ y z if B y y B
41 simprr φ y z z
42 ello12r F : A A if B y y B z x A if B y y B x F x z F 𝑂1
43 42 3expia F : A A if B y y B z x A if B y y B x F x z F 𝑂1
44 37 22 40 41 43 syl22anc φ y z x A if B y y B x F x z F 𝑂1
45 36 44 sylbid φ y z x A B +∞ y x F x z F 𝑂1
46 45 rexlimdvva φ y z x A B +∞ y x F x z F 𝑂1
47 15 46 sylbid φ x A B +∞ F x 𝑂1 F 𝑂1
48 9 47 sylbid φ F B +∞ 𝑂1 F 𝑂1
49 4 48 impbid2 φ F 𝑂1 F B +∞ 𝑂1