Metamath Proof Explorer

Theorem psstr

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

Ref Expression
Assertion psstr ⊢ A ⊂ B ∧ B ⊂ C → A ⊂ C

Proof

Step Hyp Ref Expression
1 pssss ⊢ A ⊂ B → A ⊆ B
2 pssss ⊢ B ⊂ C → B ⊆ C
3 1 2 sylan9ss ⊢ A ⊂ B ∧ B ⊂ C → A ⊆ C
4 pssn2lp ⊢ ¬ C ⊂ B ∧ B ⊂ C
5 psseq1 ⊢ A = C → A ⊂ B ↔ C ⊂ B
6 5 anbi1d ⊢ A = C → A ⊂ B ∧ B ⊂ C ↔ C ⊂ B ∧ B ⊂ C
7 4 6 mtbiri ⊢ A = C → ¬ A ⊂ B ∧ B ⊂ C
8 7 con2i ⊢ A ⊂ B ∧ B ⊂ C → ¬ A = C
9 dfpss2 ⊢ A ⊂ C ↔ A ⊆ C ∧ ¬ A = C
10 3 8 9 sylanbrc ⊢ A ⊂ B ∧ B ⊂ C → A ⊂ C