Metamath Proof Explorer

Theorem sup3

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

Ref Expression
Assertion sup3 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→∃x∈ℝ∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z

Proof

Step Hyp Ref Expression
1 ssel ⊢A⊆ℝ→y∈A→y∈ℝ
2 leloe ⊢y∈ℝ∧x∈ℝ→y≤x↔y<x∨y=x
3 2 expcom ⊢x∈ℝ→y∈ℝ→y≤x↔y<x∨y=x
4 1 3 syl9 ⊢A⊆ℝ→x∈ℝ→y∈A→y≤x↔y<x∨y=x
5 4 imp31 ⊢A⊆ℝ∧x∈ℝ∧y∈A→y≤x↔y<x∨y=x
6 5 ralbidva ⊢A⊆ℝ∧x∈ℝ→∀y∈Ay≤x↔∀y∈Ay<x∨y=x
7 6 rexbidva ⊢A⊆ℝ→∃x∈ℝ∀y∈Ay≤x↔∃x∈ℝ∀y∈Ay<x∨y=x
8 7 anbi2d ⊢A⊆ℝ→A≠∅∧∃x∈ℝ∀y∈Ay≤x↔A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x
9 8 pm5.32i ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x↔A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x
10 3anass ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x↔A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x
11 3anass ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x↔A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x
12 9 10 11 3bitr4i ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x↔A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x
13 sup2 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<x∨y=x→∃x∈ℝ∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z
14 12 13 sylbi ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→∃x∈ℝ∀y∈A¬x<y∧∀y∈ℝy<x→∃z∈Ay<z