Metamath Proof Explorer


Theorem limsupgord

Description: Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

Ref Expression
Assertion limsupgord ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → sup ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 rexr ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 1 3ad2ant1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → 𝐴 ∈ ℝ* )
3 simp3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → 𝐴𝐵 )
4 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
5 xrletr ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ* ) → ( ( 𝐴𝐵𝐵𝑤 ) → 𝐴𝑤 ) )
6 4 4 5 ixxss1 ( ( 𝐴 ∈ ℝ*𝐴𝐵 ) → ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) )
7 2 3 6 syl2anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) )
8 imass2 ( ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) → ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝐴 [,) +∞ ) ) )
9 ssrin ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝐴 [,) +∞ ) ) → ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) )
10 7 8 9 3syl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) )
11 inss2 ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
12 supxrcl ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
13 11 12 ax-mp sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ*
14 xrleid ( sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* → sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
15 13 14 ax-mp sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < )
16 supxrleub ( ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* ∧ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* ) → ( sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
17 11 13 16 mp2an ( sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
18 15 17 mpbi 𝑥 ∈ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < )
19 ssralv ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) → ( ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) → ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
20 10 18 19 mpisyl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
21 inss2 ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
22 supxrleub ( ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* ∧ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* ) → ( sup ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
23 21 13 22 mp2an ( sup ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
24 20 23 sylibr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → sup ( ( ( 𝐹 “ ( 𝐵 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )