Metamath Proof Explorer

Theorem supxrunb3

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 peano2re ⊢ ( 𝑤 ∈ ℝ → ( 𝑤 + 1 ) ∈ ℝ )
2 1 adantl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ( 𝑤 + 1 ) ∈ ℝ )
3 simpl ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
4 breq1 ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑤 + 1 ) ≤ 𝑦 ) )
5 4 rexbidv ⊢ ( 𝑥 = ( 𝑤 + 1 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 ) )
6 5 rspcva ⊢ ( ( ( 𝑤 + 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 )
7 2 3 6 syl2anc ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 )
8 7 adantll ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 )
9 nfv ⊢ Ⅎ 𝑦 𝐴 ⊆ ℝ*
10 nfcv ⊢ Ⅎ 𝑦 ℝ
11 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦
12 10 11 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦
13 9 12 nfan ⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
14 nfv ⊢ Ⅎ 𝑦 𝑤 ∈ ℝ
15 13 14 nfan ⊢ Ⅎ 𝑦 ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ )
16 simp1r ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 ∈ ℝ )
17 rexr ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℝ* )
18 16 17 syl ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 ∈ ℝ* )
19 1 rexrd ⊢ ( 𝑤 ∈ ℝ → ( 𝑤 + 1 ) ∈ ℝ* )
20 16 19 syl ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → ( 𝑤 + 1 ) ∈ ℝ* )
21 simp1l ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝐴 ⊆ ℝ* )
22 simp2 ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
23 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
24 21 22 23 syl2anc ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ* )
25 16 ltp1d ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 < ( 𝑤 + 1 ) )
26 simp3 ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → ( 𝑤 + 1 ) ≤ 𝑦 )
27 18 20 24 25 26 xrltletrd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ∧ ( 𝑤 + 1 ) ≤ 𝑦 ) → 𝑤 < 𝑦 )
28 27 3exp ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑤 ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑤 + 1 ) ≤ 𝑦 → 𝑤 < 𝑦 ) ) )
29 28 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑤 + 1 ) ≤ 𝑦 → 𝑤 < 𝑦 ) ) )
30 15 29 reximdai ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑤 + 1 ) ≤ 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) )
31 8 30 mpd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 )
32 31 ralrimiva ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 )
33 32 ex ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) )
34 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 < 𝑦 ↔ 𝑥 < 𝑦 ) )
35 34 rexbidv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) )
36 35 cbvralvw ⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
37 36 biimpi ⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
38 nfv ⊢ Ⅎ 𝑥 𝐴 ⊆ ℝ*
39 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦
40 38 39 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
41 simpll ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ⊆ ℝ* )
42 simpr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
43 rspa ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
44 43 adantll ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 )
45 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
46 45 ad3antlr ⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ* )
47 23 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ* )
48 47 adantllr ⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ* )
49 simpr ⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
50 46 48 49 xrltled ⊢ ( ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 < 𝑦 ) → 𝑥 ≤ 𝑦 )
51 50 ex ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 < 𝑦 → 𝑥 ≤ 𝑦 ) )
52 51 reximdva ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
53 52 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
54 44 53 mpd ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
55 simpr ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
56 41 42 54 55 syl21anc ⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
57 56 ex ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
58 40 57 ralrimi ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 < 𝑦 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
59 37 58 sylan2 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
60 59 ex ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
61 33 60 impbid ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ) )
62 supxrunb2 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑤 < 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
63 61 62 bitrd ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )