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	syl5ibr	⊢ ( 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 ( 𝐴 , ℝ^* , < ) = +∞ ) )

Metamath Proof Explorer

Theorem supxrunb2

Proof