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 ℝ \land \neg \leq Po ℝ)$

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2		sopo	$⊢ < Or ℝ \to < Po ℝ$
3	1 2	ax-mp	$⊢ < Po ℝ$
4		0le0	$⊢ 0 \leq 0$
5		0re	$⊢ 0 \in ℝ$
6		poirr	$⊢ (\leq Po ℝ \land 0 \in ℝ) \to \neg 0 \leq 0$
7	5 6	mpan2	$⊢ \leq Po ℝ \to \neg 0 \leq 0$
8	4 7	mt2	$⊢ \neg \leq Po ℝ$
9	3 8	pm3.2i	$⊢ (< Po ℝ \land \neg \leq Po ℝ)$