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 ℝ )