Theorem sspsstr

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

	Ref	Expression
Assertion	sspsstr	$$⊢\left(A\subseteq B\wedge B\subset C\right)\to A\subset C$$

Proof

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