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 ( 𝐴 , ℝ , < ) )