Theorem supxrbnd

Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006)

	Ref	Expression
Assertion	supxrbnd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ressxr	⊢ ℝ ⊆ ℝ*
2		sstr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
3	1 2	mpan2	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ* )
4		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6		xrltne	⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → +∞ ≠ sup ( 𝐴 , ℝ* , < ) )
7	5 6	mp3an2	⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → +∞ ≠ sup ( 𝐴 , ℝ* , < ) )
8	7	necomd	⊢ ( ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ≠ +∞ )
9	8	ex	⊢ ( sup ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
10	4 9	syl	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
11		supxrunb2	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
12		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
13	12	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
14		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
15	14	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
16		xrlenlt	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑦 ) )
17	16	con2bid	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
18	13 15 17	syl2anc	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
19	18	rexbidva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥 ) )
20		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
21	19 20	bitrdi	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
22	21	ralbidva	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
23	11 22	bitr3d	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
24		ralnex	⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
25	23 24	bitrdi	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
26	25	necon2abid	⊢ ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) ≠ +∞ ) )
27	10 26	sylibrd	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) < +∞ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
28	27	imp	⊢ ( ( 𝐴 ⊆ ℝ* ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
29	3 28	sylan	⊢ ( ( 𝐴 ⊆ ℝ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
30	29	3adant2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
31		supxrre	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ* , < ) = sup ( 𝐴 , ℝ , < ) )
32		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
33	31 32	eqeltrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )
34	30 33	syld3an3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup ( 𝐴 , ℝ* , < ) < +∞ ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ )