Theorem supxrunb2

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

	Ref	Expression
Assertion	supxrunb2	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ ℝ* → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℝ* ) )
2		pnfnlt	⊢ ( 𝑧 ∈ ℝ* → ¬ +∞ < 𝑧 )
3	1 2	syl6	⊢ ( 𝐴 ⊆ ℝ* → ( 𝑧 ∈ 𝐴 → ¬ +∞ < 𝑧 ) )
4	3	ralrimiv	⊢ ( 𝐴 ⊆ ℝ* → ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 )
5	4	adantr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 )
6		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 < 𝑦 ↔ 𝑧 < 𝑦 ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
8	7	rspcva	⊢ ( ( 𝑧 ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 )
9	8	adantrr	⊢ ( ( 𝑧 ∈ ℝ ∧ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ∧ 𝐴 ⊆ ℝ* ) ) → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 )
10	9	ancoms	⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ∧ 𝐴 ⊆ ℝ* ) ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 )
11	10	exp31	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ( 𝐴 ⊆ ℝ* → ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
12	11	a1dd	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ( 𝐴 ⊆ ℝ* → ( 𝑧 < +∞ → ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
13	12	com4r	⊢ ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ( 𝐴 ⊆ ℝ* → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
14	13	com13	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ( 𝑧 ∈ ℝ → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
15	14	imp	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ( 𝑧 ∈ ℝ → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
16	15	ralrimiv	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
17	5 16	jca	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
18		pnfxr	⊢ +∞ ∈ ℝ*
19		supxr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
20	18 19	mpanl2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
21	17 20	syldan	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
22	21	ex	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → sup ( 𝐴 , ℝ* , < ) = +∞ ) )
23		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
24	23	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝑥 ∈ ℝ* )
25		ltpnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
26		breq2	⊢ ( sup ( 𝐴 , ℝ* , < ) = +∞ → ( 𝑥 < sup ( 𝐴 , ℝ* , < ) ↔ 𝑥 < +∞ ) )
27	25 26	imbitrrid	⊢ ( sup ( 𝐴 , ℝ* , < ) = +∞ → ( 𝑥 ∈ ℝ → 𝑥 < sup ( 𝐴 , ℝ* , < ) ) )
28	27	impcom	⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝑥 < sup ( 𝐴 , ℝ* , < ) )
29	28	adantll	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → 𝑥 < sup ( 𝐴 , ℝ* , < ) )
30		xrltso	⊢ < Or ℝ*
31	30	a1i	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → < Or ℝ* )
32		xrsupss	⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑤 < 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) )
33	32	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑤 < 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) )
34	31 33	suplub	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( 𝐴 , ℝ* , < ) ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
35	24 29 34	mp2and	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ* , < ) = +∞ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
36	35	exp31	⊢ ( 𝐴 ⊆ ℝ* → ( 𝑥 ∈ ℝ → ( sup ( 𝐴 , ℝ* , < ) = +∞ → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
37	36	com23	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ → ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ) )
38	37	ralrimdv	⊢ ( 𝐴 ⊆ ℝ* → ( sup ( 𝐴 , ℝ* , < ) = +∞ → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
39	22 38	impbid	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )