Theorem psssstr

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

	Ref	Expression
Assertion	psssstr	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊊ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		sspss	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ⊊ 𝐶 ∨ 𝐵 = 𝐶 ) )
2		psstr	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐶 ) → 𝐴 ⊊ 𝐶 )
3	2	ex	⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐵 ⊊ 𝐶 → 𝐴 ⊊ 𝐶 ) )
4		psseq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 ⊊ 𝐵 ↔ 𝐴 ⊊ 𝐶 ) )
5	4	biimpcd	⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐵 = 𝐶 → 𝐴 ⊊ 𝐶 ) )
6	3 5	jaod	⊢ ( 𝐴 ⊊ 𝐵 → ( ( 𝐵 ⊊ 𝐶 ∨ 𝐵 = 𝐶 ) → 𝐴 ⊊ 𝐶 ) )
7	6	imp	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ ( 𝐵 ⊊ 𝐶 ∨ 𝐵 = 𝐶 ) ) → 𝐴 ⊊ 𝐶 )
8	1 7	sylan2b	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊊ 𝐶 )