sspsstr

Description: Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996)

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

Step	Hyp	Ref	Expression
1		sspss	$⊢ A \subseteq B \leftrightarrow (A \subset B \lor A = B)$
2		psstr	$⊢ (A \subset B \land B \subset C) \to A \subset C$
3	2	ex	$⊢ A \subset B \to (B \subset C \to A \subset C)$
4		psseq1	$⊢ A = B \to (A \subset C \leftrightarrow B \subset C)$
5	4	biimprd	$⊢ A = B \to (B \subset C \to A \subset C)$
6	3 5	jaoi	$⊢ (A \subset B \lor A = B) \to (B \subset C \to A \subset C)$
7	6	imp	$⊢ ((A \subset B \lor A = B) \land B \subset C) \to A \subset C$
8	1 7	sylanb	$⊢ (A \subseteq B \land B \subset C) \to A \subset C$

Metamath Proof Explorer