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