This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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