infxrlesupxr

Description: The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infxrlesupxr.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
	infxrlesupxr.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	infxrlesupxr	⊢ ( 𝜑 → inf ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐴 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		infxrlesupxr.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
2		infxrlesupxr.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
4	3	biimpi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 )
5	2 4	syl	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
6	1	infxrcld	⊢ ( 𝜑 → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
8	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
9	1	supxrcld	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ^* )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
13		infxrlb	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝑥 )
14	11 12 13	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝑥 )
15		eqid	⊢ sup ( 𝐴 , ℝ^* , < ) = sup ( 𝐴 , ℝ^* , < )
16	11 12 15	supxrubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℝ^* , < ) )
17	7 8 10 14 16	xrletrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐴 , ℝ^* , < ) )
18	17	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → inf ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐴 , ℝ^* , < ) ) )
19	18	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → inf ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐴 , ℝ^* , < ) ) )
20	5 19	mpd	⊢ ( 𝜑 → inf ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐴 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem infxrlesupxr

Proof