Metamath Proof Explorer

Theorem sup2

Description: A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997)

Ref Expression
Assertion sup2 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
2 1 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( 𝑥 + 1 ) ∈ ℝ )
3 2 a1i ⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( 𝑥 + 1 ) ∈ ℝ ) )
4 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
5 ltp1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( 𝑥 + 1 ) )
6 1 ancli ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) )
7 lttr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) → ( ( 𝑦 < 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) → 𝑦 < ( 𝑥 + 1 ) ) )
8 7 3expb ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) ) → ( ( 𝑦 < 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) → 𝑦 < ( 𝑥 + 1 ) ) )
9 6 8 sylan2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 < 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) → 𝑦 < ( 𝑥 + 1 ) ) )
10 5 9 sylan2i ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 < 𝑥 ∧ 𝑥 ∈ ℝ ) → 𝑦 < ( 𝑥 + 1 ) ) )
11 10 exp4b ⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 < 𝑥 → ( 𝑥 ∈ ℝ → 𝑦 < ( 𝑥 + 1 ) ) ) ) )
12 11 com34 ⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 < 𝑥 → 𝑦 < ( 𝑥 + 1 ) ) ) ) )
13 12 pm2.43d ⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 < 𝑥 → 𝑦 < ( 𝑥 + 1 ) ) ) )
14 13 imp ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 → 𝑦 < ( 𝑥 + 1 ) ) )
15 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 < ( 𝑥 + 1 ) ↔ 𝑥 < ( 𝑥 + 1 ) ) )
16 5 15 syl5ibrcom ⊢ ( 𝑥 ∈ ℝ → ( 𝑦 = 𝑥 → 𝑦 < ( 𝑥 + 1 ) ) )
17 16 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 = 𝑥 → 𝑦 < ( 𝑥 + 1 ) ) )
18 14 17 jaod ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑦 < ( 𝑥 + 1 ) ) )
19 18 ex ⊢ ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑦 < ( 𝑥 + 1 ) ) ) )
20 4 19 syl6 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ ℝ → ( ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑦 < ( 𝑥 + 1 ) ) ) ) )
21 20 com23 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 ∈ 𝐴 → ( ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑦 < ( 𝑥 + 1 ) ) ) ) )
22 21 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → 𝑦 < ( 𝑥 + 1 ) ) ) )
23 22 a2d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( 𝑦 ∈ 𝐴 → 𝑦 < ( 𝑥 + 1 ) ) ) )
24 23 ralimdv2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) )
25 24 expimpd ⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) )
26 3 25 jcad ⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) ) )
27 ovex ⊢ ( 𝑥 + 1 ) ∈ V
28 eleq1 ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( 𝑧 ∈ ℝ ↔ ( 𝑥 + 1 ) ∈ ℝ ) )
29 breq2 ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( 𝑦 < 𝑧 ↔ 𝑦 < ( 𝑥 + 1 ) ) )
30 29 ralbidv ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) )
31 28 30 anbi12d ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) ) )
32 27 31 spcev ⊢ ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < ( 𝑥 + 1 ) ) → ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) )
33 26 32 syl6 ⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) ) )
34 33 exlimdv ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) ) )
35 eleq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ℝ ↔ 𝑥 ∈ ℝ ) )
36 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 < 𝑧 ↔ 𝑦 < 𝑥 ) )
37 36 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
38 35 37 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) ) )
39 38 cbvexvw ⊢ ( ∃ 𝑧 ( 𝑧 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
40 34 39 syl6ib ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) ) )
41 df-rex ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
42 df-rex ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
43 40 41 42 3imtr4g ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
44 43 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
45 44 imdistani ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
46 df-3an ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ↔ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
47 df-3an ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) ↔ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
48 45 46 47 3imtr4i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
49 axsup ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
50 48 49 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )