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	$$⊢\left(<\mathrm{Po}ℝ\wedge \neg \le \mathrm{Po}ℝ\right)$$

Proof

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