supxrunb1

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

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

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℝ^* ) )
2		pnfnlt	⊢ ( 𝑧 ∈ ℝ^* → ¬ +∞ < 𝑧 )
3	1 2	syl6	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝑧 ∈ 𝐴 → ¬ +∞ < 𝑧 ) )
4	3	ralrimiv	⊢ ( 𝐴 ⊆ ℝ^* → ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 )
5	4	adantr	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 )
6		peano2re	⊢ ( 𝑧 ∈ ℝ → ( 𝑧 + 1 ) ∈ ℝ )
7		breq1	⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑧 + 1 ) ≤ 𝑦 ) )
8	7	rexbidv	⊢ ( 𝑥 = ( 𝑧 + 1 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 ) )
9	8	rspcva	⊢ ( ( ( 𝑧 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 )
10	9	adantrr	⊢ ( ( ( 𝑧 + 1 ) ∈ ℝ ∧ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝐴 ⊆ ℝ^* ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 )
11	10	ancoms	⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝐴 ⊆ ℝ^* ) ∧ ( 𝑧 + 1 ) ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 )
12	6 11	sylan2	⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝐴 ⊆ ℝ^* ) ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 )
13		ssel2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ^* )
14		ltp1	⊢ ( 𝑧 ∈ ℝ → 𝑧 < ( 𝑧 + 1 ) )
15	14	adantr	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ^* ) → 𝑧 < ( 𝑧 + 1 ) )
16	6	ancli	⊢ ( 𝑧 ∈ ℝ → ( 𝑧 ∈ ℝ ∧ ( 𝑧 + 1 ) ∈ ℝ ) )
17		rexr	⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ^* )
18		rexr	⊢ ( ( 𝑧 + 1 ) ∈ ℝ → ( 𝑧 + 1 ) ∈ ℝ^* )
19		xrltletr	⊢ ( ( 𝑧 ∈ ℝ^* ∧ ( 𝑧 + 1 ) ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 < ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ 𝑦 ) → 𝑧 < 𝑦 ) )
20	18 19	syl3an2	⊢ ( ( 𝑧 ∈ ℝ^* ∧ ( 𝑧 + 1 ) ∈ ℝ ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 < ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ 𝑦 ) → 𝑧 < 𝑦 ) )
21	17 20	syl3an1	⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 + 1 ) ∈ ℝ ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 < ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ 𝑦 ) → 𝑧 < 𝑦 ) )
22	21	3expa	⊢ ( ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 + 1 ) ∈ ℝ ) ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 < ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ 𝑦 ) → 𝑧 < 𝑦 ) )
23	16 22	sylan	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 < ( 𝑧 + 1 ) ∧ ( 𝑧 + 1 ) ≤ 𝑦 ) → 𝑧 < 𝑦 ) )
24	15 23	mpand	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝑧 + 1 ) ≤ 𝑦 → 𝑧 < 𝑦 ) )
25	24	ancoms	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ ) → ( ( 𝑧 + 1 ) ≤ 𝑦 → 𝑧 < 𝑦 ) )
26	13 25	sylan	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝑧 + 1 ) ≤ 𝑦 → 𝑧 < 𝑦 ) )
27	26	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑧 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 + 1 ) ≤ 𝑦 → 𝑧 < 𝑦 ) )
28	27	reximdva	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
29	28	adantll	⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝐴 ⊆ ℝ^* ) ∧ 𝑧 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 + 1 ) ≤ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
30	12 29	mpd	⊢ ( ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝐴 ⊆ ℝ^* ) ∧ 𝑧 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 )
31	30	exp31	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ( 𝐴 ⊆ ℝ^* → ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
32	31	a1dd	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ( 𝐴 ⊆ ℝ^* → ( 𝑧 < +∞ → ( 𝑧 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
33	32	com4r	⊢ ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ( 𝐴 ⊆ ℝ^* → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
34	33	com13	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ( 𝑧 ∈ ℝ → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
35	34	imp	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( 𝑧 ∈ ℝ → ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
36	35	ralrimiv	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) )
37	5 36	jca	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) )
38		pnfxr	⊢ +∞ ∈ ℝ^*
39		supxr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ +∞ ∈ ℝ^* ) ∧ ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ^* , < ) = +∞ )
40	38 39	mpanl2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ( ∀ 𝑧 ∈ 𝐴 ¬ +∞ < 𝑧 ∧ ∀ 𝑧 ∈ ℝ ( 𝑧 < +∞ → ∃ 𝑦 ∈ 𝐴 𝑧 < 𝑦 ) ) ) → sup ( 𝐴 , ℝ^* , < ) = +∞ )
41	37 40	syldan	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( 𝐴 , ℝ^* , < ) = +∞ )
42	41	ex	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → sup ( 𝐴 , ℝ^* , < ) = +∞ ) )
43		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ^* )
44	43	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝑥 ∈ ℝ^* )
45		ltpnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
46		breq2	⊢ ( sup ( 𝐴 , ℝ^* , < ) = +∞ → ( 𝑥 < sup ( 𝐴 , ℝ^* , < ) ↔ 𝑥 < +∞ ) )
47	45 46	imbitrrid	⊢ ( sup ( 𝐴 , ℝ^* , < ) = +∞ → ( 𝑥 ∈ ℝ → 𝑥 < sup ( 𝐴 , ℝ^* , < ) ) )
48	47	impcom	⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝑥 < sup ( 𝐴 , ℝ^* , < ) )
49	48	adantll	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝑥 < sup ( 𝐴 , ℝ^* , < ) )
50		xrltso	⊢ < Or ℝ^*
51	50	a1i	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → < Or ℝ^* )
52		xrsupss	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑧 ∈ ℝ^* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀ 𝑤 ∈ ℝ^* ( 𝑤 < 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) )
53	52	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ∃ 𝑧 ∈ ℝ^* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑧 < 𝑤 ∧ ∀ 𝑤 ∈ ℝ^* ( 𝑤 < 𝑧 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) ) )
54	51 53	suplub	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( ( 𝑥 ∈ ℝ^* ∧ 𝑥 < sup ( 𝐴 , ℝ^* , < ) ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
55	44 49 54	mp2and	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
56	55	ex	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) → ( sup ( 𝐴 , ℝ^* , < ) = +∞ → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
57	43	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
58	13	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ^* )
59		xrltle	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑥 < 𝑦 → 𝑥 ≤ 𝑦 ) )
60	57 58 59	syl2anc	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝑥 ≤ 𝑦 ) )
61	60	reximdva	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
62	56 61	syld	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ ℝ ) → ( sup ( 𝐴 , ℝ^* , < ) = +∞ → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
63	62	ralrimdva	⊢ ( 𝐴 ⊆ ℝ^* → ( sup ( 𝐴 , ℝ^* , < ) = +∞ → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
64	42 63	impbid	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup ( 𝐴 , ℝ^* , < ) = +∞ ) )

Metamath Proof Explorer

Theorem supxrunb1

Proof