This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminfgord

Description: Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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