This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-suprubd

Description: suprubd without ax-mulcom , proven trivially from sn-suprcld . (Contributed by SN, 29-Jun-2025)

Ref Expression
Hypotheses sn-sup3d.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
sn-sup3d.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
sn-sup3d.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
sn-suprubd.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
Assertion sn-suprubd ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 sn-sup3d.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 sn-sup3d.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 sn-sup3d.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4 sn-suprubd.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
5 1 4 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6 1 2 3 sn-suprcld ⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
7 ltso ⊢ < Or ℝ
8 7 a1i ⊢ ( 𝜑 → < Or ℝ )
9 1 2 3 sn-sup3d ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
10 8 9 supub ⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 → ¬ sup ( 𝐴 , ℝ , < ) < 𝐵 ) )
11 4 10 mpd ⊢ ( 𝜑 → ¬ sup ( 𝐴 , ℝ , < ) < 𝐵 )
12 5 6 11 nltled ⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )