Metamath Proof Explorer


Theorem sup3

Description: A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004)

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

Proof

Step Hyp Ref Expression
1 ssel ( 𝐴 ⊆ ℝ → ( 𝑦𝐴𝑦 ∈ ℝ ) )
2 leloe ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦𝑥 ↔ ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) )
3 2 expcom ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ℝ → ( 𝑦𝑥 ↔ ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ) )
4 1 3 syl9 ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦𝐴 → ( 𝑦𝑥 ↔ ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ) ) )
5 4 imp31 ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦𝑥 ↔ ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) )
6 5 ralbidva ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝐴 𝑦𝑥 ↔ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) )
7 6 rexbidva ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) )
8 7 anbi2d ( 𝐴 ⊆ ℝ → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ↔ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ) )
9 8 pm5.32i ( ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ) )
10 3anass ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ) )
11 3anass ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) ) )
12 9 10 11 3bitr4i ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ↔ ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) )
13 sup2 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 ( 𝑦 < 𝑥𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
14 12 13 sylbi ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )