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 \left(A\subset B\wedge B\subset A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfpss3	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$
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	$$⊢\left(A\subset B\to \neg B\subset A\right)\leftrightarrow \neg \left(A\subset B\wedge B\subset A\right)$$
6	4 5	mpbi	$$⊢\neg \left(A\subset B\wedge B\subset A\right)$$