ressiooinf

Description: If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	ressiooinf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ressiooinf.s	⊢ 𝑆 = inf ( 𝐴 , ℝ^* , < )
	ressiooinf.n	⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
	ressiooinf.i	⊢ 𝐼 = ( 𝑆 (,) +∞ )
Assertion	ressiooinf	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ressiooinf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ressiooinf.s	⊢ 𝑆 = inf ( 𝐴 , ℝ^* , < )
3		ressiooinf.n	⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝐴 )
4		ressiooinf.i	⊢ 𝐼 = ( 𝑆 (,) +∞ )
5		ressxr	⊢ ℝ ⊆ ℝ^*
6	5	a1i	⊢ ( 𝜑 → ℝ ⊆ ℝ^* )
7	1 6	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ^* )
9	8	infxrcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
10	2 9	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ∈ ℝ^* )
11		pnfxr	⊢ +∞ ∈ ℝ^*
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → +∞ ∈ ℝ^* )
13	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
15	13 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
16	7	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
17		infxrlb	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝑥 )
18	8 14 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ^* , < ) ≤ 𝑥 )
19	2 18	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ≤ 𝑥 )
20		id	⊢ ( 𝑥 = 𝑆 → 𝑥 = 𝑆 )
21	20	eqcomd	⊢ ( 𝑥 = 𝑆 → 𝑆 = 𝑥 )
22	21	adantl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 = 𝑥 )
23		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑥 ∈ 𝐴 )
24	22 23	eqeltrd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
25	24	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → 𝑆 ∈ 𝐴 )
26	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = 𝑆 ) → ¬ 𝑆 ∈ 𝐴 )
27	25 26	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝑆 )
28	27	neqned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ 𝑆 )
29	28	necomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 ≠ 𝑥 )
30	10 16 19 29	xrleneltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑆 < 𝑥 )
31	15	ltpnfd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 < +∞ )
32	10 12 15 30 31	eliood	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑆 (,) +∞ ) )
33	32 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐼 )
34	33	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
35		dfss3	⊢ ( 𝐴 ⊆ 𝐼 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐼 )
36	34 35	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ 𝐼 )

Metamath Proof Explorer

Theorem ressiooinf

Proof