Metamath Proof Explorer

Theorem supsr

Description: A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion supsr ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ 𝐴 )
2 ltrelsr ⊢ <R ⊆ ( R × R )
3 2 brel ⊢ ( 𝑦 <R 𝑥 → ( 𝑦 ∈ R ∧ 𝑥 ∈ R ) )
4 3 simpld ⊢ ( 𝑦 <R 𝑥 → 𝑦 ∈ R )
5 4 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ R )
6 dfss3 ⊢ ( 𝐴 ⊆ R ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ R )
7 5 6 sylibr ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → 𝐴 ⊆ R )
8 7 sseld ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝑢 ∈ 𝐴 → 𝑢 ∈ R ) )
9 8 rexlimivw ⊢ ( ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ( 𝑢 ∈ 𝐴 → 𝑢 ∈ R ) )
10 9 impcom ⊢ ( ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → 𝑢 ∈ R )
11 eleq1 ⊢ ( 𝑢 = if ( 𝑢 ∈ R , 𝑢 , 1R ) → ( 𝑢 ∈ 𝐴 ↔ if ( 𝑢 ∈ R , 𝑢 , 1R ) ∈ 𝐴 ) )
12 11 anbi1d ⊢ ( 𝑢 = if ( 𝑢 ∈ R , 𝑢 , 1R ) → ( ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ↔ ( if ( 𝑢 ∈ R , 𝑢 , 1R ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) ) )
13 12 imbi1d ⊢ ( 𝑢 = if ( 𝑢 ∈ R , 𝑢 , 1R ) → ( ( ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) ↔ ( ( if ( 𝑢 ∈ R , 𝑢 , 1R ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) ) )
14 opeq1 ⊢ ( 𝑣 = 𝑤 → ⟨ 𝑣 , 1P ⟩ = ⟨ 𝑤 , 1P ⟩ )
15 14 eceq1d ⊢ ( 𝑣 = 𝑤 → [ ⟨ 𝑣 , 1P ⟩ ] ~R = [ ⟨ 𝑤 , 1P ⟩ ] ~R )
16 15 oveq2d ⊢ ( 𝑣 = 𝑤 → ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) = ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) )
17 16 eleq1d ⊢ ( 𝑣 = 𝑤 → ( ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ 𝐴 ↔ ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 ) )
18 17 cbvabv ⊢ { 𝑣 ∣ ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑣 , 1P ⟩ ] ~R ) ∈ 𝐴 } = { 𝑤 ∣ ( if ( 𝑢 ∈ R , 𝑢 , 1R ) +R [ ⟨ 𝑤 , 1P ⟩ ] ~R ) ∈ 𝐴 }
19 1sr ⊢ 1R ∈ R
20 19 elimel ⊢ if ( 𝑢 ∈ R , 𝑢 , 1R ) ∈ R
21 18 20 supsrlem ⊢ ( ( if ( 𝑢 ∈ R , 𝑢 , 1R ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
22 13 21 dedth ⊢ ( 𝑢 ∈ R → ( ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
23 10 22 mpcom ⊢ ( ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )
24 23 ex ⊢ ( 𝑢 ∈ 𝐴 → ( ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
25 24 exlimiv ⊢ ( ∃ 𝑢 𝑢 ∈ 𝐴 → ( ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
26 1 25 sylbi ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) ) )
27 26 imp ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ R ∀ 𝑦 ∈ 𝐴 𝑦 <R 𝑥 ) → ∃ 𝑥 ∈ R ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀ 𝑦 ∈ R ( 𝑦 <R 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <R 𝑧 ) ) )