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

Metamath Proof Explorer

Theorem pssn2lp

Description: Proper subclass has no 2-cycle loops. Compare Theorem 8 of Suppes p. 23. (Contributed by NM, 7-Feb-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	pssn2lp	$⊢ \neg (A \subset B \land B \subset A)$

Proof

Step	Hyp	Ref	Expression
1		dfpss3	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg B \subseteq A)$
2	1	simprbi	$⊢ A \subset B \to \neg B \subseteq A$
3		pssss	$⊢ B \subset A \to B \subseteq A$
4	2 3	nsyl	$⊢ A \subset B \to \neg B \subset A$
5		imnan	$⊢ (A \subset B \to \neg B \subset A) \leftrightarrow \neg (A \subset B \land B \subset A)$
6	4 5	mpbi	$⊢ \neg (A \subset B \land B \subset A)$