Metamath Proof Explorer


Theorem lo1res

Description: The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion lo1res F 𝑂1 F A 𝑂1

Proof

Step Hyp Ref Expression
1 lo1f F 𝑂1 F : dom F
2 lo1bdd F 𝑂1 F : dom F x m y dom F x y F y m
3 1 2 mpdan F 𝑂1 x m y dom F x y F y m
4 inss1 dom F A dom F
5 ssralv dom F A dom F y dom F x y F y m y dom F A x y F y m
6 4 5 ax-mp y dom F x y F y m y dom F A x y F y m
7 elinel2 y dom F A y A
8 7 fvresd y dom F A F A y = F y
9 8 breq1d y dom F A F A y m F y m
10 9 imbi2d y dom F A x y F A y m x y F y m
11 10 ralbiia y dom F A x y F A y m y dom F A x y F y m
12 6 11 sylibr y dom F x y F y m y dom F A x y F A y m
13 12 reximi m y dom F x y F y m m y dom F A x y F A y m
14 13 reximi x m y dom F x y F y m x m y dom F A x y F A y m
15 3 14 syl F 𝑂1 x m y dom F A x y F A y m
16 fssres F : dom F dom F A dom F F dom F A : dom F A
17 1 4 16 sylancl F 𝑂1 F dom F A : dom F A
18 resres F dom F A = F dom F A
19 ffn F : dom F F Fn dom F
20 fnresdm F Fn dom F F dom F = F
21 1 19 20 3syl F 𝑂1 F dom F = F
22 21 reseq1d F 𝑂1 F dom F A = F A
23 18 22 eqtr3id F 𝑂1 F dom F A = F A
24 23 feq1d F 𝑂1 F dom F A : dom F A F A : dom F A
25 17 24 mpbid F 𝑂1 F A : dom F A
26 lo1dm F 𝑂1 dom F
27 4 26 sstrid F 𝑂1 dom F A
28 ello12 F A : dom F A dom F A F A 𝑂1 x m y dom F A x y F A y m
29 25 27 28 syl2anc F 𝑂1 F A 𝑂1 x m y dom F A x y F A y m
30 15 29 mpbird F 𝑂1 F A 𝑂1