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

Metamath Proof Explorer

Theorem domnsym

Description: Theorem 22(i) of Suppes p. 97. (Contributed by NM, 10-Jun-1998)

		Ref	Expression
	Assertion	domnsym	$⊢ A ≼ B \to \neg B ≺ A$

Step	Hyp	Ref	Expression
1		brdom2	$⊢ A ≼ B \leftrightarrow (A ≺ B \lor A \approx B)$
2		sdomnsym	$⊢ A ≺ B \to \neg B ≺ A$
3		sdomnen	$⊢ B ≺ A \to \neg B \approx A$
4		ensym	$⊢ A \approx B \to B \approx A$
5	3 4	nsyl3	$⊢ A \approx B \to \neg B ≺ A$
6	2 5	jaoi	$⊢ (A ≺ B \lor A \approx B) \to \neg B ≺ A$
7	1 6	sylbi	$⊢ A ≼ B \to \neg B ≺ A$