Metamath Proof Explorer

Theorem lo1le

Description: Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1le.1 
|- ( ph -> M e. RR )
lo1le.2 
|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
lo1le.3 
|- ( ( ph /\ x e. A ) -> B e. V )
lo1le.4 
|- ( ( ph /\ x e. A ) -> C e. RR )
lo1le.5 
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )
Assertion lo1le 
|- ( ph -> ( x e. A |-> C ) e. <_O(1) )

Proof

Step Hyp Ref Expression
1 lo1le.1 
 |-  ( ph -> M e. RR )
2 lo1le.2 
 |-  ( ph -> ( x e. A |-> B ) e. <_O(1) )
3 lo1le.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 lo1le.4 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
5 lo1le.5 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )
6 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
7 1 adantr 
 |-  ( ( ph /\ y e. RR ) -> M e. RR )
8 6 7 ifcld 
 |-  ( ( ph /\ y e. RR ) -> if ( M <_ y , y , M ) e. RR )
9 1 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> M e. RR )
10 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> y e. RR )
11 3 ralrimiva 
 |-  ( ph -> A. x e. A B e. V )
12 dmmptg 
 |-  ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
13 11 12 syl 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
14 lo1dm 
 |-  ( ( x e. A |-> B ) e. <_O(1) -> dom ( x e. A |-> B ) C_ RR )
15 2 14 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
16 13 15 eqsstrrd 
 |-  ( ph -> A C_ RR )
17 16 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> A C_ RR )
18 simprr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> x e. A )
19 17 18 sseldd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> x e. RR )
20 maxle 
 |-  ( ( M e. RR /\ y e. RR /\ x e. RR ) -> ( if ( M <_ y , y , M ) <_ x <-> ( M <_ x /\ y <_ x ) ) )
21 9 10 19 20 syl3anc 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( if ( M <_ y , y , M ) <_ x <-> ( M <_ x /\ y <_ x ) ) )
22 simpr 
 |-  ( ( M <_ x /\ y <_ x ) -> y <_ x )
23 21 22 biimtrdi 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( if ( M <_ y , y , M ) <_ x -> y <_ x ) )
24 23 imim1d 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( ( y <_ x -> B <_ m ) -> ( if ( M <_ y , y , M ) <_ x -> B <_ m ) ) )
25 5 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. A /\ M <_ x ) ) -> C <_ B )
26 25 adantrll 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> C <_ B )
27 simpl 
 |-  ( ( ph /\ y e. RR ) -> ph )
28 simplr 
 |-  ( ( ( m e. RR /\ x e. A ) /\ M <_ x ) -> x e. A )
29 27 28 4 syl2an 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> C e. RR )
30 3 2 lo1mptrcl 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
31 27 28 30 syl2an 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> B e. RR )
32 simprll 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> m e. RR )
33 letr 
 |-  ( ( C e. RR /\ B e. RR /\ m e. RR ) -> ( ( C <_ B /\ B <_ m ) -> C <_ m ) )
34 29 31 32 33 syl3anc 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> ( ( C <_ B /\ B <_ m ) -> C <_ m ) )
35 26 34 mpand 
 |-  ( ( ( ph /\ y e. RR ) /\ ( ( m e. RR /\ x e. A ) /\ M <_ x ) ) -> ( B <_ m -> C <_ m ) )
36 35 expr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( M <_ x -> ( B <_ m -> C <_ m ) ) )
37 36 adantrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( ( M <_ x /\ y <_ x ) -> ( B <_ m -> C <_ m ) ) )
38 21 37 sylbid 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( if ( M <_ y , y , M ) <_ x -> ( B <_ m -> C <_ m ) ) )
39 38 a2d 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( ( if ( M <_ y , y , M ) <_ x -> B <_ m ) -> ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
40 24 39 syld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( m e. RR /\ x e. A ) ) -> ( ( y <_ x -> B <_ m ) -> ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
41 40 anassrs 
 |-  ( ( ( ( ph /\ y e. RR ) /\ m e. RR ) /\ x e. A ) -> ( ( y <_ x -> B <_ m ) -> ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
42 41 ralimdva 
 |-  ( ( ( ph /\ y e. RR ) /\ m e. RR ) -> ( A. x e. A ( y <_ x -> B <_ m ) -> A. x e. A ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
43 42 reximdva 
 |-  ( ( ph /\ y e. RR ) -> ( E. m e. RR A. x e. A ( y <_ x -> B <_ m ) -> E. m e. RR A. x e. A ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
44 breq1 
 |-  ( z = if ( M <_ y , y , M ) -> ( z <_ x <-> if ( M <_ y , y , M ) <_ x ) )
45 44 imbi1d 
 |-  ( z = if ( M <_ y , y , M ) -> ( ( z <_ x -> C <_ m ) <-> ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
46 45 rexralbidv 
 |-  ( z = if ( M <_ y , y , M ) -> ( E. m e. RR A. x e. A ( z <_ x -> C <_ m ) <-> E. m e. RR A. x e. A ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) )
47 46 rspcev 
 |-  ( ( if ( M <_ y , y , M ) e. RR /\ E. m e. RR A. x e. A ( if ( M <_ y , y , M ) <_ x -> C <_ m ) ) -> E. z e. RR E. m e. RR A. x e. A ( z <_ x -> C <_ m ) )
48 8 43 47 syl6an 
 |-  ( ( ph /\ y e. RR ) -> ( E. m e. RR A. x e. A ( y <_ x -> B <_ m ) -> E. z e. RR E. m e. RR A. x e. A ( z <_ x -> C <_ m ) ) )
49 48 rexlimdva 
 |-  ( ph -> ( E. y e. RR E. m e. RR A. x e. A ( y <_ x -> B <_ m ) -> E. z e. RR E. m e. RR A. x e. A ( z <_ x -> C <_ m ) ) )
50 16 30 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> B <_ m ) ) )
51 16 4 ello1mpt 
 |-  ( ph -> ( ( x e. A |-> C ) e. <_O(1) <-> E. z e. RR E. m e. RR A. x e. A ( z <_ x -> C <_ m ) ) )
52 49 50 51 3imtr4d 
 |-  ( ph -> ( ( x e. A |-> B ) e. <_O(1) -> ( x e. A |-> C ) e. <_O(1) ) )
53 2 52 mpd 
 |-  ( ph -> ( x e. A |-> C ) e. <_O(1) )