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