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

Metamath Proof Explorer

Theorem ex-po

Description: Example for df-po . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion ex-po ( < Po ℝ ∧ ¬ ≤ Po ℝ )

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 sopo ⊢ ( < Or ℝ → < Po ℝ )
3 1 2 ax-mp ⊢ < Po ℝ
4 0le0 ⊢ 0 ≤ 0
5 0re ⊢ 0 ∈ ℝ
6 poirr ⊢ ( ( ≤ Po ℝ ∧ 0 ∈ ℝ ) → ¬ 0 ≤ 0 )
7 5 6 mpan2 ⊢ ( ≤ Po ℝ → ¬ 0 ≤ 0 )
8 4 7 mt2 ⊢ ¬ ≤ Po ℝ
9 3 8 pm3.2i ⊢ ( < Po ℝ ∧ ¬ ≤ Po ℝ )