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 ( ( ( 𝐹 “ ( 𝐴 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )