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

Metamath Proof Explorer

Theorem sn-sup3d

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

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

Proof

Step Hyp Ref Expression
1 sn-sup3d.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 sn-sup3d.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 sn-sup3d.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
5 leloe ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
6 5 expcom ⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ℝ → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) )
7 4 6 syl9 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ ℝ → ( 𝑦 ∈ 𝐴 → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) ) ) )
8 7 imp31 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
9 8 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
10 9 rexbidva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
11 1 10 syl ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) )
12 3 11 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) )
13 sn-sup2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
14 1 2 12 13 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )