psstr

Description: Transitive law for proper subclass. Theorem 9 of Suppes p. 23. (Contributed by NM, 7-Feb-1996)

		Ref	Expression
	Assertion	psstr	$⊢ (A \subset B \land B \subset C) \to A \subset C$

Step	Hyp	Ref	Expression
1		pssss	$⊢ A \subset B \to A \subseteq B$
2		pssss	$⊢ B \subset C \to B \subseteq C$
3	1 2	sylan9ss	$⊢ (A \subset B \land B \subset C) \to A \subseteq C$
4		pssn2lp	$⊢ \neg (C \subset B \land B \subset C)$
5		psseq1	$⊢ A = C \to (A \subset B \leftrightarrow C \subset B)$
6	5	anbi1d	$⊢ A = C \to ((A \subset B \land B \subset C) \leftrightarrow (C \subset B \land B \subset C))$
7	4 6	mtbiri	$⊢ A = C \to \neg (A \subset B \land B \subset C)$
8	7	con2i	$⊢ (A \subset B \land B \subset C) \to \neg A = C$
9		dfpss2	$⊢ A \subset C \leftrightarrow (A \subseteq C \land \neg A = C)$
10	3 8 9	sylanbrc	$⊢ (A \subset B \land B \subset C) \to A \subset C$

Metamath Proof Explorer