Theorem sn-suprcld

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

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

Proof

Step	Hyp	Ref	Expression
1		sn-sup3d.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		sn-sup3d.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		sn-sup3d.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		ltso	⊢ < Or ℝ
5	4	a1i	⊢ ( 𝜑 → < Or ℝ )
6	1 2 3	sn-sup3d	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
7	5 6	supcl	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )